HoTTEST Summer School HoTT Notes 5

Homotopies

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

$${\mathrm{\Pi }}_{(y:B)}{\mathrm{\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:

$${\mathrm{\Sigma }}_{(g:B\to A)}{\mathrm{\Pi }}_{(y:B)}f(g(y))=y$$

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

And this relation is what we call homotopy.

Formal definition

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

$$f\sim g:={\mathrm{\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\doteq i{d}_{Bool}$$

Instead, we can define a pointwise identification between the values of $neg\text{-}bool\cdot neg\text{-}bool$ and $i{d}_{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$.

$$\begin{array}{ccc}A& \stackrel{f}{\to }& X\\ h\downarrow & g{\cancel{}}^{}\\ B\end{array}$$

A square is similar:

$$\begin{array}{ccc}A& \stackrel{g}{\to }& A^{\prime }\\ f\downarrow & & f^{\prime }\downarrow & \\ B& \stackrel{h}{\to }& B^{\prime }\end{array}$$

Here $h\cdot f\sim f^{\prime }\cdot g$.

And we can have homotopies between homotopies:

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

$$f,g:{\mathrm{\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 :{\mathrm{\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: ${\mathrm{\Pi }}_{(f:{\mathrm{\Pi }}_{(x:A)}B(x))}f\sim f$

inv-htpy: ${\mathrm{\Pi }}_{(f,g:{\mathrm{\Pi }}_{(x:A)}B(x))}(f\sim g)\to (g\sim f)$

concat-htpy: ${\mathrm{\Pi }}_{(f,g,h:{\mathrm{\Pi }}_{(x:A)}B(x))}(f\sim g)\to (g\sim h)\to (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\to B$, and let $h:B\to C$. We define

$$h\cdot H:=\lambda x.a{p}_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\to B$ and $H:g\sim h$ for two functions $g,h:B\to C$. We define

$$H\cdot f:=\lambda 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):={\mathrm{\Sigma }}_{(g:B\to A)}f\cdot g\sim i{d}_B$$

  For any equivalence $e:𝐴\simeq 𝐵$ 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):={\mathrm{\Sigma }}_{(h:B\to A)}h\cdot f\sim i{d}_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)\times 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\simeq B$ for the type ${\mathrm{\Sigma }}_{(f:A\to B)}is\text{-}equiv(f)$ of all equivalences from $A$ to $B$.

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

  $$has\text{-}inverse(f):={\mathrm{\Sigma }}_{(g:B\to A)}(f\cdot g\sim i{d}_B)\times (g\cdot f\sim i{d}_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:={\mathrm{\Pi }}_{(x:A)}B(x)$, because both $\sim$ and $\simeq$ are refl. we get

$$id\text{-}to\text{-}\sim :{\mathrm{\Pi }}_{(f,g:P)}(f\underset{P}{=}g\to f\sim g)$$

$$id\text{-}to\text{-}\simeq :{\mathrm{\Pi }}_{(A,B:\mathcal{U})}(A\underset{\mathcal{U}}{=}B\to A\simeq 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:{\mathrm{\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 $Path{s}_{Type}(X,Y)$. The univalence axiom says that these two notions of “sameness” for types are the same. —— nLab

$$U{A}^{\mathcal{U}}:{\mathrm{\Pi }}_{(A,B:\mathcal{U})}is\text{-}eqiv(id\text{-}to\text{-}\simeq (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:={\Sigma }_{(x:A)}B(x)$, we want a reflexive relation $z,z^{\prime }:S⊢R(z,z^{\prime })type$, we can call this type $Eq\text{-}\Sigma$

Assume

$$z\doteq (x,y)$$

$$z^{\prime }\doteq (x^{\prime },y^{\prime })$$

By $a{p}_{p{r}_1}$² we should have a $p:x\underset{A}{=}{x}^{\prime }$

Recall the $t{r}_B$ function we mentioned before, with this, we can define "type of identifications of $y$ with $y^{\prime }$ over $p$":

$$(y\stackrel{B}{\underset{p}{=}}{y}^{\prime }):=(t{r}_B(p,y)\underset{B(x^{\prime })}{=}{y}^{\prime })$$

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

$$Eq\text{-}\Sigma (z,z^{\prime }):={\Sigma }_{(p:x=x^{\prime })}(y\stackrel{B}{\underset{p}{=}}{y}^{\prime })$$

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{-}\Sigma :{\mathrm{\Pi }}_{(z:S)}Eq\text{-}\mathrm{\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:{\mathrm{\Pi }}_{(z,z^{\prime }:S)}((z\underset{S}{=}{z}^{\prime })\to Eq\text{-}\mathrm{\Sigma }(z,z^{\prime }))$$

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:{\mathrm{\Pi }}_{(z,z^{\prime }:S)}(Eq\text{-}\mathrm{\Sigma }(z,z^{\prime })\to (z\underset{S}{=}{z}^{\prime }))$$ ⁵

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:

$${\mathrm{\Pi }}_{(z,z^{\prime }:S)}{\mathrm{\Pi }}_{(w:Eq\text{-}\Sigma (z,z^{\prime }))}Eq\text{-}pair(pair\text{-}Eq(w))=w$$

$${\mathrm{\Pi }}_{(z,z^{\prime }:S)}{\mathrm{\Pi }}_{(r:z=z^{\prime })}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^{\prime }$ and $Eq\text{-}\Sigma (z,z^{\prime })$:

$$(z\underset{S}{=}{z}^{\prime })\simeq Eq\text{-}\Sigma (z,z^{\prime })$$

Materials

Lecture Note

HoTTEST_Lecture_5.pdf

Record on Youtube