# Homotopy Type Theory

## Homotopy

$f,g:X→Y,H:X×[0,1]→Y→H(x,0)=f(x),H(x,1)=g(x).$$p:x=Ay.$$p,q:x=Ay.$

2-path/homotopy

$r:p=x=Ayq.$

## Types Are Higher Groupoids

### inverse : =-symmetry

First proof.

$λ(A).λ(a).λ(b).λ(p).ind=A(λ(a).λ(b).λ(p).(a=b),λ(a).refla,a,b,p):(A:𝒰)→(a,b:A)→(a=b)→(b=a).$

### concatenate/compose : =-transitivity

$λ(A).λ(a).λ(b).λ(c).λ(p).λ(q).ind=A(λ(a).λ(b).λ(p).λ(c).λ(q).(a=c),ind=A(λ(a).λ(c).λ(q).(a=c),refla)):(A:𝒰)→(a,b,c:A)→(a=b)→(b=c)→(a=c).$

### Lemma

$A:𝒰x,y,z,w:Ap:x=y,q:y=z,r:z=w1. p=p⋅↺y, p=↺x⋅p. 2. p−1⋅p=↺y, p⋅p−1=↺x. 3. (p−1)^[−1]=p. 4. p⋅(q⋅r)=(p⋅q)⋅r.$

### Eckmann–Hilton

$α,β:Ω2(A,a)→α⋅β=β⋅α.$

### Pointed type

$(A,a):𝒰•≡(A:𝒰,A).$

### Loop space

$Ω(A,a)≡(a=Aa,↺a).$$Ω0(A,a)≡(A,a)$$Ωn+1(A,a)≡Ωn(Ω(A,a)).$$Ω2(A,a)≡Ω(Ω(A,a))≡Ω((a=Aa,↺a)).≡Ω(a=Aa,↺a)≡(↺a=a=Aa↺a,↺↺a).$

## Functions Are Functors

### Lemma

$f:A→B,x,y:A,apf:(x=Ay)→(f(x)=Bf(y)).$$D≡(x,y,p)↦f(x)=f(y),D:x,y:A→(x=y)→𝒰,d≡x↦↺f(x),d:x:A→D(x,x,↺x),apf:x,y:A→(x=y)→(f(x)=f(y))(by path induction).x:A→ap_f(↺x)≡↺_[f(x)] (by computation rule).$



## Dependent Types are Fibrations

### Transport

#### Transport

$a:A→P:𝒰→p:x=Ay→p*≡transportP(p,–)≡ind=A(D,d,x,y,p):P(x)→P(y),D≡x,y:A,p:x=Ay→P(x)=P(y),d≡x:A→idP(x),ind=A(D,d,x,y,p):P(x)→P(y)forp:x=y.$

Type theory: P respects equality: x=yP(x)P(y). Topology: path lifting in a fibration P with base space A, with P(x) being the fibre over x and with Σ_[x:A] P being the total space of the fibration, with the first projection Σ_[x:A] P(x)A.

#### Path Lifting Property

$A:𝒰→a:A→P:𝒰,a_0:A,p_0:P→p:x=Ay→lift(p0,p):(x,p0)=(y,p*(p0)),pr1(lift(p0,p))=p.$

#### Dependent map

$a:A→p:P→p:x=Ay→p*(f(x))=P(y)f(y).D≡x,y,p→,(↺x)_*(f(x))≡f(x),d≡x:A→↺f(x),$

#### Lemma

$(f(x)=f(y))→(p*(f(x))=f(y)),(p*(f(x))=f(y))→(f(x)=f(y)).$



#### Lemma

$a:A→P:U,p:x =A y,q:y =A z, p_0:P(x) →q_*(p*(p_0))=(p q)_*(p_0).$

#### Lemma

$a:A→b:B,b:B→ P:U,p:x =Ay, p_0:P(b(x)) →$

#### Lemma

$a:A→P,Q:U, (a:A→P→Q), p:x =Ay, p_0:P(b(x)) →$

## Homotopies and Equivalences

### Homotopies

Natural transformations.

$f,g:(a:A)→B(a)(f∼g)≡(a:A)→(f(a)=g(a)).$

### Equivalence Relation

$reflexivity∼:(f:(a:A)→B(a))→(f∼f).symmetry∼:(f,g:(a:A)→B(a))→(f∼g)→(g∼f).transitivity∼:(f,g,h:(a:A)→B(a))→(f∼g)→(g∼h)→(f∼h).$

#### Lemma

$(a:A)→f,g:B→H:f∼g,p:x=Ay→H(x)⋅g(p)=f(p)⋅H(y).$

#### Corollary

$(a:A)→f:A→H:f→idA→(a:A)→H(f(x))=f(H(x)).$

### Quasi-Inverse

Homotopy equivalence, 'equivalence of (higher) groupoids'.

$(f:A→B),qinv≡(g:B→A)×(fg∼idB)×(gf∼idA).$

#### Example

$(idA,↺y,↺x):qinv(idA).$





### Equivalence

1. $\left(a:A\right)\to f:B\to \mathrm{qinv}\left(f\right)\to \mathrm{is-equiv}\left(f\right).$
2. $\left(a:A\right)\to f:B\to \mathrm{is-equiv}\left(f\right)\to \mathrm{qinv}\left(f\right).$
3. ${e}_{1},{e}_{2}:\mathrm{is-equiv}\left(f\right)\to {e}_{1}={e}_{2}$.
$g∼βh◦f◦g∼αh,A≃B≡(f:A→B),is-equiv(f).$

#### Lemma

1. $A\simeq A.$
2. $A\simeq B\to B\simeq A.$
3. $A\simeq B\to B\simeq C\to A\simeq C.$

## ×

### Theorem

$(x=A×By)→(pr1(x)=Apr1(y))×(pr3(x)=Bpr3(y)).$













## Dependent ×

### Theorem

$w,w':(a:A,P)→(w=w')≃p:w0=w'0,p*(w1)=w'1.$

### Propositional Uniqueness Principle

$z:(a:A)×P(a)→z=(pr1(z),pr3(z)).$

#### Theorem

$A:𝒰,a:A→P:𝒰,(a:A,p:P)→Q:𝒰0→a:A→(p:P,Q).$$p:x=Au,(u,z):(p:P,Q)0→p*(u,z)=(p*(u),pair=(p,↺p*(u))*(z)).$

## 𝟏

#### Theorem

$x,u:𝟏→(x=u)≃𝟏.$$(x=u)→𝟏,relf⋆:x=u,𝟏→(x=u),$

## Π-Types and the Function Extensionality Axiom

### Function Extensionality

$a:A→B:𝒰→f,g:B→(f=g)≃(a:A→f(a)=B(a)g(a)).$$happly:(f=Bg)→(a:A→f(a)=B(a)g(x)),_:is-equiv(happly).$$funext:(a:A→f=Bg)→f=Bg.$

### Lemma

$x:X→A,B:𝒰,p:x=Xy,(a:A→f:B),(a:A→g:B)→(p*(f)=g)≃(a:A→p*(f)=g(p*)).$

### Lemma

$x:X,A:𝒰,a:A,B:𝒰,b:B,p:x=Xy,(x:X→a:A,f:B),(y:X→a:A,g:B)→(p*(f)=g)≃(a:A→).$

## Universes and the Univalence Axiom

### Lemma

$A,B:𝒰→idtoeqv:(A=B)→(A≃B).$

### Univalence

$(A=B)≃(A≃B).$

### Introduction rule for =𝒰

$ua:(A≃B)→(A=B).$

### Elimination Rule for =𝒰

$idtoeqv≡transportX→X:(A=B)→(A≃B).$

### Propositional Computation Rule for =𝒰

$transportX→X(ua(f),x)=f(x).$

### Propositional Uniqueness Rule for =𝒰

$p=ua(transport(p)).$
• ${↺}_{A}=\mathrm{ua}\left({\mathrm{id}}_{A}\right)$.
• $\mathrm{ua}\left(f\right)\cdot \mathrm{ua}\left(g\right)=\mathrm{ua}\left(g◦f\right)$.
• ${\mathrm{ua}\left(f\right)}^{-1}=\mathrm{ua}\left({f}^{-1}\right)$.

## =

### Theorem

$(a=Aa')→(b(a)=Bb(a'))$

## +

$(inj1(a)=inj1(a'))≃(a=a')(inj2(b)=inj2(b'))≃(b=b')(inj1(a)=inj2(b))≃𝟎code(inj1(a))≡(a0=a),code(inj2(b))≡𝟎.$

## ℕ

$code:ℕ→ℕ→𝒰,$$code(0,0)≡𝟏,$$code(succ(m),0)≡𝟎,$$code(0,succ(n))≡𝟎,$$code(succ(m),succ(n))≡code(m,n).$$r:n:ℕ→code(n,n),r(0)≡⋆,r(succ(n))≡r(n).$

### Theorem

$(m,n:ℕ)→(m=n)≃code(m,n).$$encode:(m,n):ℕ→(m=n)→code(m,n),$$encode(m,n,p)≡transportcode(m,–)(p,r(m)),$$decode:m,n:ℕ→code(m,n)→(m=n)(by double induction on m, n).$$code(succ(m),succ(n))≡code(m,n)→decode(m,n)(m=n)→apsuccsucc(m)=succ(n).$

## Equality of Structures

### Semigroup structures

$(m:A→A→A,x,y,z:A)→m(x,m(y,z))=m(m(x,y),z)$

## Universal Properties

### ×

#### Mapping in, non-dependent.

$(C→A×B)≃(C→A)×(C→B).$$f:X→A×Bpr1f:X→Apr3f:X→B(pr1f,pr3f):(X→A)×(X→B)×-introductionλf.(pr1f,pr3f):(X→A×B)→((X→A)×(X→B))→-introduction.$$a:X→A,b:X→B(a,b):(X→A)×(X→B)×-introductionλ(a,b).λx.(ax,bx):((X→A)×(X→B))→(X→A×B) →-introduction.$$ind(X→A)×(X→B)(C,c,(a,b))≡c(a)(b),ind(X→A)×(X→B):(C:((X→A)×(X→B))→𝒰)→((a:X→A)→(b:X→B)→C((a,b)))→(x:(X→A)×(X→B))→C(x).λx.((pr1fx,pr3fx))≡f,(λx.a(x),λx.b(x))≡(a,b).$

#### Mapping in, dependent.

$((x:X)→(A(x)×B(x)))→((x:X)→A(x))×((x:X)→B(x))$

Mapping out, non-dependent.

$((A×B)→C)≃(A→(B→C)).$

Mapping out, dependent.

$((w:A×B)→C(w))≃((a:A)→((b:B)→C(a,b))).$

### Dependent ×

#### Mapping in, dependent.

Axiom of choice.

$(x:X)→((a:A(x))×B(x)(a))≃(a:(x:X)→A(x))×((x:X)→B(x)(a(x))).$

#### Mapping out, dependent.

$((b:(a:A)×B(a))→C(b))≃((a:A)→((b:B(a))→C(a,b))).$

### +

$(A+B→C)≃(A→C)×(B→C).$

### 𝟎

#### ?

$((x:A)→(p:a=x)B(x,p))≃B(a,refla).f:A→Cg:B→CA×CB≡(a:A)×(b:B)(f(a)=g(b)).$

## 𝕊1

'Circle'.

### Formation Rule

$𝕊1:𝒰.$

### Introduction Rules

$base:𝕊1,loop:base=𝕊1base$



## 𝕀

'Interval'.

### Formation Rule

$𝕀:𝒰.$

### Introduction Rules

$0𝕀:𝕀,1𝕀:𝕀,seg:0𝕀=𝕀1𝕀$

### Function Extensionality

#### Lemma

$is-truncated−2(𝕀).$

#### Lemma

$(f,g:A→B)→(a:A→f(a)=g(a))→(f=A→Bg).$

### Circle and Sphere

#### Lemma

$loop≠↺base.$

#### Lemma

$f:(x:𝕊1)→(x=x),f≠x↦↺x.$

#### Corollary

$𝕊1:𝒰,is-truncated_1(𝒰)→𝟎.$

#### Lemma

$f:A→B,x,y:A,p,q:x=y,r:p=q→apf2(↺p)≡↺f(p).$

#### Lemma

$P:A→𝒰,x,y:A,p,q:x=y,r:p=q,u:P(x)→transport2(r,u):p*(u)=q*(u).$

### Suspension

• $N:\mathrm{\Sigma A}$,
• $S:\mathrm{\Sigma A}$,
• $\mathrm{merid}:A\to \left(N{=}_{\mathrm{\Sigma A}}S\right)$.

#### Lemma

$Σ𝟐≃S_1 .$

#### Lemma

$A,(B,b0):U→Map*(A+,B)≃(A→B).$

#### Lemma

$(A,a0),(B,b0):𝒰→Map*(ΣA,B)≃Map*(A,ΩB).$

### Truncation

#### Lemma

$(||A∪^CB||0→E)≃coconeD(E).$

### Algebra

#### Theorem

$(F(A)→GroupG)≃(A→G).$

### Monoid

$is-0-type(G)→$
• $\left(x,y\right)↦xy:G×G\to G$,
• $1:G$,
• $\left(x:G\right)\to \left(x1=x\right)×\left(1x=x\right)$,
• $\left(x,y,z:G\right)\to x\left(yz\right)=\left(xy\right)z$.

### Group

• $x↦{x}^{-1}:G\to G$,
• $\left(x:G\right)\to \left(x{x}^{-1}=1\right)×\left({x}^{-1}x=1\right)$.

### General Syntax

#### Example

$f:(X:𝒰)→X→X,fX≡idX,f2:2→2.a,b:K,σ:fK(a)→fK(b).$

### Quotient

$(a,b:A)×R(a,b)⇉A.$
• $q:A\to A/R$,
• $\left(a,b:A\right)\to R\left(a,b\right)\to \left(q\left(a\right)=q\left(b\right)\right)$,
• $\left(x,y:A/R\right)\to \left(r,s:x=y\right)\to \left(r=s\right)$.

### Integers

$(a,b)∼(c,d)≡(a+d=b+c)→Z≡(N×N)/∼.$

#### Lemma

$idempotentr:A→A,x,y:A→(r(x)=r(y))≃(x∼y)→(A/∼)≡((x:A)×r(x)=x),q:A→(A/∼),((A/∼)→B)≃((g:A→B)×x,y:A→(x∼y)→(g(x)=g(y))).$

#### Lemma

$P:Z→U,$
• ${d}^{0}:P\left(0\right)$,
• $d_+:\left(n:ℕ\right)\to P\left(n\right)\to P\left(\mathrm{succ}\left(n\right)\right)$,
• $d_-:\left(n:ℕ\right)\to P\left(-n\right)\to P\left(-\mathrm{succ}\left(n\right)\right)$
$→f:z:Z→P(z),$
• $f\left(0\right)={d}_{0}$,
• $\left(n:ℕ\right)\to f\left(\mathrm{succ}\left(n\right)\right)=d_+\left(n,f\left(n\right)\right),$
• $\left(n:ℕ\right)\to f\left(-\mathrm{succ}\left(n\right)\right)=d_-\left(n,f\left(-n\right)\right).$

#### Corollary

$p:a=a,n↦pn:(n:ℤ)→(a=a),p0≡↺a,pn+1≡pnpfor0≤n,pn−1≡pnp−1forn≤0.$