reed-thesis
reed-thesis copied to clipboard
My undergradate thesis on coinductive types in univalent type theory
Undergraduate Thesis
This repo holds my undergraduate thesis (completed in May 2018), which focused on adding "internal" M-types to the UniMath library. See this paper for details: "Non-wellfounded Trees in Homotopy Type Theory".
Directory Structure
-
archive/
contains things I thought I would need, but didn't. -
coq/
contains formalized mathematics-
coq/Exercises
contains solutions to exercises in the HoTT book.
-
-
exercises/
contains informal solutions to exercises in various texts-
exercises/hott*
: From the HoTT book (scanned from handwritten versions) -
exercises/hatcher*
: From Hatcher's Algebraic Topology -
exercises/awodey*
: From Awodey's Category Theory
-
-
notes/
contains LaTeX notes on various subjects at the level of detail I required at the time (no attempt to be comprehensive nor expository has been made).-
notes/hott-figures
is a bunch of Tikz drawings corresponding to lemmas and theorems in the HoTT book
-
-
tex-preamble/
is a collection of LaTeX files that are useful to\input{}
at the beginning of documents.
Work elsewhere
For work I've done related to my thesis that isn't hosted here, see my work on: