# 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 5 _⊆_
  _⊆_ :
    {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))))
```