From 564e0f7543a549845703ae2af558fa12734b3d0d Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 14 Jun 2017 14:45:20 +0200 Subject: [PATCH] add README for the lectures --- lectures/README.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 lectures/README.md 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 -- 2.34.1