Disjoint subtypes

Content created by Fredrik Bakke, Louis Wasserman and Egbert Rijke.

Created on 2025-02-25.
Last modified on 2026-05-02.

module foundation.disjoint-subtypes where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.empty-subtypes
open import foundation.empty-types
open import foundation.intersections-subtypes
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

Two subtypes are disjoint if their intersection is empty.

Definition

module _
  {l1 l2 l3 : Level} {A : UU l1} (B : subtype l2 A) (C : subtype l3 A)
  where

  disjoint-subtype-Prop : Prop (l1 ⊔ l2 ⊔ l3)
  disjoint-subtype-Prop = is-empty-prop-subtype (intersection-subtype B C)

  disjoint-subtype : UU (l1 ⊔ l2 ⊔ l3)
  disjoint-subtype = type-Prop disjoint-subtype-Prop

Properties

A subtype disjoint from itself is empty

module _
  {l1 l2 : Level} {A : UU l1} (B : subtype l2 A)
  where

  is-empty-disjoint-subtype-self :
    disjoint-subtype B B → is-empty (type-subtype B)
  is-empty-disjoint-subtype-self H (b , b∈B) = H b (b∈B , b∈B)

See also

Recent changes