# A Functional Programmer’s Guide to Homotopy Type Theory (HoTT)

Since April 2019 until I re-visit this Youtube video on 12 August 2019, I can now totally understand his speech after a pause of 4 months by viewing other related Youtube (below prerequisite) videos on Category Theory, Type Theory, Homotopy Type Theory.

That is the technique of self-study:

1. First go through the whole video,
2. Don’t understand? view other related simpler videos.
3. Repeat 1.

Prerequisite knowledge:

1. Homotopy
2. Type Theory
3. Homotopy Type Theory
4. Bijection = Isomorphism
5. Functional Programming in Category Theory Concept: Monad & Applicative  Two Key Takeaway Points:

1. In the Homotopy “Space” : Programs are points in the space, Paths are Types.
2. “Univalence Axiom” : Paths Induce Bijection, vice versa.        # Morphism Summary Chart

The more common morphisms are:

1. Homomorphism (Similarity between 2 different structures) 同态
Analogy: Similar triangles of 2 different triangles.

2. Isomorphism (Sameness between 2 different structures) 同构
Analogy: Congruence of 2 different triangles

Example: 2 objects are identical up to an isomorphism.

3. Endomorphism (Similar structure of self) = {Self + Homomorphism} 自同态
Analogy: A triangle and its image in a magnifying glass.

4. Automorphism (Sameness structure of self) = {Self + Isomorphism} 自同构
Analogy: A triangle and its image in a mirror; or
A triangle and its rotated (clock-wise or anti-clock-wise), or reflected (flip-over) self. 5. Monomorphism 单同态 = Injective + Homomorphism 6. Epimorphism 满同态 = Surjective + Homomorphism

# Proofs of Isomorphism

Two ways to prove f is Isomorphism:

1) By definition:
f is Homomorphism + f bijective (= surjective + injective)

2) f is homomorphism + f has inverse map $f^{-1}$

Note: The kernel of a map (homomorphism) is the Ideal of a ring.

Two ways to construct an Ideal:
1) use Kernel of the map
2) by the generators of the map.

Two ways to prove Injective:

1) By definition of Injective Map:
f(x) = f(y)
prove x= y

2) By Kernel of homomorphism:
If f is homomorphism $f: A \mapsto B$
Prove Ker f = {0}

Note: Lemma: $\text{f is injective} \iff Ker f = {0}$

Proof Isomorphism 4 Steps:
1. Define function f：S -> T
Dom(f) = S
2. Show f is 1 to 1(injective)
3. Show f is onto (surjective)
4. Show f(a*b) = f(a). f(b)

Example:
Let T = even Z
Prove (Z,+) and (T,+) isomorphic
Proof:
1. Define f: Z -> T by
f(a) = 2a
2. f(a)=f(b)
2a=2b
a=b
=> f injective

3. Suppose b is any even Z
then a= b/2 ∈ Z and
f(a)=f(b/2)=2(b/2)=b
=> f onto

4. f(a+b) =2(a+b) =2a+2b =f(a)+f(b)
Hence (Z,+) ≌ (T,+)

Isomorphism (≌)
1. To prove G not isomorphic to H:
=> Prove |G| ≠ |H|

2. Isomorphism class = Equivalence Class
B’cos “≌” is an Equivalence relation.

3. Properties of Isomorphism (≌):
i) match e $\phi(e) = e'$
ii) match inverse $\phi (g^{-1} )= (\phi (g))^{-1}$

iii) match power $\phi(g^{k})= (\phi(g))^{k}$

# Visualize Isomorphism

This is the Chinese graphical way to visualize Abstract Algebra:

Third Theorem of Isomorphism Second Theorem of Isomorphism

Group G with normal subgroup N,
H subgroup of G (H ≤ G ).
=>
1.(H ∩ N) normal subgroup of H;
2. HN/N ≌ H /(H ∩ N) # Isomorphism = Congruence, Homomorphism = Similar

New Math <=> Old Math

1. Isomorphism of Groups (or any structures)
<=> Congruence Triangles
(Faithful Representation)

2. Homomorphism of Groups (or any structures)
<=> Similar Triangles
(unFaithful Representation)