Subtypes

1. Subtypes

1 Subtypes

module Lib.SubTypes where

This file defines subtypes and some properties associated to them.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.FundamentalTheorem
import Lib.Prop.Equiv
import Lib.Prop.Levels
import Lib.Prop.Proposition

1.2 Definitions

is-subtype (X : U) (P : X → U) : U = (x : X) → is-prop (P x)

is-decidable-subtype (X : U) (P : X → U) : U = is-subtype X P * ((x : X) → is-decidable (P x))

1.3 Equivalence of substructure

We show a lemma that helps us show that the identity type of a subtype agrees with the identity type of the original type.

substructure/is-contr-total-Eq (A : U) (B C : A → U) (is-contr-tot : is-contr (Σ A B))
                               (is-subtype-C : is-subtype A C) (a : A) (b : B a) (c : C a)
                                  : is-contr (Σ (Σ A C) (λt. B t.1)) =
  is-contr/is-contr-equiv (Σ (Σ A C) (λt. B t.1)) (Σ (Σ A B) (λt. C t.1))
    (Equiv/assoc-Σ A C B)
    (is-contr/closed-retract (Σ (Σ A B) (λt. C t.1)) (C a)
      (Sg/left-unit-law-is-contr (Σ A B) (λt. C t.1) is-contr-tot (a, b))
      (is-prop/is-proof-irrelevant (C a) (is-subtype-C a) c))

1.4 Equivalent subtypes

If P and Q are two subtypes of A such that there are back-and-forth maps between P and Q, then Σ A P is equivalent to Σ A Q.

subtype/Equiv-tot (A : U) (P Q : A → U) (is-subtype-P : is-subtype A P) (is-subtype-Q : is-subtype A Q)
                  (f : (x : A) → P x → Q x) (g : (x : A) → Q x → P x) : Equiv (Σ A P) (Σ A Q) =
  fam-equiv/Equiv-tot A P Q f
    (λx. Prop/is-equiv
          ( P x, is-subtype-P x)
          ( Q x, is-subtype-Q x)
          ( f x)
          ( g x))

1.5 A map is injective iff its fibrations are propositions

subtype/is-inj-prop-map (A B : U) (f : A → B) (is-subtype-fib : (b : B) → is-prop (Fib A B f b)) (x : A)
                             : (y : A) → is-equiv (Path A x y) (Path B (f x) (f y)) (ap A B f x y) =
  fundamental-theorem-id 
    A
    ( λy. Path B (f x) (f y)) x
    ( ap A B f x)
    ( is-prop/is-proof-irrelevant
      ( Fib A B f (f x))
      ( is-subtype-fib (f x))
      ( x, refl B (f x)))

1.6 Equivalence of `pr1`

We have shown that fib pr1 x is equivalent to B x. Then, whenever B x is a proposition for all x, pr1 is an equivalence.

pr1/is-inj (A : U) (B : A → U) (is-prop-B : (x : A) → is-prop (B x)) (t u : Σ A B)
                      : is-equiv (Path (Σ A B) t u) (Path A t.1 u.1) (ap (Σ A B) A (λv. v.1) t u) =
  subtype/is-inj-prop-map
    ( Σ A B)
    A
    ( λv. v.1)
    ( λx. is-prop/closed-equiv
      ( Fib (Σ A B) A (λv. v.1) x)
      ( B x)
      ( Equiv/fib-space-Equiv A B x)
      ( is-prop-B x))
    t u