Set Truncation

1. Set Truncation

1 Set Truncation

module Lib.SetTrunc where

This file defines the set truncation of a type as a higher inductive type (as done in the HoTT book, §6.9). The set truncation of a type X is the ``best approximation'' of X as a set. As such, every map from X to a set A has a unique extension from the set truncation of X to A. We're also going to show that set truncating can be obtained by quotienting a type by its mere equality. It means that, in fact, only one representant of identifiable points are chosen. For instance, set truncating the type of singleton will give a single point, as any singleton is equivalent to any other and hence, by univalence, they are all identifiable between themselves.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Lib.SetQuotients
import Lib.Prop.Levels
import Lib.PropTrunc
import Lib.Prop.Paths
import Lib.IsFinite

1.2 Specification

Let A be a type and B a set. A map f : A → B is a set truncation whenever its precomposition is an equivalence.

precomp-Set (A : U) (B : UU-Set) (f : A → (Set/type B)) (C : UU-Set) (g : Set/hom B C) : A → Set/type C =
  λz. g (f z)

is-set-trunc (A : U) (B : UU-Set) (f : A → (Set/type B)) : U =
  (C : UU-Set) → is-equiv (Set/hom B C) (A → Set/type C) (precomp-Set A B f C)

We can extract the underlying map of a set truncation.

is-set-trunc/map (A : U) (B : UU-Set) (f : A → Set/type B) (H : is-set-trunc A B f) (C : UU-Set) (g : A → Set/type C) : Set/hom B C =
  (H C g).1.1

1.3 Definition as an higher inductive type

We can define set truncation as a higher inductive type.

data Set-trunc (A : U) : U
  = Set-trunc/unit (a : A)
  | Set-trunc/squash (x y : Set-trunc A) (p q : Path (Set-trunc A) x y) <i j> [(i=0) → p j, (i=1) → q j, (j=0) → x, (j=1) → y]

We can remark that the second constructor makes Set-trunc a set.

Set-trunc/is-set (A : U) : is-set (Set-trunc A) =
  λx y p q i j. Set-trunc/squash x y p q i j

Thus, Set-trunc A is in UU-Set.

Set-trunc/Set (A : U) : UU-Set =
  (Set-trunc A, Set-trunc/is-set A)

Of course, as it is an inductive type, it has a recurrence principle.

rec-Set-trunc (A : U) (B : UU-Set) (f : A → Set/type B) : Set-trunc A → Set/type B = split
  Set-trunc/unit a → f a
  Set-trunc/squash x y p q i j →
    ( Set/is-set B
      ( rec-Set-trunc A B f x)
      ( rec-Set-trunc A B f y)
      ( ap ( Set-trunc A) ( Set/type B) ( rec-Set-trunc A B f) x y p)
      ( ap ( Set-trunc A) ( Set/type B) ( rec-Set-trunc A B f) x y q)) i j

The recurrence principle can also be expressed using propositions.

rec-Set-trunc/Prop (A : U) (B : UU-Prop) (f : A → Prop/type B) : Set-trunc A → Prop/type B =
  rec-Set-trunc A
    ( Prop/Set B) f

1.4 Induction principle

ind-Set-trunc (A : U) (B : (x : Set-trunc A) → UU-Set) (f : (x : A) → Set/type (B (Set-trunc/unit x)))
                 : (x : Set-trunc A) → Set/type (B x) = split
  Set-trunc/unit a → f a
  Set-trunc/squash x y p q i j →
    square/dependent-fill
      ( Set-trunc A) B x y p q
      ( λi' j'. Set-trunc/squash x y p q i' j')
      ( ind-Set-trunc A B f x)
      ( ind-Set-trunc A B f y)
      ( λk. ind-Set-trunc A B f (p k))
      ( λk. ind-Set-trunc A B f (q k)) i j

Likewise, it can be expressed using propositions.

ind-Set-trunc/Prop (A : U) (B : Set-trunc A → UU-Prop) (f : (x : A) → Prop/type (B (Set-trunc/unit x)))
                      : (x : Set-trunc A) → Prop/type (B x) =
  ind-Set-trunc A
    ( λx. Prop/Set (B x)) f

1.5 Proposition of equality between elements of set truncation

Set-trunc/eq/Prop (X : U) (x y : Set-trunc X) : UU-Prop =
  ( Path (Set-trunc X) x y,
    Set-trunc/is-set X x y)

1.6 Set-trunc/unit defines a set truncation

Set-trunc/is-set-trunc/right-htpy (X : U) (Y : UU-Set) (h : X → Set/type Y)
                                     : Path (X → Set/type Y)
                                            (precomp-Set X (Set-trunc/Set X) (λz. Set-trunc/unit z) Y (rec-Set-trunc X Y h)) h =
  refl (X → Set/type Y) h

Set-trunc/is-set-trunc/left-htpy (X : U) (Y : UU-Set) (h : (Set-trunc X) → Set/type Y)
                                     : Path (Set-trunc X → Set/type Y)
                                            (rec-Set-trunc X Y (precomp-Set X (Set-trunc/Set X) (λz. Set-trunc/unit z) Y h)) h =
  λi x.
    ind-Set-trunc/Prop X
      ( λx'. Set/eq/Prop Y (rec-Set-trunc X Y (precomp-Set X (Set-trunc/Set X) (λz. Set-trunc/unit z) Y h) x') (h x'))
      ( λx'. refl (Set/type Y) (h (Set-trunc/unit x'))) x i

Set-trunc/is-set-trunc (X : U) : is-set-trunc X (Set-trunc/Set X) (λx. Set-trunc/unit x) =
  λY.
    has-inverse/is-equiv
      ( Set-trunc X → Set/type Y)
      ( X → Set/type Y)
      ( precomp-Set X (Set-trunc/Set X) (λx. Set-trunc/unit x) Y)
      ( rec-Set-trunc X Y,
        ( Set-trunc/is-set-trunc/right-htpy X Y,
          Set-trunc/is-set-trunc/left-htpy X Y))

1.7 Set-trunc/unit is surjective

Of course, sending an element to its set truncation is surjective.

Set-trunc/is-surjective (X : U) : is-surj X (Set-trunc X) (λx. Set-trunc/unit x) =
  ind-Set-trunc/Prop X
    ( λx. Prop-trunc/Prop (Fib X (Set-trunc X) (λz. Set-trunc/unit z) x))
    ( λx. Prop-trunc/unit (x, refl (Set-trunc X) (Set-trunc/unit x)))

1.8 Set truncation is a set quotient

We show that set truncation is actually a type that is quotiented by the equivalence relation that is the mere equality.

Set-trunc/relation/map (X : U) (x y : X) : (p : mere-eq X x y) → Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y) =
  rec-Prop-trunc
    ( Path X x y)
    ( Set-trunc/eq/Prop X
      ( Set-trunc/unit x)
      ( Set-trunc/unit y))
    ( ap X (Set-trunc X) (λz. Set-trunc/unit z) x y)

Set-trunc/relation (X : U) : reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set-trunc X) =
  ( (λx. Set-trunc/unit x),
    Set-trunc/relation/map X)

We can define the back-and-forth map using the induction principle in both cases.

Set-trunc/Set-quotient/map (X : U) : Set-trunc X → Set-quotient X (mere-eq/Eq-Rel X) =
  rec-Set-trunc X
    ( Set-quotient/Set X
      ( mere-eq/Eq-Rel X))
    ( λx. Set-quotient/q x)

Set-trunc/Set-quotient/inv-map (X : U) : Set-quotient X (mere-eq/Eq-Rel X) → Set-trunc X =
  rec-Set-quotient X
    ( mere-eq/Eq-Rel X)
    ( Set-trunc/Set X)
    ( λx. Set-trunc/unit x)
    ( Set-trunc/relation/map X)

By induction, these maps are inverse to each other.

Set-trunc/Set-quotient/right-htpy (X : U) : (x : Set-quotient X (mere-eq/Eq-Rel X))
                                          → Path (Set-quotient X (mere-eq/Eq-Rel X))
                                                  (Set-trunc/Set-quotient/map X (Set-trunc/Set-quotient/inv-map X x)) x =
  ind-Set-quotient/Prop X
    ( mere-eq/Eq-Rel X)
    ( λx. Set/eq/Prop
          ( Set-quotient/Set X (mere-eq/Eq-Rel X))
          ( Set-trunc/Set-quotient/map X (Set-trunc/Set-quotient/inv-map X x)) x)
    ( λx. rec-Set-trunc/Prop X
          ( Set/eq/Prop
            ( Set-quotient/Set X (mere-eq/Eq-Rel X))
            ( Set-trunc/Set-quotient/map X (Set-trunc/Set-quotient/inv-map X (Set-quotient/q x))) (Set-quotient/q x))
          ( λ_. refl (Set-quotient X (mere-eq/Eq-Rel X)) (Set-quotient/q x)) (Set-trunc/unit x))          

Set-trunc/Set-quotient/left-htpy (X : U) : (x : Set-trunc X)
                                          → Path (Set-trunc X)
                                                 (Set-trunc/Set-quotient/inv-map X (Set-trunc/Set-quotient/map X x)) x =
  ind-Set-trunc/Prop X
    ( λx. Set/eq/Prop
          ( Set-trunc/Set X)
          ( Set-trunc/Set-quotient/inv-map X (Set-trunc/Set-quotient/map X x)) x)
    ( λx. rec-Set-quotient/Prop X
          ( mere-eq/Eq-Rel X)
          ( Set/eq/Prop
            ( Set-trunc/Set X)
            ( Set-trunc/Set-quotient/inv-map X (Set-trunc/Set-quotient/map X (Set-trunc/unit x)))
            ( Set-trunc/unit x))
          ( λ_. refl (Set-trunc X) (Set-trunc/unit x)) (Set-quotient/q x))

That is, a type quotiented by mere equality is equivalent to its set truncation.

Set-trunc/Set-quotient (X : U) : Equiv (Set-trunc X) (Set-quotient X (mere-eq/Eq-Rel X)) =
  has-inverse/Equiv
    ( Set-trunc X)
    ( Set-quotient X (mere-eq/Eq-Rel X))
    ( Set-trunc/Set-quotient/map X)
    ( Set-trunc/Set-quotient/inv-map X,
      ( Set-trunc/Set-quotient/right-htpy X,
        Set-trunc/Set-quotient/left-htpy X))

Moreover, we can show that set truncation is a set quotient. First, we define the map using precomp-Set-quotient, and the inverse map using the recursor of set truncation.

Set-trunc/is-set-quotient/map (X : U) (B : UU-Set)
                                 : (Set-trunc X → Set/type B) → (reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set/type B)) =
  precomp-Set-quotient X
    ( mere-eq/Eq-Rel X)
    ( Set-trunc/Set X) B
    ( Set-trunc/relation X)

Set-trunc/is-set-quotient/inv-map (X : U) (B : UU-Set)
                                     : (reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set/type B)) → (Set-trunc X → Set/type B) =
  λt. rec-Set-trunc X B t.1

These maps are inverse to each other by function extensionality.

Set-trunc/is-set-quotient/right-htpy (X : U) (B : UU-Set) (t : reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set/type B))
                                        : Path (reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set/type B))
                                               (Set-trunc/is-set-quotient/map X B (Set-trunc/is-set-quotient/inv-map X B t)) t =
  SgPath-prop
    ( X → Set/type B)
    ( λf. (x y : X) → (mere-eq X x y) → Path (Set/type B) (f x) (f y))
    ( λf. is-prop/pi-2 X
          ( λ_. X)
          ( λx y. mere-eq X x y → Path (Set/type B) (f x) (f y))
          ( λx y. is-prop/pi
                  ( mere-eq X x y)
                  ( λ_. Path (Set/type B) (f x) (f y))
                  ( λ_. Set/is-set B (f x) (f y))))
    ( Set-trunc/is-set-quotient/map X B (Set-trunc/is-set-quotient/inv-map X B t)) t
    ( λi x. refl (Set/type B) (t.1 x) i)

Set-trunc/is-set-quotient/left-htpy (X : U) (B : UU-Set) (f : Set-trunc X → Set/type B)
                                       : Path (Set-trunc X → Set/type B)
                                              (Set-trunc/is-set-quotient/inv-map X B (Set-trunc/is-set-quotient/map X B f)) f =
  λi x.
    ind-Set-trunc/Prop X
      ( λz. Set/eq/Prop B
            ( Set-trunc/is-set-quotient/inv-map X B (Set-trunc/is-set-quotient/map X B f) z)
            ( f z))
      ( λz. refl (Set/type B) (f (Set-trunc/unit z))) x i

Thus, set truncation is a set quotient.

Set-trunc/is-set-quotient (X : U) : is-set-quotient X (mere-eq/Eq-Rel X) (Set-trunc/Set X) (Set-trunc/relation X) =
  λB.
    has-inverse/is-equiv
      ( Set-trunc X → Set/type B)
      ( reflecting-map-Eq-Rel X (mere-eq/Eq-Rel X) (Set/type B))
      ( Set-trunc/is-set-quotient/map X B)
      ( Set-trunc/is-set-quotient/inv-map X B,
        ( Set-trunc/is-set-quotient/right-htpy X B,
          Set-trunc/is-set-quotient/left-htpy X B))

1.9 Equivalence between set truncation equality and mere equality

We have shown that || X ||₀ ≅ X/||x = y||. Moreover, quotienting is effective; that is, q(x) = q(y) ≅ R(x, y). Here, R is mere equality. Hence, |x|₀ = |y|₀ ≅ q(x) = q(y) ≅ || x = y ||.

Set-trunc/is-effective (X : U) (x y : X) : Equiv (Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y)) (mere-eq X x y) =
  Equiv/trans
    ( Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y))
    ( Path (Set-quotient X (mere-eq/Eq-Rel X)) (Set-quotient/q x) (Set-quotient/q y))
    ( mere-eq X x y)
    ( Equiv/Equiv-id
      ( Set-trunc X)
      ( Set-quotient X (mere-eq/Eq-Rel X))
      ( Set-trunc/Set-quotient X)
      ( Set-trunc/unit x)
      ( Set-trunc/unit y))
    ( is-set-quotient/is-effective X
      ( mere-eq/Eq-Rel X) x y)

Set-trunc/is-effective' (X : U) (x y : X) : Equiv (mere-eq X x y) (Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y)) =
  Equiv/sym 
    ( Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y))
    ( mere-eq X x y)
    ( Set-trunc/is-effective X x y)

Set-trunc/is-effective/map (X : U) (x y : X) : Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y) → mere-eq X x y =
  Equiv/map
    ( Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y))
    ( mere-eq X x y)
    ( Set-trunc/is-effective X x y)

Set-trunc/is-effective/inv-map (X : U) (x y : X) : mere-eq X x y → Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y) =
  Equiv/inv-map
    ( Path (Set-trunc X) (Set-trunc/unit x) (Set-trunc/unit y))
    ( mere-eq X x y)
    ( Set-trunc/is-effective X x y)

1.10 Map between truncations

If there is a map between A and B, then there is a map between the set truncations of A and B.

Set-trunc/map (A B : U) (f : A → B) : (Set-trunc A) → Set-trunc B =
  rec-Set-trunc A
    ( Set-trunc/Set B)
    ( λx. Set-trunc/unit (f x))

1.11 Closure under equivalences

If A and B are equivalent, then ||A||₀ and ||B||₀ are, of course, also both equivalent.

Set-trunc/Path (A B : U) (p : Path U A B) : Path U (Set-trunc A) (Set-trunc B) =
  λi. Set-trunc (p i)

Set-trunc/Equiv (A B : U) (e : Equiv A B) : Equiv (Set-trunc A) (Set-trunc B) =
  path-to-equiv
    ( Set-trunc A)
    ( Set-trunc B)
    ( Set-trunc/Path A B
      ( equiv-to-path A B e))

Set-trunc/Equiv/map (A B : U) (e : Equiv A B) : (Set-trunc A) → (Set-trunc B) =
  Equiv/map
    ( Set-trunc A)
    ( Set-trunc B)
    ( Set-trunc/Equiv A B e)

Set-trunc/Equiv/inv-map (A B : U) (e : Equiv A B) : (Set-trunc B) → (Set-trunc A) =
  Equiv/inv-map
    ( Set-trunc A)
    ( Set-trunc B)
    ( Set-trunc/Equiv A B e)

1.12 Distribution over products

We have an equivalence ||A||₀ × ||B||₀ ≅ ||A × B||₀.

Set-trunc/prod/map (A B : U) (t : (Set-trunc A) * (Set-trunc B)) : Set-trunc (A * B) =
  rec-Set-trunc A
    ( Set-trunc/Set (A * B))
    ( λx. rec-Set-trunc B
          ( Set-trunc/Set (A * B))
          ( λy. Set-trunc/unit (x, y)) t.2) t.1

Set-trunc/prod/inv-map (A B : U)
                            : (t : Set-trunc (A * B))
                            → (Set-trunc A) * (Set-trunc B) =
  rec-Set-trunc (A * B)
    ( Set/closed-Prod
      ( Set-trunc/Set A)
      ( Set-trunc/Set B))
    ( λu. (Set-trunc/unit u.1, Set-trunc/unit u.2))

lock Set/closed-Prod/is-set Set-trunc/is-set
Set-trunc/prod/right-htpy (A B : U)
                               : (t : Set-trunc (A * B))
                               → Path (Set-trunc (A * B))
                                      (Set-trunc/prod/map A B (Set-trunc/prod/inv-map A B t)) t =
  ind-Set-trunc/Prop
    ( A * B)
    ( λu. Set-trunc/eq/Prop
          ( A * B)
          ( Set-trunc/prod/map A B (Set-trunc/prod/inv-map A B u)) u)
    ( λu. refl (Set-trunc (A * B)) (Set-trunc/unit u))

Set-trunc/prod/left-htpy (A B : U) (t : (Set-trunc A * Set-trunc B))
                              : Path (Set-trunc A * Set-trunc B)
                                     (Set-trunc/prod/inv-map A B (Set-trunc/prod/map A B t)) t =
  ind-Set-trunc/Prop A
    ( λx. Set/eq/Prop
            ( Set/closed-Prod
              ( Set-trunc/Set A)
              ( Set-trunc/Set B))
            ( Set-trunc/prod/inv-map A B (Set-trunc/prod/map A B (x, t.2)))
            ( x, t.2))
    ( λx. ind-Set-trunc/Prop B
          ( λy. Set/eq/Prop
                ( Set/closed-Prod
                  ( Set-trunc/Set A)
                  ( Set-trunc/Set B))
                ( Set-trunc/prod/inv-map A B (Set-trunc/prod/map A B (Set-trunc/unit x, y)))
                ( Set-trunc/unit x, y))
          ( λy. refl (Set-trunc A * Set-trunc B) (Set-trunc/unit x, Set-trunc/unit y)) t.2) t.1

Set-trunc/closed-Prod (A B : U) : Equiv (Set-trunc A * Set-trunc B) (Set-trunc (A * B)) =
  has-inverse/Equiv
    ( Set-trunc A * Set-trunc B)
    ( Set-trunc (A * B))
    ( Set-trunc/prod/map A B)
    ( Set-trunc/prod/inv-map A B,
      ( Set-trunc/prod/right-htpy A B,
        Set-trunc/prod/left-htpy A B))
unlock Set/closed-Prod/is-set Set-trunc/is-set

1.13 Distribution over coproduct

We also have an equivalence || A ||₀ + || B ||₀ ≅ || A + B ||₀. Maps:

Set-trunc/Coprod/map (A B : U) : Coprod (Set-trunc A) (Set-trunc B) → Set-trunc (Coprod A B) = split
  inl x →
    rec-Set-trunc A
      ( Set-trunc/Set (Coprod A B))
      ( λa. Set-trunc/unit (inl a)) x
  inr y →
    rec-Set-trunc B
      ( Set-trunc/Set (Coprod A B))
      ( λb. Set-trunc/unit (inr b)) y

Set-trunc/Coprod/inv-map' (A B : U) : Coprod A B → Coprod (Set-trunc A) (Set-trunc B) = split
  inl a → inl (Set-trunc/unit a)
  inr b → inr (Set-trunc/unit b)

Set-trunc/Coprod/inv-map (A B : U) : Set-trunc (Coprod A B) → Coprod (Set-trunc A) (Set-trunc B) =
  rec-Set-trunc
    ( Coprod A B)
    ( Set/closed-Coprod
      ( Set-trunc/Set A)
      ( Set-trunc/Set B))
    ( Set-trunc/Coprod/inv-map' A B)

Homotopies:

Set-trunc/Coprod/right-htpy' (A B : U) : (u : Coprod A B)
                                        → Path (Set-trunc (Coprod A B))
                                               (Set-trunc/Coprod/map A B (Set-trunc/Coprod/inv-map A B (Set-trunc/unit u)))
                                               (Set-trunc/unit u) = split
  inl x → refl (Set-trunc (Coprod A B)) (Set-trunc/unit (inl x))
  inr y → refl (Set-trunc (Coprod A B)) (Set-trunc/unit (inr y))

Set-trunc/Coprod/right-htpy (A B : U) : (u : Set-trunc (Coprod A B))
                                       → Path (Set-trunc (Coprod A B))
                                              (Set-trunc/Coprod/map A B (Set-trunc/Coprod/inv-map A B u)) u =
  ind-Set-trunc/Prop
    ( Coprod A B)
    ( λu. Set-trunc/eq/Prop
      ( Coprod A B)
      ( Set-trunc/Coprod/map A B (Set-trunc/Coprod/inv-map A B u)) u)
    ( Set-trunc/Coprod/right-htpy' A B)

Set-trunc/Coprod/left-htpy (A B : U) : (u : Coprod (Set-trunc A) (Set-trunc B))
                                      → Path (Coprod (Set-trunc A) (Set-trunc B))
                                             (Set-trunc/Coprod/inv-map A B (Set-trunc/Coprod/map A B u)) u = split
  inl x →
    ind-Set-trunc/Prop A
      ( λu. Set/eq/Prop
            ( Set/closed-Coprod (Set-trunc/Set A) (Set-trunc/Set B))
            ( Set-trunc/Coprod/inv-map A B (Set-trunc/Coprod/map A B (inl u))) (inl u))
      ( λa. refl (Coprod (Set-trunc A) (Set-trunc B)) (inl (Set-trunc/unit a))) x
  inr y →
    ind-Set-trunc/Prop B
      ( λu. Set/eq/Prop
            ( Set/closed-Coprod (Set-trunc/Set A) (Set-trunc/Set B))
            ( Set-trunc/Coprod/inv-map A B (Set-trunc/Coprod/map A B (inr u))) (inr u))
      ( λb. refl (Coprod (Set-trunc A) (Set-trunc B)) (inr (Set-trunc/unit b))) y

Equivalence:

Set-trunc/closed-Coprod (A B : U) : Equiv (Coprod (Set-trunc A) (Set-trunc B)) (Set-trunc (Coprod A B)) =
  has-inverse/Equiv
    ( Coprod (Set-trunc A) (Set-trunc B))
    ( Set-trunc (Coprod A B))
    ( Set-trunc/Coprod/map A B)
    ( Set-trunc/Coprod/inv-map A B,
      ( Set-trunc/Coprod/right-htpy A B,
        Set-trunc/Coprod/left-htpy A B))

Set-trunc/closed-Coprod' (A B : U) : Equiv (Set-trunc (Coprod A B)) (Coprod (Set-trunc A) (Set-trunc B)) =
  has-inverse/Equiv
    ( Set-trunc (Coprod A B))
    ( Coprod (Set-trunc A) (Set-trunc B))
    ( Set-trunc/Coprod/inv-map A B)
    ( Set-trunc/Coprod/map A B,
      ( Set-trunc/Coprod/left-htpy A B,
        Set-trunc/Coprod/right-htpy A B))

1.14 Closure of contractibility

If A is contractible, then the set truncation of A is also contractible.

Set-trunc/closed-Path (A : U) (x y : A) (p : Path A x y) : Path (Set-trunc A) (Set-trunc/unit x) (Set-trunc/unit y) =
  λi. Set-trunc/unit (p i)

Set-trunc/closed-contr/aux (A : U) (is-contr-A : is-contr A) (x : A)
                              : Path (Set-trunc A) (Set-trunc/unit (center A is-contr-A)) (Set-trunc/unit x) =
  Set-trunc/closed-Path A
    ( center A is-contr-A) x
    ( contraction A is-contr-A x)

Set-trunc/closed-contr (A : U) (is-contr-A : is-contr A) : is-contr (Set-trunc A) =
  ( Set-trunc/unit (center A is-contr-A),
    ind-Set-trunc/Prop A
      ( λx'. Set-trunc/eq/Prop A (Set-trunc/unit (center A is-contr-A)) x')
      ( Set-trunc/closed-contr/aux A is-contr-A))

1.15 Set truncation of a set is the set itself

Set/Set-trunc/map (X : UU-Set) : Set-trunc (Set/type X) → Set/type X =
  rec-Set-trunc
    ( Set/type X) X
    ( id (Set/type X))

Prop/Set-trunc/map (X : UU-Prop) : Set-trunc (Prop/type X) → Prop/type X =
  Set/Set-trunc/map
    ( Prop/Set X)

Homotopies:

Set/Equiv-Set-trunc/left-htpy (X : UU-Set) (x : Set/type X)
                                 : Path (Set/type X) (Set/Set-trunc/map X (Set-trunc/unit x)) x =
  refl (Set/type X) x

Set/Equiv-Set-trunc/right-htpy (X : UU-Set) : (x : Set-trunc (Set/type X))
                                            → Path (Set-trunc (Set/type X)) (Set-trunc/unit (Set/Set-trunc/map X x)) x =
  ind-Set-trunc
    ( Set/type X)
    ( λz. Prop/Set (Set-trunc/eq/Prop (Set/type X) (Set-trunc/unit (Set/Set-trunc/map X z)) z))
    ( λz. refl (Set-trunc (Set/type X)) (Set-trunc/unit z))

Set/Equiv-Set-trunc (X : UU-Set) : Equiv (Set/type X) (Set-trunc (Set/type X)) =
  has-inverse/Equiv
    ( Set/type X)
    ( Set-trunc (Set/type X))
    ( λx. Set-trunc/unit x)
    ( ( Set/Set-trunc/map X),
      ( Set/Equiv-Set-trunc/right-htpy X,
        Set/Equiv-Set-trunc/left-htpy X))

Set-trunc/Equiv-Set (X : UU-Set) : Equiv (Set-trunc (Set/type X)) (Set/type X) =
  Equiv/sym
    ( Set/type X)
    ( Set-trunc (Set/type X))
    ( Set/Equiv-Set-trunc X)

1.16 Connected type

A type is connected whenever its set truncation is contractible.

is-conn (A : U) : U =
  is-contr (Set-trunc A)

A connected type is inhabited.

is-conn/is-inhabited (A : U) (is-conn-A : is-conn A) : Prop-trunc A =
  rec-Set-trunc A
    ( Prop/Set (Prop-trunc/Prop A))
    ( λx. Prop-trunc/unit x)
    ( center (Set-trunc A) is-conn-A)

1.17 Surjectivity of fiber inclusion whenever `A` is connected and pointed

If A is connected, then for any family B over A, the map B a → Σ A B defined as follows:

fiber-inclusion (A : U) (B : A → U) (a : A) : B a → Σ A B =
  λb. (a, b)

is surjective:

is-connected/fiber-inclusion/Path (A : U) (B : A → U) (H : is-conn A) (a : A) (x : A) (y : B x) (p : Path A a x)
                                     : Path (Σ A B) (fiber-inclusion A B a (tr A x a (inv A a x p) B y)) (x, y) =
  J A a
    ( λz q. (u : B z) → Path (Σ A B) (fiber-inclusion A B a (tr A z a (inv A a z q) B u)) (z, u))
    ( λu. comp (Σ A B)
          ( fiber-inclusion A B a (tr A a a (inv A a a (refl A a)) B u))
          ( fiber-inclusion A B a (tr A a a (refl A a) B u))
          ( ap (Path A a a) (Σ A B) (λq. fiber-inclusion A B a (tr A a a q B u)) (inv A a a (refl A a)) (refl A a) (inv/refl A a))
          ( a, u)
          ( ap (B a) (Σ A B) (λv. (a, v)) (tr A a a (refl A a) B u) u (tr/refl-path A a B u))) x p y

is-connected/fiber-inclusion-is-surj (A : U) (B : A → U) (H : is-conn A) (a : A) : is-surj (B a) (Σ A B) (fiber-inclusion A B a) =
  λb.
    rec-Prop-trunc
      ( Path A a b.1)
      ( Prop-trunc/Prop (Fib (B a) (Σ A B) (fiber-inclusion A B a) b))
      ( λp. Prop-trunc/unit
            ( tr A b.1 a (inv A a b.1 p) B b.2,
              inv (Σ A B) (a, tr A b.1 a (inv A a b.1 p) B b.2) b
              ( is-connected/fiber-inclusion/Path A B H a b.1 b.2 p)))
      ( Set-trunc/is-effective/map A a b.1
        ( is-contr/all-elements-equal
          ( Set-trunc A) H
          ( Set-trunc/unit a)
          ( Set-trunc/unit b.1)))

1.18 Set truncated map is surjective whenever original map is surjective

Let f : A → B. The set truncation of f, || f ||₀ : || A ||₀ → || B ||₀ defined as follows:

Set-trunc-map (A B : U) (f : A → B) : Set-trunc A → Set-trunc B =
  rec-Set-trunc A
    ( Set-trunc/Set B)
    ( λa. Set-trunc/unit (f a))

is surjective whenever f is surjective.

Set-trunc-map/is-surj (A B : U) (f : A → B) (H : is-surj A B f) : is-surj (Set-trunc A) (Set-trunc B) (Set-trunc-map A B f) =
  ind-Set-trunc/Prop B
    ( λy. Prop-trunc/Prop (Fib (Set-trunc A) (Set-trunc B) (Set-trunc-map A B f) y))
    ( λy. rec-Prop-trunc
          ( Fib A B f y)
          ( Prop-trunc/Prop (Fib (Set-trunc A) (Set-trunc B) (Set-trunc-map A B f) (Set-trunc/unit y)))
            ( λt. Prop-trunc/unit (Set-trunc/unit t.1, ap B (Set-trunc B) (λz. Set-trunc/unit z) y (f t.1) t.2))
            ( H y))

1.19 Empty set truncation means empty type

is-empty-Set-trunc/is-empty (A : U) : is-empty (Set-trunc A) → is-empty A =
  λf a. f (Set-trunc/unit a)

1.20 Finite type means finite set truncation

is-finite/is-finite-Set-trunc (X : U) (H : is-finite X) : is-finite (Set-trunc X) =
  is-finite/closed-Equiv
    ( Set-trunc X) X
    ( Set-trunc/Equiv-Set
      ( X, is-finite/is-set X H)) H

1.21 Finite set truncation implies map

We show that if || A ||₀ is finite with k elements, then there merely exists an f : Fin k → A such that |⋅|₀ ˆ f is an equivalence. Morally, |⋅|₀ ˆ f is the equivalence between Fin k and || A ||₀.

is-finite-Set-trunc/Prop-trunc-map (A : U) (k : Nat) (e : Equiv (Fin k) (Set-trunc A))
                                      : Prop-trunc ((x : Fin k)
                                                      → Fib A (Set-trunc A) (λz. Set-trunc/unit z)
                                                              (Equiv/map (Fin k) (Set-trunc A) e x)) =
  Fin/choice k
    ( λx. Fib A (Set-trunc A) (λz. Set-trunc/unit z) (Equiv/map (Fin k) (Set-trunc A) e x))
    ( λx. Set-trunc/is-surjective A
            ( Equiv/map (Fin k) (Set-trunc A) e x))

is-finite-Set-trunc/has-Equiv-map (A : U) (k : Nat) (e : Equiv (Fin k) (Set-trunc A))
                                     : Prop-trunc (Σ ((Fin k) → A)
                                                     (λf. (x : Fin k)
                                                          → Path (Set-trunc A) (Set-trunc/unit (f x))
                                                                 (Equiv/map (Fin k) (Set-trunc A) e x))) =
  rec-Prop-trunc
    ( (x : Fin k) → Fib A (Set-trunc A) (λz. Set-trunc/unit z) (Equiv/map (Fin k) (Set-trunc A) e x))
    ( Prop-trunc/Prop
      ( Σ (Fin k → A) (λf. (x : Fin k) → Path (Set-trunc A) (Set-trunc/unit (f x)) (Equiv/map (Fin k) (Set-trunc A) e x))))
    ( λg. Prop-trunc/unit
          ( λx. (g x).1,
            λx. inv (Set-trunc A) (Equiv/map (Fin k) (Set-trunc A) e x) (Set-trunc/unit (g x).1) (g x).2))
    ( is-finite-Set-trunc/Prop-trunc-map A k e)