5
Cubical Type Theory: lectures
source link: https://github.com/mortberg/cubicaltt/tree/master/lectures
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Cubical Type Theory: lectures
This folder contains four lectures given by Anders at Inria Sophia Antipolis in May-June 2017. The lectures cover the main features of the system and doesn't assume any prior knowledge of homotopy type theory or univalent foundations. Only basic familiarity with type theory and proof assistants based on type theory (e.g. Coq or Agda) is assumed.
The contents of the lectures are:
lecture1.ctt
- Basic features of the base type theory
- A little bit of Path types (Path abstraction and application)
lecture2.ctt
- More on Path types (symmetry and connections)
- Compositions
lecture3.ctt
- Higher dimensional compositions
- Transport and J for Path types
- H-levels (contractible types, propositions, sets, groupoids...)
lecture4.ctt
- Equivalences
- Glue types
- Proofs of the univalence axiom
The lectures hence give a hands-on introduction covering sections 2-7 of the paper.
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK