HoTTEST Summer School HoTT Notes 6

Contractable Types

A contractible type is a type which has, up to identification, only one element. In other words, a contractible type is a type that comes equipped with a point, and an identification of this point with any point. —— Introduction to Homotopy Type Theory

Basically I think a contractible type is a type that all instances of it are equal.

Formally, we def:

$$ is\text{-}contr(A) := Σ_{(c:A)}\Pi_{(x:A)} c=x $$

is-contr : (A : Set) → Set
is-contr A = Σ A (λ c → (x : A) → x ≡ c)

We call $c$ here the center of contraction, and call the $$ C: \Pi_{(x:A)} c=x $$ part the contraction of $A$.

$C$ is a homotopy from the constant function to the identity function.

$$ const_C \sim id_A $$

is-contr' : (A : Set) → Set
is-contr' A = Σ A (λ c → const c ~ id)

-- prove these two definitions are same

-- helper functions
id-eq : {A : Set} → (x : A) → x ≡ id x
id-eq {A} x = refl

const-eq : {A : Set} → (c x : A) → c ≡ const c x
const-eq {A} c x = refl
-- helper functions end

is-contr-def-eq-l : {A : Set} → is-contr A → is-contr' A
is-contr-def-eq-l (c , Cdef1) = c , λ x → 
    sym $
    trans 
        (trans 
            (sym (id-eq x)) 
            (Cdef1 x))
        (const-eq c x)

is-contr-def-eq-r : {A : Set} → is-contr' A → is-contr A
is-contr-def-eq-r (c , Cdef2) = c , λ x → 
    sym $ 
    trans
        (trans 
            (const-eq c x) 
            (Cdef2 x))
        (sym (id-eq x))

Examples of contractible types includes the unit type and the type $\Sigma_{(x:A)}a=x$.

A type $A$ is contractible if and only if the map $const_{tt} : A \rightarrow \bf{1}$ is an equivalence.

const-tt : {A : Set} → A → ⊤
const-tt _ = tt

is-contr-equ-l : {A : Set} → (is-equiv (const-tt {A})) → (is-contr' A)
is-contr-equ-l (_ , (h , retrPart)) = h tt , λ x → retrPart x

is-contr-equ-r : {A : Set} → (is-contr' A) → (is-equiv (const-tt {A}))
is-contr-equ-r (c , C) = (const c , λ x → refl) , (const c , λ x → C x)

Singleton induction

Let $A$ be a type with an element $a$, we said $A$ satisfies singleton induction if for every type family $B$ over $A$, the map defined by $ev-pt(f) := f(a)$ where

$$ ev\text{-}pt : (\Pi_{(x:A)} B(x)) → B(a) $$ ¹

ev-pt : {A : Set} {B : A → Set} → (a : A) → ((x : A) → B x) → B a
ev-pt a f = f a

has a section, ie. has

$$ ind\text{-}sing_a : B(a) → \Pi_{(x:A)} B(x) $$

$$ comp\text{-}sing_a : ev\text{-}pt \cdot ind\text{-}sing_a \sim id $$

is-singleton : {A : Set} → (c : A) → Set₁
is-singleton {A} c = (B : A → Set) → sec (ev-pt {A} {B} c)

ind-sing : {A : Set} (a : A) → (is-singleton {A} a) → 
  (B : A → Set) → B a → (x : A) → B x
ind-sing = λ c is-sing B → fst (is-sing B)

comp-sing : {A : Set} {B : A → Set} (a : A) → (is-sing : is-singleton {A} a) → 
    (B : A → Set) → (ev-pt {A} {B} a ∘ ind-sing a is-sing B) ~ id
comp-sing = λ a is-sing B → snd (is-sing B) 

And $is-contr A$ is iff to $A$ satisfied to $ind\text{-}sing_a$ with some $a:A$.

is-contr''' : (A : Set) → Set₁
is-contr''' A = Σ A is-singleton

is-contr-equ-ind-l : {A : Set} → (is-contr''' A) → (is-contr' A)
is-contr-equ-ind-l (c , Cdef3) = c , fst (Cdef3 (_≡_ c)) refl

left-inv : {A : Set} {x y : A} (p : x ≡ y) → (trans p (sym p)) ≡ refl
left-inv refl = refl

is-contr-equ-ind-r : {A : Set} → (is-contr A) → (is-contr''' A)
is-contr-equ-ind-r (c , Cdef1) = c , λ B → 
    (λ bc x → transport B (trans (Cdef1 c) (sym (Cdef1 x))) bc) , 
    λ bc → cong (λ t → transport B t bc) (left-inv (Cdef1 c))

Fiber

The fiber of a morphism or bundle $f : E → B$ over a point of B is the collection of elements of E that are mapped by f to this point. —— nLab

$$ fib_f(b) := Σ_{(a:A)}f(a) = b $$

fib : {A : Set} {B : Set} (f : A → B) (b : B) → Set
fib {A} f b = Σ A (λ a → f a ≡ b)

And it can be regarded as type version of prop "b is in the image of f".

Identification of points in the fiber

For all $(a, p)$ and $(a', p')$ of type $fib_f(b)$ we have

$$ ((a,p)=(a',p')) ≃ Eq\text{-}fib_f((a, p),(a', p')) $$

where

$$ Eq\text{-}fib_f((a, p),(a', p')) := Σ_{(q : a = a')} (p = ap_f(q) ⋅ p') $$

Eq-fib : {A B : Set} {b : B} {f : A → B} ((a , p): fib f b) ((a' , p') : fib f b) → Set
Eq-fib {_} {_} {_} {f} (a , p) (a' , p') = Σ (a ≡ a') (λ aEq → p ≡ trans (cong f aEq) p')

The proof of it is a little long:

fib-eq-to-Eq-fib : {A B : Set} {b : B} {f : A → B} {s t : fib f b} → s ≡ t → Eq-fib s t
fib-eq-to-Eq-fib refl = refl , refl

Eq-fib-to-fib-eq : {A B : Set} {b : B} {f : A → B} {s t : fib f b} → Eq-fib s t → s ≡ t
Eq-fib-to-fib-eq (refl , refl) = refl

Eq-fib-inv-l : {A B : Set} {b : B} {f : A → B} {s t : fib f b} (w : Eq-fib s t) →
    fib-eq-to-Eq-fib (Eq-fib-to-fib-eq w) ≡ w
Eq-fib-inv-l (refl , refl) = refl

Eq-fib-inv-r : {A B : Set} {b : B} {f : A → B} {s t : fib f b} (w : s ≡ t) →
    Eq-fib-to-fib-eq (fib-eq-to-Eq-fib w) ≡ w
Eq-fib-inv-r refl = refl

is-equiv-fib-eq-to-Eq-fib : {A B : Set} {b : B} {f : A → B} {s t : fib f b} → is-equiv (fib-eq-to-Eq-fib {A} {B} {b} {f} {s} {t})
is-equiv-fib-eq-to-Eq-fib = 
    (Eq-fib-to-fib-eq , Eq-fib-inv-l) , 
    (Eq-fib-to-fib-eq , Eq-fib-inv-r)

fib-eq-equiv-Eq-fib : {A B : Set} {b : B} {f : A → B} ((a , p) : fib f b) ((a' , p') : fib f b) → 
    ((a , p) ≡ (a' , p')) ≃ Eq-fib (a , p) (a' , p')
fib-eq-equiv-Eq-fib (a , p) (a' , p') = 
    fib-eq-to-Eq-fib , is-equiv-fib-eq-to-Eq-fib 

Contractible Map

We say that a function $f : A → B$ is contractible if it comes equipped with an element of type

$$ is\text{-}contr(f) = \Sigma_{(b:B)} is\text{-}contr(fib_f(b)) $$

-- the type which contains "all fibers with same endpoint b" are contractable
is-contr-f : {A B : Set} (f : A → B) → Set
is-contr-f {B = B} f = Σ B (λ b → is-contr (fib f b))

We can prove any contractible map is an equivalence.

is-contr-f-to-inverse : {A B : Set} {f : A → B} → is-contr-f f → (B → A)
is-contr-f-to-inverse H = fst ∘ center-of-contr ∘ H

-- section part is easy, just take the center of the contraction out
contr-f-sec : {A B : Set} {f : A → B} → is-contr-f f → sec f
contr-f-sec H = is-contr-f-to-inverse H , snd ∘ center-of-contr ∘ H

-- retr part is a little complex
-- we need the following two lemmas

-- "fib f y" is contractable means each two fibs in such type are equal
contr-f-all-eq : {A B : Set} {f : A → B} {y : B} 
    → is-contr-f f → (a b : fib f y) → a ≡ b
contr-f-all-eq {y = y} H a b = trans ((snd (H y)) a) (sym ((snd (H y)) b))

-- construct an instance of fib f f(x)
-- the instance is basically (f⁻¹ f(x) , f(f⁻¹(f(x))) ≡ f(x))
fx-fiber : {A B : Set} {f : A → B} → (x : A) → 
    (H : is-contr-f f) → fib f (f x)
fx-fiber {f = f} x H = (fst (contr-f-sec H) (f x)) , ((snd (contr-f-sec H)) (f x))

-- by contr-f-all-eq, we can know the instance constructed by fx-fiber is equal to (x , refl),
-- which is also an instance of fib f f(x)
-- so (f⁻¹ f(x) , ...) ≡ (x , ...), thus we have f⁻¹ f(x) ≡ x and it is the retr we need
contr-f-retr : {A B : Set} {f : A → B} → is-contr-f f → retr f
contr-f-retr H = is-contr-f-to-inverse H , 
    λ x → cong fst (contr-f-all-eq H (fx-fiber x H) (x , refl))

contr-f-is-equiv : {A B : Set} {f : A → B} → is-contr-f f → is-equiv f
contr-f-is-equiv H = (contr-f-sec H , contr-f-retr H)

Coherently Invertible Maps

Consider an invertible map $f : A → B$, which equipped with an inverse $g : B → A$ and two homotopies : $G : (f ∘ g) \sim id$ and $H : (g ∘ f) \sim id$.

And if there exists another homotopy $K : G ∘ f \sim f ∘ H$, we call that $f$ is coherently invertible.

is-coh-invertible : {A : Set} {B : Set} (f : A → B) → Set
is-coh-invertible {A = A} {B = B} f = Σ (B → A) 
    (λ g → (Σ ((f ∘ g) ~ id) 
        (λ G → Σ ((g ∘ f) ~ id) (
            λ H → ((inv-htpy (H-chain-f G f)) ~ (f-chain-H f H))
        )
    )))

We can prove that any coherently invertible map has contractable fibers:

-- WIP, I tried hard but it seems to complex 😭
is-coh-invertible-has-contractable-fib : {A : Set} {B : Set} 
    (f : A → B) → is-coh-invertible f → is-contr-f f
is-coh-invertible-has-contractable-fib f (g , G , H , K) = λ b → (g b , G b) , λ x → trustMe

Naturality Square of the Homotopy

Let $f, g : A → B$ be functions, and consider $H : f ~ g$ and $p : x =_A y$. We define the identification

$$ nat\text{-}htpy(H, p) := ap_f (p) \cdot H(y) = H(x) \cdot ap_g(p) $$

ie.

$$ H(x) $$ $$ \require{amscd} \begin{CD} \ \ \ \ \ \ \ \ f(x) @= g(x)\\ @|ap_f(p) @|ap_g(p)\\ \ \ \ \ \ \ \ \ f(y) @= g(y) \end{CD} $$ $$ H(y) $$ ¹: $ev\text{-}pt$ is abbreviation for "evaluate at point"