Subtypes

module foundation-core.subtypes where

Imports

open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.logical-equivalences
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtype-identity-principle
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

Idea

A subtype of a type A is a family of propositions over A. The underlying type of a subtype P of A is the total space Σ A B.

Definition

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

  is-subtype : UU (l1 ⊔ l2)
  is-subtype = (x : A) → is-prop (B x)

  is-property : UU (l1 ⊔ l2)
  is-property = is-subtype

subtype : {l1 : Level} (l : Level) (A : UU l1) → UU (l1 ⊔ lsuc l)
subtype l A = A → Prop l

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

  is-in-subtype : A → UU l2
  is-in-subtype x = type-Prop (P x)

  is-prop-is-in-subtype : (x : A) → is-prop (is-in-subtype x)
  is-prop-is-in-subtype x = is-prop-type-Prop (P x)

  type-subtype : UU (l1 ⊔ l2)
  type-subtype = Σ A is-in-subtype

  inclusion-subtype : type-subtype → A
  inclusion-subtype = pr1

  ap-inclusion-subtype :
    (x y : type-subtype) →
    x ＝ y → (inclusion-subtype x ＝ inclusion-subtype y)
  ap-inclusion-subtype x y p = ap inclusion-subtype p

  is-in-subtype-inclusion-subtype :
    (x : type-subtype) → is-in-subtype (inclusion-subtype x)
  is-in-subtype-inclusion-subtype = pr2

  is-closed-under-eq-subtype :
    {x y : A} → is-in-subtype x → (x ＝ y) → is-in-subtype y
  is-closed-under-eq-subtype p refl = p

  is-closed-under-eq-subtype' :
    {x y : A} → is-in-subtype y → (x ＝ y) → is-in-subtype x
  is-closed-under-eq-subtype' p refl = p

Properties

Equality in subtypes

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

  Eq-type-subtype : (x y : type-subtype P) → UU l1
  Eq-type-subtype x y = (pr1 x ＝ pr1 y)

  extensionality-type-subtype' :
    (a b : type-subtype P) → (a ＝ b) ≃ (pr1 a ＝ pr1 b)
  extensionality-type-subtype' (pair a p) =
    extensionality-type-subtype P p refl (λ x → id-equiv)

  eq-type-subtype :
    {a b : type-subtype P} → (pr1 a ＝ pr1 b) → a ＝ b
  eq-type-subtype {a} {b} = map-inv-equiv (extensionality-type-subtype' a b)

If `B` is a subtype of `A`, then the projection map `Σ A B → A` is an embedding

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

  abstract
    is-emb-inclusion-subtype : is-emb (inclusion-subtype B)
    is-emb-inclusion-subtype =
      is-emb-is-prop-map
        ( λ x →
          is-prop-equiv
            ( equiv-fib-pr1 (is-in-subtype B) x)
            ( is-prop-is-in-subtype B x))

  emb-subtype : type-subtype B ↪ A
  pr1 emb-subtype = inclusion-subtype B
  pr2 emb-subtype = is-emb-inclusion-subtype

  equiv-ap-inclusion-subtype :
    {s t : type-subtype B} →
    (s ＝ t) ≃ (inclusion-subtype B s ＝ inclusion-subtype B t)
  pr1 (equiv-ap-inclusion-subtype {s} {t}) = ap-inclusion-subtype B s t
  pr2 (equiv-ap-inclusion-subtype {s} {t}) = is-emb-inclusion-subtype s t

Restriction of an embedding to an embedding into a subtype

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

  emb-into-subtype :
    {l3 : Level} {X : UU l3} (f : X ↪ A) →
    ((x : X) → is-in-subtype B (map-emb f x)) →
    X ↪ type-subtype B
  pr1 (emb-into-subtype f p) x = (map-emb f x , p x)
  pr2 (emb-into-subtype f p) =
    is-emb-is-prop-map
      ( λ (a , b) →
        is-prop-equiv
          ( equiv-tot
            ( λ x → extensionality-type-subtype' B (map-emb f x , p x) (a , b)))
          ( is-prop-map-is-emb (is-emb-map-emb f) a))

If the projection map of a type family is an embedding, then the type family is a subtype

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  abstract
    is-subtype-is-emb-pr1 : is-emb (pr1 {B = B}) → is-subtype B
    is-subtype-is-emb-pr1 H x =
      is-prop-equiv' (equiv-fib-pr1 B x) (is-prop-map-is-emb H x)

A subtype of a `k+1`-truncated type is `k+1`-truncated

module _
  {l1 l2 : Level} (k : 𝕋) {A : UU l1} (P : subtype l2 A)
  where

  abstract
    is-trunc-type-subtype :
      is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) (type-subtype P)
    is-trunc-type-subtype =
      is-trunc-is-emb k
        ( inclusion-subtype P)
        ( is-emb-inclusion-subtype P)

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

  abstract
    is-prop-type-subtype : is-prop A → is-prop (type-subtype P)
    is-prop-type-subtype = is-trunc-type-subtype neg-two-𝕋 P

  abstract
    is-set-type-subtype : is-set A → is-set (type-subtype P)
    is-set-type-subtype = is-trunc-type-subtype neg-one-𝕋 P

prop-subprop :
  {l1 l2 : Level} (A : Prop l1) (P : subtype l2 (type-Prop A)) → Prop (l1 ⊔ l2)
pr1 (prop-subprop A P) = type-subtype P
pr2 (prop-subprop A P) = is-prop-type-subtype P (is-prop-type-Prop A)

set-subset :
  {l1 l2 : Level} (A : Set l1) (P : subtype l2 (type-Set A)) → Set (l1 ⊔ l2)
pr1 (set-subset A P) = type-subtype P
pr2 (set-subset A P) = is-set-type-subtype P (is-set-type-Set A)

Logically equivalent subtypes induce equivalences on the underlying type of a subtype

equiv-type-subtype :
  { l1 l2 l3 : Level} {A : UU l1} {P : A → UU l2} {Q : A → UU l3} →
  ( is-subtype-P : is-subtype P) (is-subtype-Q : is-subtype Q) →
  ( f : (x : A) → P x → Q x) →
  ( g : (x : A) → Q x → P x) →
  ( Σ A P) ≃ (Σ A Q)
pr1 (equiv-type-subtype is-subtype-P is-subtype-Q f g) = tot f
pr2 (equiv-type-subtype is-subtype-P is-subtype-Q f g) =
  is-equiv-tot-is-fiberwise-equiv {f = f}
    ( λ x → is-equiv-is-prop (is-subtype-P x) (is-subtype-Q x) (g x))

Equivalences of subtypes

equiv-subtype-equiv :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} (e : A ≃ B)
  (C : A → Prop l3) (D : B → Prop l4) →
  ((x : A) → type-Prop (C x) ↔ type-Prop (D (map-equiv e x))) →
  type-subtype C ≃ type-subtype D
equiv-subtype-equiv e C D H =
  equiv-Σ (type-Prop ∘ D) (e) (λ x → equiv-iff' (C x) (D (map-equiv e x)) (H x))

abstract
  is-equiv-subtype-is-equiv :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
    {P : A → UU l3} {Q : B → UU l4}
    (is-subtype-P : is-subtype P) (is-subtype-Q : is-subtype Q)
    (f : A → B) (g : (x : A) → P x → Q (f x)) →
    is-equiv f → ((x : A) → (Q (f x)) → P x) → is-equiv (map-Σ Q f g)
  is-equiv-subtype-is-equiv {Q = Q} is-subtype-P is-subtype-Q f g is-equiv-f h =
    is-equiv-map-Σ Q f g is-equiv-f
      ( λ x → is-equiv-is-prop (is-subtype-P x) (is-subtype-Q (f x)) (h x))

abstract
  is-equiv-subtype-is-equiv' :
    {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
    {P : A → UU l3} {Q : B → UU l4}
    (is-subtype-P : is-subtype P) (is-subtype-Q : is-subtype Q)
    (f : A → B) (g : (x : A) → P x → Q (f x)) →
    (is-equiv-f : is-equiv f) →
    ((y : B) → (Q y) → P (map-inv-is-equiv is-equiv-f y)) →
    is-equiv (map-Σ Q f g)
  is-equiv-subtype-is-equiv' {P = P} {Q}
    is-subtype-P is-subtype-Q f g is-equiv-f h =
    is-equiv-map-Σ Q f g is-equiv-f
      ( λ x → is-equiv-is-prop (is-subtype-P x) (is-subtype-Q (f x))
        ( (tr P (isretr-map-inv-is-equiv is-equiv-f x)) ∘ (h (f x))))