From: Anders Mörtberg <andersmortberg@gmail.com>
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