Skip to content

My undergradate thesis on coinductive types in univalent type theory

License

Notifications You must be signed in to change notification settings

langston-barrett/reed-thesis

Repository files navigation

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: