# Subtypes

```agda
module foundation-core.subtypes where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.propositional-maps
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.transport-along-identifications
open import foundation-core.truncated-maps
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
```

</details>

## Idea

A **subtype** of a type `A` is a family of
[propositions](foundation-core.propositions.md) over `A`. The underlying type of
a subtype `P` of `A` is the [total space](foundation.dependent-pair-types.md)
`Σ A B`.

## Definitions

### Subtypes

```agda
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

  eq-is-in-subtype :
    {x : A} {p q : is-in-subtype x} → p ＝ q
  eq-is-in-subtype {x} = eq-is-prop (is-prop-is-in-subtype x)

  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
```

### The containment relation on subtypes

```agda
module _
  {l1 : Level} {A : UU l1}
  where

  leq-prop-subtype :
    {l2 l3 : Level} → subtype l2 A → subtype l3 A → Prop (l1 ⊔ l2 ⊔ l3)
  leq-prop-subtype P Q =
    Π-Prop A (λ x → hom-Prop (P x) (Q x))

  infix  _⊆_
  _⊆_ :
    {l2 l3 : Level} (P : subtype l2 A) (Q : subtype l3 A) → UU (l1 ⊔ l2 ⊔ l3)
  P ⊆ Q = type-Prop (leq-prop-subtype P Q)

  is-prop-leq-subtype :
    {l2 l3 : Level} (P : subtype l2 A) (Q : subtype l3 A) → is-prop (P ⊆ Q)
  is-prop-leq-subtype P Q =
    is-prop-type-Prop (leq-prop-subtype P Q)
```

## Properties

### The containment relation on subtypes is a preordering

```agda
module _
  {l1 : Level} {A : UU l1}
  where

  refl-leq-subtype : {l2 : Level} (P : subtype l2 A) → P ⊆ P
  refl-leq-subtype P x = id

  transitive-leq-subtype :
    {l2 l3 l4 : Level}
    (P : subtype l2 A) (Q : subtype l3 A) (R : subtype l4 A) →
    Q ⊆ R → P ⊆ Q → P ⊆ R
  transitive-leq-subtype P Q R H K x = H x ∘ K x
```

### Equality in subtypes

```agda
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' (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 a propositional map

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

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

  prop-map-subtype : prop-map (type-subtype B) A
  pr1 prop-map-subtype = inclusion-subtype B
  pr2 prop-map-subtype = is-prop-map-inclusion-subtype
```

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

```agda
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
        ( is-prop-map-inclusion-subtype B)

  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 a `k`-truncated map to a `k`-truncated map into a subtype

```agda
module _
  {l1 l2 l3 : Level} (k : 𝕋) {A : UU l1} (B : subtype l2 A) {X : UU l3}
  where

  abstract
    is-trunc-map-into-subtype :
      {f : X → A} → is-trunc-map k f →
      (p : (x : X) → is-in-subtype B (f x)) →
      is-trunc-map k {B = type-subtype B} (λ x → (f x , p x))
    is-trunc-map-into-subtype H p (a , b) =
      is-trunc-equiv k _
        ( equiv-tot (λ x → extensionality-type-subtype' B _ _))
        ( H a)

  trunc-map-into-subtype :
    (f : trunc-map k X A) → ((x : X) → is-in-subtype B (map-trunc-map f x)) →
    trunc-map k X (type-subtype B)
  pr1 (trunc-map-into-subtype f p) x = (map-trunc-map f x , p x)
  pr2 (trunc-map-into-subtype f p) =
    is-trunc-map-into-subtype
      ( is-trunc-map-map-trunc-map f)
      ( p)
```

### Restriction of an embedding to an embedding into a subtype

```agda
module _
  {l1 l2 l3 : Level} {A : UU l1} (B : subtype l2 A) {X : UU l3} (f : X ↪ A)
  (p : (x : X) → is-in-subtype B (map-emb f x))
  where

  map-emb-into-subtype : X → type-subtype B
  pr1 (map-emb-into-subtype x) = map-emb f x
  pr2 (map-emb-into-subtype x) = p x

  abstract
    is-emb-map-emb-into-subtype : is-emb map-emb-into-subtype
    is-emb-map-emb-into-subtype =
      is-emb-is-prop-map
        ( is-trunc-map-into-subtype
          ( neg-one-𝕋)
          ( B)
          ( is-prop-map-is-emb (is-emb-map-emb f))
          ( p))

  emb-into-subtype : X ↪ type-subtype B
  pr1 emb-into-subtype = map-emb-into-subtype
  pr2 emb-into-subtype = is-emb-map-emb-into-subtype
```

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

```agda
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-fiber-pr1 B x) (is-prop-map-is-emb H x)
```

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

```agda
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

```agda
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

```agda
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))
```

```agda
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 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 is-equiv-f
      ( λ x → is-equiv-is-prop (is-subtype-P x) (is-subtype-Q (f x))
        ( (tr P (is-retraction-map-inv-is-equiv is-equiv-f x)) ∘ (h (f x))))
```