Homotopy type theory reading group at ANU, 2017
- Florrie will give us a crash course on type theory on Wednesday March 1.
- Max will explain to us what a fibration is, and what the path lifting property is (notes)
- What is the Curry-Howard isomorphism?
- What does the univalence axiom say?
- The Homotopy type theory book.
- A course on HoTT at Carnegie-Mellon, including video lectures.
- A series of introductory lectures at the IAS.
- We will put up notes from each week's discussion here. Anyone who has notes, either handwritten or TeX'd can contribute them.
- Week 1
- the email summarising the organisational meeting
- notes from Feb 22; a crash course in algebraic topology.
- Week 1
- To add content or files here, either
- send them to Scott,
- create a github account and ask Scott for commit access,
- create a github account and create a pull request, or
- you can use the online LaTeX editor at SageMathCloud, which we've hooked up to this repository. You'll need to create an account there and ask for access. Please remember to
git pushyour changes from the SageMath terminal.
- Let's try using the issues page here on github to keep track of questions we'd like to collectively think about. Scott has put up a first example, about the space of proofs that fg = gf in \pi_2(X). Please feel free to put anything up here, including basic questions asking for clarifications.
Homotopy type theorists like to use computer proof assistants (aka interactive theorem provers). The options are essentially
- Coq,
- Lean (installation hints), and
- Agda.
Coq is probably the best option for now. It is easy to install, but we need someone to also install the HoTT library, and then explain to all of us how to do that. Please send Scott an email (or even better a pull request here)!
(Agda is apparently less pleasant to use. Lean has some great features --- please talk to Scott if you're interested in learning Lean! --- but support for homotopy type theory has been abandoned.)