stuff
This commit is contained in:
parent
afd32b8c67
commit
f30aa5751c
3 changed files with 62 additions and 14 deletions
|
|
@ -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},
|
||||
}
|
||||
}
|
||||
|
|
@ -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 <defVsProp>
|
||||
|
|
@ -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$) <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$) <identityType>
|
||||
|
||||
#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 <hlevels>
|
||||
|
||||
#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>
|
||||
== 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)) $
|
||||
] <exactness>
|
||||
|
||||
= 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(<licata_eilenberg-maclane_2014>, 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?]
|
||||
|
|
@ -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(<unitType>)[$bb(1)$]
|
||||
#let tt = $sans("tt")$
|
||||
|
||||
#let boolType = $bb(2)$
|
||||
#let boolType = link(<boolType>)[$bb(2)$]
|
||||
#let bTrue = $sans("true")$
|
||||
#let bFalse = $sans("false")$
|
||||
|
||||
#let S1 = $S^1$
|
||||
#let S1 = link(<circle>)[$S^1$]
|
||||
#let base = $sans("base")$
|
||||
#let loop = $sans("loop")$
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue