HoTTEST Summer School HoTT Notes 5

Homotopies

Let's consider the type theory represent of proposition "$f: A → B$ is surjective":

$$ \Pi_{(y:B)}\Sigma_{(x:A)} f(x) = y $$

Note $=$ (or we should use $=_B$) here stands for this is an instance of "identity type".

Apply AC we introduced in last course:

$$ \Sigma_{(g: B\rightarrow A)} \Pi_{(y:B)} f(g(y)) = y $$

So we can see there's some relation between $f \cdot g$ and $id_B$, this relation is similar, but weaker than $f \cdot g \underset{B → B}{=} id_B$.

And this relation is what we call homotopy.

Formal definition

For two dependent functions $f$ and $g$,

$$ f \sim g := \Pi_{(x:A)} f(x) = g(x) $$

Here $f \sim g$ is the type of homotopies from $f$ to $g$.

module _ {l1 l2} {A : Set l1} {B : A → Set l2} where
    _~_ : (f g : (x : A) → B x) → Set (l1 ⊔ l2)
    f ~ g = (x : A) → f x ≡ g x

Here we can say $g$ is a section of $f$ and $f$ is a retraction of $g$, we'll introduce these concepts later.

Example

neg-bool : Bool → Bool
neg-bool true = false
neg-bool false = true

There's no way can we prove:

$$ neg\text{-}bool \cdot neg\text{-}bool ≐ id_{Bool} $$

Instead, we can define a pointwise identification between the values of $neg\text{-}bool \cdot neg\text{-}bool$ and $id_{Bool}$.

neg-neg-bool : (neg-bool ∘ neg-bool) ~ id
neg-neg-bool false = refl
neg-neg-bool true = refl

Commutativity of Diagrams¹

We can use homotopies to express the commutativity of diagrams.

For example, we say that a triangle commutes if it comes equipped with a homotopy $H: f \sim g \cdot h$.

$$ \require{amscd} \require{cancel} \def\diaguparrow#1{\smash{\raise.6em\rlap{\ \ \scriptstyle #1} \lower.6em{\cancelto{}{\Space{2em}{1.7em}{0px}}}}} \begin{CD} A @>f>>X\\ @VhVV \diaguparrow{g}\\ B \end{CD} $$

A square is similar:

$$ \require{amscd} \begin{CD} A @>g>> A'\\ @VfVV @Vf'VV\\ B @>h>> B' \end{CD} $$

Here $h \cdot f \sim f' \cdot g$.

And we can have homotopies between homotopies:

If $H, K: f \sim g$ are two homotopies, ie

$$ f,g: \Pi_{(x:A)}B(x) $$ $$ H,K: f \sim g $$

then the type of homotopies $f \sim g$ between them is just the type

$$ \alpha: \Pi_{(x:A)}H(x) = K(x) $$

And we can push this further, homotopies of homotopies of homotopies, homotopies⁴, etc.

Operations on Homotopies

refl-htpy: $\Pi_{(f:\Pi_{(x:A)}B(x))} f \sim f$

inv-htpy: $\Pi_{(f,g:\Pi_{(x:A)}B(x))} (f \sim g) → (g \sim f)$

concat-htpy: $\Pi_{(f,g,h:\Pi_{(x:A)}B(x))} (f \sim g) → (g \sim h) \rightarrow (f \sim h)$

We will often write $H^{-1}$ for $inv\text{-}htpy(H)$, and $H \cdot K$ for $concat\text{-}htpy(H, K)$

refl-htpy : {A : Set} {B : A → Set} (f : (x : A) → B x) → f ~ f
refl-htpy = λ f x → refl

inv-htpy : {A : Set} {B : A → Set} {f g : (x : A) → B x} → f ~ g → g ~ f
inv-htpy htpy = λ x → sym (htpy x)

concat-htpy : {A : Set} {B : A → Set} {f g h : (x : A) → B x} → f ~ g → g ~ h → f ~ h
concat-htpy htpy1 htpy2 = λ x → trans (htpy1 x) (htpy2 x)

_·_ : {A : Set} {B : A → Set} {f g h : (x : A) → B x} → f ~ g → g ~ h → f ~ h
_·_ = concat-htpy

Laws of Homotopies

Homotopies satisfy the groupoid laws, ie. associative, has left and right unit (refl-htpy), left and right inverse law.

assoc-htpy : {A B : Set} {f g h i : A → B} (H : f ~ g) (K : g ~ h) (L : h ~ i) → (((H · K) · L) ~ (H · (K · L)))
assoc-htpy H K L = λ x → trans-assoc (H x) {K x} {L x}

left-unit-htpy : {A B : Set} {f g : A → B} (H : f ~ g) → ((refl-htpy f · H) ~ H)
left-unit-htpy H = λ x → refl

right-unit : {A : Set} {x y : A} {p : x ≡ y} → (trans p (refl {x = y})) ≡ p
right-unit {p = refl} = refl

right-unit-htpy : {A B : Set} {f g : A → B} (H : f ~ g) → ((H · (refl-htpy g)) ~ H)
right-unit-htpy {_} {_} {f} {g} H = λ x → right-unit

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

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

left-inv-htpy : {A B : Set} {f g : A → B} (H : f ~ g) → (((inv-htpy H) · H) ~ (refl-htpy g))
left-inv-htpy H = λ x → left-inv (H x)

right-inv-htpy : {A B : Set} {f g : A → B} (H : f ~ g) → ((H · (inv-htpy H)) ~ (refl-htpy f))
right-inv-htpy H = λ x → right-inv (H x)

Whiskering

Whiskering operations are operations that allow us to compose homotopies with functions.

• Suppose $H: f \sim g$ for two functions $f,g: A → B$, and let $h:B→C$. We define

$$ h \cdot H := λx.ap_h(H(x)) : h \cdot f \sim h \cdot g $$

f-chain-H : {A B C : Set} {f g : A → B} (h : B → C) (H : f ~ g) → ((h ∘ f) ~ (h ∘ g))
f-chain-H h H = λ x → cong h (H x)

• Suppose $f: A → B$ and $H: g \sim h$ for two functions $g,h:B→C$. We define

$$ H \cdot f := λx.H(f(x)) : h \cdot f \sim g \cdot f $$

H-chain-f : {A B C : Set} {g h : B → C} (H : g ~ h) (f : A → B) → ((h ∘ f) ~ (g ∘ f))
H-chain-f H f = λ x → sym (H (f x))

Bi-invertible maps

We can use homotopies to define sections, retractions and equivalence of a map.

• A section is a right inverse of some morphism.

  $$ sec(f) := \Sigma_{(g:B\rightarrow A)} f\cdot g \sim id_B $$

  For any equivalence $e : 𝐴 ≃ 𝐵$ we define $e^{-1}$ to be the section of $e$.

  sec : {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) → Set (l1 ⊔ l2)
  sec {_} {_} {A} {B} f = Σ (B → A) (λ g → ((f ∘ g) ~ id))
  

• A retraction is a left inverse of some morphism.

  $$ retr(f) := \Sigma_{(h:B\rightarrow A)} h\cdot f \sim id_A $$

  retr : {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) → Set (l1 ⊔ l2)
  retr {_} {_} {A} {B} f = Σ (B → A) (λ h → ((h ∘ f) ~ id))
  

• equivalence = section + retraction

  $$ is\text{-}equiv(f) := sec(f) × retr(f) $$

  is-equiv : {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) → Set (l1 ⊔ l2)
  is-equiv {_} {_} {A} {B} f = sec f × retr f
  

  Or "f is bi-invertible".

  We will write $A ≃ B$ for the type $\Sigma_{(f:A→B)} is\text{-}equiv(f)$ of all equivalences from $A$ to $B$.

• Besides, we can define $has\text{-}inverse$:

  $$ has\text{-}inverse(f) := \Sigma_{(g:B→A)} (f\cdot g \sim id_B) \times (g\cdot f \sim id_A) $$

  has-inverse : {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) → Set (l1 ⊔ l2)
  has-inverse{_} {_} {A} {B} f = Σ (B → A) (λ g → ((f ∘ g) ~ id) × ((g ∘ f) ~ id))
  

We can prove that $has\text{-}inverse(f) \leftrightarrow is\text{-}equiv(f)$

is-equiv-to-has-inverse : {A : Set} {B : Set} {f : A → B} → is-equiv f → has-inverse f
is-equiv-to-has-inverse {f = f} ((r-inv , r-homo), (l-inv , l-homo)) = 
    r-inv , (r-homo , 
        inv-htpy (inv-htpy 
            l-homo · (
                H-chain-f (H-chain-f l-homo r-inv · f-chain-H l-inv r-homo) f
            )
        )
    )

has-inverse-to-is-equiv : {A : Set} {B : Set} {f : A → B} → has-inverse f → is-equiv f
has-inverse-to-is-equiv (inv , (r-homo , l-homo)) = (inv , r-homo) , (inv , l-homo)

Example of Equivalences

Ref section 9.2.9 and 9.2.10 of the book Introduction to Homotopy Type Theory

Laws & Operations on Equivalences

We have $refl\text{-}eqiv$, $inv\text{-}eqiv$ and $concat\text{-}eqiv$.

Function Extensionality & Univalence Axiom

Let $P := \Pi_{(x:A)}B(x)$, because both $\sim$ and $≃$ are refl. we get

$$ id\text{-}to\text{-}\sim: \Pi_{(f,g:P)}(f \underset{P}{=} g \rightarrow f \sim g) $$

$$ id\text{-}to\text{-}≃: \Pi_{(A,B:\mathcal{U})}(A\underset{\mathcal{U}}{=}B \rightarrow A ≃ B) $$

With these, we can define function extensionality:

The principle of functional extensionality states that two functions are equal if their values are equal at every argument. —— nLab

$$ funext:\Pi_{(f,g:P)}is\text{-}equiv(id\text{-}to\text{-}\sim(f, g)) $$

Similarly, we can define the univalence axiom (UA):

In intensional type theory, identity types behave like path space objects; this viewpoint is called homotopy type theory. This induces furthermore a notion of homotopy fibers, hence of homotopy equivalences between types.

On the other hand, if type theory contains a universe Type, so that types can be considered as points of Type, then between two types we also have an identity type Paths $Paths_{Type}(X,Y)$. The univalence axiom says that these two notions of “sameness” for types are the same. —— nLab

$$ UA^{\mathcal{U}}:\Pi_{(A,B:\mathcal{U})}is\text{-}eqiv(id\text{-}to\text{-}≃(A,B)) $$

Identification in Σ-types

We can characterize the identity type of Σ-type as a Σ-type of identity types.

Fix an $A$ type, $x: A ⊢ B(x)\ \ type$, $S := Σ_{(x:A)}B(x)$, we want a reflexive relation $z, z': S ⊢ R(z,z')\ \ type$, we can call this type $Eq\text{-}Σ$

Assume

$$ z ≐ (x, y) $$

$$ z' ≐ (x', y') $$

By $ap_{pr_{1}}$² we should have a $p: x \underset{A}= x'$

Recall the $tr_B$ function we mentioned before, with this, we can define "type of identifications of $y$ with $y'$ over $p$":

$$ (y \overset{B}{\underset{p}=} y') := (tr_B(p,y) \underset{B(x')}{=} y') $$

And we can then define $Eq\text{-}Σ$:

$$ Eq\text{-}Σ(z, z') := Σ_{(p:x=x')} (y \overset{B}{\underset{p}=} y') $$

Eq-Σ : {A : Set} {B : A → Set} (z : Σ A B) (z' : Σ A B) → Set
Eq-Σ {_} {B} z z' = Σ (fst z ≡ fst z') (λ p → transport B p (snd z) ≡ snd z')

To show this is reflexive, we should have a term:

$$ refl\text{-}Eq\text{-}Σ : \Pi_{(z:S)}Eq\text{-}\Sigma(z, z) $$

This is easy to construct such a term with a pair of refl (notice fst refl and snd refl in this pair is in different types ³):

refl-Eq-Σ : ∀{A : Set} {B : A → Set} (z : Σ A B) → Eq-Σ z z
refl-Eq-Σ z = refl , refl

With path induction⁴, we can push this a step further to:

$$ pair\text{-}Eq : \Pi_{(z,z':S)} ((z\underset{S}=z') \rightarrow Eq\text{-}\Sigma(z, z')) $$

pair-Eq : ∀{A : Set} {B : A → Set} {z : Σ A B} {z' : Σ A B} →
    (z ≡ z') → Eq-Σ z z'
pair-Eq {_} {_} {z} refl = refl-Eq-Σ z

And reversely:

$$ Eq\text{-}pair : \Pi_{(z,z':S)} (Eq\text{-}\Sigma(z, z') \rightarrow (z\underset{S}=z')) $$ ⁵

Eq-pair : ∀{A : Set} {B : A → Set} {z : Σ A B} {z' : Σ A B} →
    Eq-Σ z z' → (z ≡ z')
Eq-pair (refl , refl) = refl

And we can find that $Eq\text{-}pair$ and $pair\text{-}Eq$ are "inverse" of each other:

$$ \Pi_{(z,z':S)} \Pi_{(w:Eq\text{-}Σ(z,z'))} Eq\text{-}pair(pair\text{-}Eq(w)) = w $$

$$ \Pi_{(z,z':S)} \Pi_{(r:z=z')} pair\text{-}Eq(Eq\text{-}pair(w)) = w $$

inv-l : ∀{A : Set} {B : A → Set} {z : Σ A B} {z' : Σ A B} (w : Eq-Σ z z') →
    pair-Eq ( Eq-pair w ) ≡ w
inv-l (refl , refl) = refl

inv-r : ∀{A : Set} {B : A → Set} {z : Σ A B} {z' : Σ A B} (r : z ≡ z') →
     Eq-pair ( pair-Eq r ) ≡ r
inv-r refl = refl

So we can find out that $Eq\text{-}pair$ is a section of $pair\text{-}Eq$ and $pair\text{-}Eq$ is a retraction of $Eq\text{-}pair$.

Thus we can form an equivalence between $z = z'$ and $Eq\text{-}Σ(z, z')$:

$$ (z \underset{S}= z') ≃ Eq\text{-}Σ(z, z') $$

Materials

Lecture Note

HoTTEST_Lecture_5.pdf

Record on Youtube