From: Anders Mörtberg Date: Wed, 14 Jun 2017 12:45:20 +0000 (+0200) Subject: add README for the lectures X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=564e0f7543a549845703ae2af558fa12734b3d0d;p=cubicaltt.git add README for the lectures --- diff --git a/lectures/README.md b/lectures/README.md new file mode 100644 index 0000000..871d1af --- /dev/null +++ b/lectures/README.md @@ -0,0 +1,25 @@ +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: + +1. Basic features of the base type theory and little bit of Path types + (Path abstraction and application). + +2. More on Path types (symmetry and connections) and compositions. + +3. Higher dimensional compositions, transport and J for Path types, + fill and H-levels (contractible types, propositions, sets, + groupoids...). + +4. Equivalences, Glue types and proofs of the univalence axiom. + +The lectures hence gives a hands-on introduction covering sections 2-7 +of the [paper](https://arxiv.org/abs/1611.02108). \ No newline at end of file