type-theory/thesis/main.typ

#import "./style.typ": *
#import "@preview/prooftrees:0.1.0": *
#import "@preview/cetz:0.3.1" as cetz: canvas, draw

#show: doc => template(
  title: "THESISge",
  doc,
)

= Introduction

This work extends Floris van Doorn's PhD dissertation @van_doorn_formalization_2018.
In that work, the mechanization of the proof was done in Lean 2's HoTT mode.
This mode has been removed from Lean's later versions, and as of the time of writing, Lean has no support for doing full homotopy type theory.

== Computer formalization

One of the benefits of using a computationally-friendly system of proof is that we can use computer programs to verify the correctness of our proofs.

== Cubical Agda

The results in this paper have been formalized using Cubical Agda @vezzosi_cubical_2021, an extension to the Agda proof assistant that implements cubical type theory.

= Martin-Löf type theory

Martin-Löf type theory @martin-lof_intuitionistic_1975

== Types as propositions

=== Definitional vs. propositional equality <defVsProp>

Because of the computational nature of the theory, we distinguish these equalities:

- $a$ and $b$ are *definitionally* (or judgmentally) equal, denoted $defEq(a, b)$, if they reduce to exactly the same term through reduction rules
- $a$ and $b$ are *propositionally* equal, denoted $propEq(a, b)$, if there exists any term in the #link(<identityType>)[identity type] $propEq(a, b)$ (will be introduced in a later section).

== Basic types

=== Unit type ($unitType$) <unitType>

The unit type $unitType$ is the type with only a single inhabitant, $isTyp(tt, unitType)$.

=== Boolean type ($boolType$)

Similar to the unit type, the boolean type $boolType$ is the 

=== Empty type ($emptyType$)

The empty type $emptyType$ is the type with no inhabitants.
Logically, this corresponds to falsehood.
A function $arro(A, emptyType)$ represents a proof of the negation of $A$, since as a consequence $A$ implies false.

The empty type eliminator is hence the principle of #link("https://en.wikipedia.org/wiki/Principle_of_explosion")[_ex falso quodlibet_]:

$ isTyp(ind_emptyType, #[$forall (isTyp(A, typ)), arro(emptyType, A)$]) $

== Functions ($Pi$)

== Pairs ($Sigma$)

== Identity type ($propEqSym$) <identityType>

= Homotopy type theory

== Equivalences

== Univalence axiom <univalence>

One of the key observations of homotopy type theory is that the equivalence type $eqv(A, B)$ internally reflects an underlying equality between $A$ and $B$.
The *univalence axiom* realizes this idea by giving a way to "upgrade" our equivalence into a propositional equality:

#axiom("Univalence")[
  $ isTyp(ua, arro((eqv(A, B)), (propEq(A, B)))) $
] <univalenceAxiom>

#axiom("Univalence equivalence")[
  $ isTyp(uaEqv, isEquiv(ua)) $
] <univalenceEqvAxiom>

This property is not expressible with book HoTT.

== Pointed types

== Higher inductive types

=== Circle ($S1$) <circle>

The circle is a simple yet rich space that demonstrates a lot of interesting properties.
Analytically, the circle could be defined as the set of points $isTyp((x, y), RR times RR)$ such that:

$ x^2 + y^2 = 1 $

#align(center, canvas({
  import draw: *
  grid((-3, -3), (3, 3), stroke: luma(90%))
  circle((0, 0), radius: 2)
}))

In synthetic homotopy theory, we distill the circle to its only distinguishing property: that it cannot be contracted into a point, due to the hole in the middle.
We call this type $S1$, where the 1 indicates that it is a 1-dimensional sphere.

For some arbitrary choice of base point, denoted $isTyp(base, S1)$, we can imagine the circle as a path going from the base to itself.
We call this path $isTyp(loop, propEq(base, base))$.

#align(center, canvas({
  import draw: *
  circle((0, 2), radius: 2)
  content((0, 4.5), $loop$)
  circle((0, 0), radius: 0.05, stroke: (paint: red, thickness: 3pt))
  content((0, 0.5), text($base$, stroke: red))
}))

=== Suspensions ($Sigma$)

== Homotopy levels <hlevels>

#footnote[
  Homotopy levels are also known under a different name, homotopy $n$-types.
  Although the name is the same, the numbers are offset by 2, such that sets are $0$-types, mere props are $(-1)$-types, and contractible types are $(-2)$-types.
  This may introduce a lot of confusion, so for the purposes of this paper I will stick to homotopy levels since it makes more sense to begin induction on homotopy levels from 0.
]

= Cubical type theory <cubicaltt>

Cubical type theory @cohen_cubical_2016

== Cubical interval

== $sans(#[hcomp])$ and $sans(#[hfill])$

== $sans(#[Glue])$ and $sans(#[glue])$

= Algebra

== Groups

#definition("Group")[
A group ($G$, $dot$) is a type ($G$) equipped with a binary operation ($dot$) that satisfies a few axioms.

- Associativity: for any #isTyp($a, b, c$, $G$), 
- Identity: #TODO[identity]
- Inverse: #TODO[inverse]
] <group>

The mechanized definition of this can be found in #agdaCubicalLink("Cubical.Algebra.Group.Base").

#definition("Abelian group")[] <abelianGroup>

== Images and kernels

For any function $isTyp(f, arro(A, B))$, we can define the image of $f$, denoted $imOf(f)$ to be all of the elements in $B$ such that are mapped to from $A$. This differs from the _codomain_ of $f$, which is the entire set $B$ including points that cannot be mapped to.

#definition("Image")[
  For types $A$ and $B$, and a function $isTyp(f, arro(A, B))$, define:
  $ defEq(imOf(f), sum_(isTyp(b, B)) (sum_(isTyp(a, A)) propEq(f(a), b))) $

  #TODO[This needs to be mere existence, but I need to figure out how to write that]
] <image>

#align(center, canvas({
  import draw: *
  content((0, 2.5), $A$)
  circle((0, 0), radius: (1, 2))
  content((5, 2.5), $B$)
  circle((5, 0), radius: (1, 2))
  circle((5, 0), radius: (0.75, 1.25), stroke: none, fill: luma(80%))

  circle((0, 1.5), stroke: 3pt, radius: 0.05)
  circle((0, 0.75), stroke: 3pt, radius: 0.05)
  circle((0, 0), stroke: 3pt, radius: 0.05)
  circle((0, -0.75), stroke: 3pt, radius: 0.05)
  circle((0, -1.5), stroke: 3pt, radius: 0.05)
  circle((5, 1.5), stroke: 3pt, radius: 0.05)
  circle((5, 0.75), stroke: 3pt, radius: 0.05)
  circle((5, 0), stroke: 3pt, radius: 0.05)
  circle((5, -0.75), stroke: 3pt, radius: 0.05)
  circle((5, -1.5), stroke: 3pt, radius: 0.05)

  bezier((0, 1.5), (5, 0.75), (3, 1.5), (2, 0.75), mark: (end: ">"))
  line((0, 0), (5, 0), mark: (end: ">"))
  line((0, 0.75), (5, 0.75), mark: (end: ">"))
  bezier((0, -0.75), (5, 0), (3, -0.75), (2, 0), mark: (end: ">"))
  bezier((0, -1.5), (5, -0.75), (3, -1.5), (2, -0.75), mark: (end: ">"))
  
  line((6.25, 0), (5.5, 0), stroke: luma(80%))
  content((7, 0), text($imOf(f)$, fill: luma(50%)))
}))

== Modules

== Grading

== Exactness <exactness>

= Algebraic topology

== Basic spaces


== Eilenberg-MacLane spaces

#agdaCubicalLink("Cubical.Homotopy.EilenbergMacLane.Base")

== Chain complexes

#definition("Chain complex")[
  A *chain complex* is a sequence of #link(<abelianGroup>)[abelian groups] $isTyp(C_n, AbGroup)$ ("chains") along with homomorphisms between consecutive groups $isTyp(d_n, hom(C_n, C_(n-1)))$ ("boundaries"), such that for any $n$, the proposition $propEq(homComp(d_(n-1), d_n), 0_(C_(n-2)))$ is inhabited.
] <chainComplex>

Another way to word this is that for consecutive homomorphisms $d_n$ and $d_(n-1)$, the #link(<image>)[image] of $d_n$ is a subgroup of the kernel of $d_(n-1)$.

#definition("Exact sequence")[
  An *exact sequence* is a chain complex where all consecutive homomorphisms are #link(<exactness>)[exact].
] <exactSequence>

== Homology and cohomology

== Long exact sequence of homotopy groups

= Spectral sequences

== Definition

== Exact couples

== Serre spectral sequence

= Applications

= Conclusion