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) $$ 1
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"