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:

• siddharthist/write-yourself-a-scheme-in-agda
• HoTT/HoTT
• UniMath/UniMath
• HoTT/book