diff --git a/thesis/main.bib b/thesis/main.bib index 0802035..95c9b33 100644 --- a/thesis/main.bib +++ b/thesis/main.bib @@ -320,4 +320,4 @@ The construction of the spectral sequences for cohomology is joint work with Jer editor = {Martin-Löf, Per}, date = {1975}, file = {An-Intuitionistic-Theory-of-Types-1972.pdf:/Users/michael/Zotero/storage/ICVD458G/An-Intuitionistic-Theory-of-Types-1972.pdf:application/pdf;Snapshot:/Users/michael/Zotero/storage/JLETE5WU/MARAIT-27.html:text/html}, -} +} \ No newline at end of file diff --git a/thesis/main.typ b/thesis/main.typ index 2f8dc74..4399900 100644 --- a/thesis/main.typ +++ b/thesis/main.typ @@ -11,11 +11,23 @@ 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. +This mode has been removed from Lean's later versions. + +Cubical offers benefits such as higher inductive types. == 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. +#TODO[Need to have this section at all?] + +One of the benefits of using a computationally-friendly system of proof is that we can use computer programs (known as proof assistants) to verify the correctness of our proofs. + +The primary proof assistant used in this work is Agda @agda_developers_agda_2025. Unlike many other popular general proof assistants, it doesn't use a tactic language to express the proofs. Instead, proofs are done by writing the proof term directly. + +Despite this, Agda is still friendly to the interactive theorem proving process, with the holes feature. +Inserting a question mark in place of a proof term adds a hole, which acts as a placeholder. +Type-checking continues assuming a proof term will be placed there later. +Additionally, the context at the hole can be queried with editor extensions, and refined with functions or constructors to produce more specific expressions but with holes where the arguments would be. +This allows for a top-down interactive theorem proving experience. == Cubical Agda @@ -25,6 +37,8 @@ The results in this paper have been formalized using Cubical Agda @vezzosi_cubic Martin-Löf type theory @martin-lof_intuitionistic_1975 +== Types as terms + == Types as propositions === Definitional vs. propositional equality @@ -40,9 +54,13 @@ Because of the computational nature of the theory, we distinguish these equaliti The unit type $unitType$ is the type with only a single inhabitant, $isTyp(tt, unitType)$. -=== Boolean type ($boolType$) +$ isTyp(ind_unitType, + product_isTyp(C, arro(unitType, typ)) + arro((isTyp(c, product_isTyp(x, unitType) C(x))), (isTyp(y, unitType)) , C(y))) $ -Similar to the unit type, the boolean type $boolType$ is the +=== Boolean type ($boolType$) + +Similar to the unit type, the boolean type $boolType$ is the type with only two inhabitants, which we will call $isTyp(bTrue, boolType)$ and $isTyp(bFalse, boolType)$. === Empty type ($emptyType$) @@ -52,14 +70,28 @@ A function $arro(A, emptyType)$ represents a proof of the negation of $A$, since 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)$]) $ +$ isTyp(ind_emptyType, product_isTyp(A, typ) arro(emptyType, A)) $ == Functions ($Pi$) == Pairs ($Sigma$) +== Type families + == Identity type ($propEqSym$) +#definition($ap$)[ + Function application preserve identities: + + $ + isTyp(ap, + product_(isTyp(#[$x, y$], A)) + product_(isTyp(f, arro(A, B))) + arro((propEq(x, y)), propEq(f(x), f(y))) + ) + $ +] + = Homotopy type theory == Equivalences @@ -114,6 +146,7 @@ We call this path $isTyp(loop, propEq(base, base))$. == Homotopy levels +#agdaCubicalLink("Cubical.Foundations.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. @@ -190,7 +223,12 @@ For any function $isTyp(f, arro(A, B))$, we can define the image of $f$, denoted == Grading -== Exactness +== Exactness + +#definition("Exactness")[ + Two functions $isTyp(f, arro(A, B))$ and $isTyp(g, arro(B, C))$ are *exact* if the image of $f$ is isomorphic to the kernel of $g$. + $ eqv(imOf(f), kerOf(g)) $ +] = Algebraic topology @@ -199,6 +237,8 @@ For any function $isTyp(f, arro(A, B))$, we can define the image of $f$, denoted == Eilenberg-MacLane spaces +Eilenberg-MacLane spaces were defined in homotopy type theory by #cite(, form: "author") @licata_eilenberg-maclane_2014. + #agdaCubicalLink("Cubical.Homotopy.EilenbergMacLane.Base") == Chain complexes @@ -219,7 +259,7 @@ Another way to word this is that for consecutive homomorphisms $d_n$ and $d_(n-1 = Spectral sequences -== Definition +== Spectra == Exact couples @@ -228,3 +268,7 @@ Another way to word this is that for consecutive homomorphisms $d_n$ and $d_(n-1 = Applications = Conclusion + + +- #TODO[References @agda_developers_agda_2025 should probably have more info] +- #TODO[References @martin-lof_intuitionistic_1975 is this correct?] \ No newline at end of file diff --git a/thesis/style.typ b/thesis/style.typ index fa30b5b..1e03d28 100644 --- a/thesis/style.typ +++ b/thesis/style.typ @@ -11,8 +11,8 @@ ) set par( // leading: 1.3em, - spacing: 2.4em, - first-line-indent: 1.8em, + // spacing: 2.4em, + // first-line-indent: 1.8em, justify: true, ) set heading( @@ -37,7 +37,7 @@ bibliography("main.bib", title: none) } -#let TODO(c) = [#text(fill: red)[*TODO:*] #c] +#let TODO(c) = [#text(fill: red)[*TODO:* #c]] #let agdaCubicalLink(s) = link("https://github.com/agda/cubical/blob/2f085f5675066c0e1708752587ae788c036ade87/" + s.split(".").join("/") + ".agda", raw(s)) // ctheorems @@ -55,7 +55,7 @@ // Notation #let emptyType = $bot$ -#let arro(a, b) = $#a op(arrow) #b$ +#let arro(..a) = $#a.pos().join($op(arrow)$)$ #let judgCtx(a) = $#a sans("ctx")$ #let isTyp(a, b) = $#a op(:) #b$ #let judgTyp(G, a, A) = $#G tack.r isTyp(#a, #A)$ @@ -65,7 +65,9 @@ #let defEq(a, b) = $#a := #b$ #let judgEqTyp(G, a, b, A) = $#G tack.r isTyp(#a equiv #b, #A)$ #let imOf(f) = $sans("Im")(#f)$ +#let kerOf(f) = $sans("Ker")(#f)$ #let ind = $sans("ind")$ +#let ap = $sans("ap")$ #let ua = $sans("ua")$ #let uaEqv = $sans("uaEqv")$ #let isEquiv = $sans("isEquiv")$ @@ -76,9 +78,11 @@ #let unitType = link()[$bb(1)$] #let tt = $sans("tt")$ -#let boolType = $bb(2)$ +#let boolType = link()[$bb(2)$] +#let bTrue = $sans("true")$ +#let bFalse = $sans("false")$ -#let S1 = $S^1$ +#let S1 = link()[$S^1$] #let base = $sans("base")$ #let loop = $sans("loop")$