From 9e65b53eedee2db767d8183dd748d917c8b1828e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 13 Sep 2017 14:57:51 +0200 Subject: [PATCH] update lectures --- lectures/lecture1.ctt | 19 +++++++++++-------- lectures/lecture2.ctt | 36 +++++++++++++++++------------------- lectures/lecture3.ctt | 37 +++++++++++++++++-------------------- lectures/lecture4.ctt | 43 +++++++++++++++++++++++-------------------- 4 files changed, 68 insertions(+), 67 deletions(-) diff --git a/lectures/lecture1.ctt b/lectures/lecture1.ctt index 1a83540..9366c86 100644 --- a/lectures/lecture1.ctt +++ b/lectures/lecture1.ctt @@ -187,7 +187,7 @@ import nat However as this lecture will be self-contained no imports are necessary. Note that the import mechanism is very simple and recursive so that if I import nat then it will automatically import everything -nat depends on (like prelude). +nat depends on (like prelude.ctt). -} @@ -257,7 +257,7 @@ or : bool -> bool -> bool = split true -> true false -> false --- Note the _, this is name that is used for arguments that do not +-- Note the _, this is a name that is used for arguments that do not -- appear in the rest of the term (in particular one cannot refer to a -- variable called _). @@ -329,6 +329,7 @@ head (A : U) (a : A) : list A -> A = split -- Path types {- + We would like to prove: (b : bool) -> not (not b) = b But what is =? @@ -339,11 +340,12 @@ type A can then be thought of as a function II -> A. As II is not a type we introduce a Path type called PathP together with a binder, written , for path-abstraction and a path-application written p @ r where r is some element of the interval. + -} -- As in the Cubical Type Theory paper the type PathP (written Path in --- the paper!) is heterogeneous. The homogeneous Path type can be +-- the paper!) is heterogeneous. The homogeneous Path type can be -- defined by: Path (A : U) (a b : A) : U = PathP (<_> A) a b @@ -364,20 +366,21 @@ So the above goal can now be written: {- The simplest path possible is the reflexivity path: - a - a ------> a + a + a -------> a The intuition is that - u + a corresponds to - \(i : II) -> u + \(i : II) -> a So a is a function out of II that is constantly a. (But as II isn't a type we cannot write that as a lambda abstraction and we need a special syntax for it) + -} refl (A : U) (a : A) : Path A a a = a @@ -427,7 +430,7 @@ congbin (A B C : U) (f : A -> B -> C) (a a' : A) (b b' : B) (p : Path A a a') (q : Path B b b') : Path C (f a b) (f a' b') = undefined --- Note that undefined can be used at the top-level to introduce +-- Note that undefined can only be used at the top-level to introduce -- definitions without bodies, much like axioms in Coq. The reason -- that it only works at the top-level is that we need to know the -- type. We could have a version of undefined that is annotated with diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt index ba7a308..13e0570 100644 --- a/lectures/lecture2.ctt +++ b/lectures/lecture2.ctt @@ -17,7 +17,7 @@ module lecture2 where import lecture1 -{- +{- We have an involutive operation on II that corresponds to: @@ -30,14 +30,13 @@ for a point i in the real interval [0,1]. -- This can be used to prove symmetry of Path-equality: sym (A : U) (a b : A) (p : Path A a b) : Path A b a = p @ -i --- As this operation is an involution, so - - i = i. This gives new +-- This operation is an involution, so - - i = i. This gives new -- judgmental equalities, in particular sym A b a (sym A a b p) is -- judgmentally equality to p. This is not true in standard type --- theory where sym would be defined using by induction on p. This is --- useful for formalizing mathematics, for example we get the --- judgmental equality C^op^op = C for a category C that cannot be --- obtained in standard type theory with the standard definition of --- category. +-- theory where sym would be defined by induction on p. This is useful +-- for formalizing mathematics, for example we get the judgmental +-- equality C^op^op = C for a category C that cannot be obtained in +-- standard type theory with the standard definition of category. {- @@ -79,10 +78,10 @@ In particular the laws: - r \/ r = 1 do *not* hold (unless r is 0 or 1). This means that a De Morgan -algebra is *not* a Boolean algebra. The intuition for why this has to -be the case is that II should model the real interval [0,1] and there -we of course cannot have min(1-r,r) = 0 or max(1-r,r) = 1 for a point -r in [0,1] (unless r is 0 or 1). +algebra is *not* a Boolean algebra. The intuition for why this is the +case is that II should model the real interval [0,1] and there we of +course cannot have min(1-r,r) = 0 or max(1-r,r) = 1 for a point r in +[0,1] (unless r is 0 or 1). To test if two elements r and s in II are equal we first push the negations to the atoms and then compare their disjunctive normal forms @@ -93,7 +92,7 @@ example the following equations: 0 /\ r = 0 1 /\ r = r r /\ s = s /\ r - + and similarly for \/. @@ -178,14 +177,14 @@ inductive family: | refl : eq A a a. this means that eq comes with an induction principle: - + eq_rect : forall (A : Type) (a : A) (P : forall b : A, eq A a b -> Type), P a (refl A a) -> forall (b : A) (e : eq A a b), P b e This principle is commonly referred to simply as J and it says that in order to prove P for an equality e it suffices to do it in the case of refl. This can then be used to prove things like transitivity and all -the other properties one expects equality to have. +the other properties one expects equality to have. The approach taken in cubicaltt is very different to this approach to adding equality to type theory. Instead of adding equality as an @@ -232,15 +231,15 @@ i : II |- | | | | a ----------------> b - p @ i + p @ i The composition is the dashed line at the top of the square. The direction i goes left-to-right and j goes down-to-up. As we are constructing a Path from a to c we have i : II in the context already which is why we have to put p @ i as bottom (this is achieved by -writing the comp under a binder). The direction j that we are -doing the composition in is implicit, more about this below. +writing the comp after a path-abstraction). The direction j that we +are doing the composition in is implicit, more about this below. -} trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = @@ -285,7 +284,7 @@ ex (A : U) (a b : A) (p : Path A a b) : -- Hint: draw a cube with a square with these as sides as its missing -- top and compute it as a composition (the exercise about which -- squares one can make using /\, \/ and - will be very useful for --- this). +-- this). The solution can be found in the beginning of lecture3. -- We can use Path types and compositions to prove basic results about @@ -339,7 +338,6 @@ addCA (a b c : nat) : Path nat (add a (add b c)) (add b (add a c)) = undefined - {- That's all for this lecture. Next time we will do: diff --git a/lectures/lecture3.ctt b/lectures/lecture3.ctt index 584dc0d..812489f 100644 --- a/lectures/lecture3.ctt +++ b/lectures/lecture3.ctt @@ -18,7 +18,7 @@ import lecture2 -- Higher dimensional compositions -- Recall: the composition operation takes an open box in a type A and --- compute the lid. +-- computes the lid. -- Recall: compinv composes p with its inverse: -- compinv (A : U) (a b : A) (p : Path A a b) : Path A a a = @@ -46,7 +46,7 @@ type theory). If we substitute k for 0 in ex we get: - comp (<_> A) (p @ j /\ -0) + comp (<_> A) (p @ j /\ -0) [ (j = 0) -> a , (j = 1) -> p @ -i /\ -0 , (0 = 1) -> a ] @@ -54,7 +54,7 @@ If we substitute k for 0 in ex we get: The face 0=1 is absurd and disappears by the rules of the system. We hence get the following after simplifications: - comp (<_> A) (p @ j) + comp (<_> A) (p @ j) [ (j = 0) -> a , (j = 1) -> p @ -i ] @@ -62,8 +62,8 @@ Which is the same as compinv up to renaming of dimensions. We could also give the k = 0 side explicitly. Such a square is produced by an operation called "fill", this takes the same arguments -as comp and produces the interior of a cube with comp as its missing -side. +as comp and produces the interior of a cube with the comp as its +missing side. -} @@ -99,9 +99,8 @@ Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = undefined --- Exercise (very hard and not solved as far as I know, so let me know --- if someone manages to do it): define a cube type and construct a --- constant cube. +-- Exercise (VERY hard, for solutions see examples/constcubes.ctt): +-- define a cube type and construct a constant cube. @@ -110,7 +109,7 @@ constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = {- -Given P : Path U A B we want to define +Given P : Path U A B we want to define transport P : A -> B @@ -119,8 +118,7 @@ This is like a cast operation (compare with castmx of MathComp). -} -- We do this by a comp with an empty list of sides: -trans (A B : U) (p : Path U A B) (a : A) : B = - comp p a [] +trans (A B : U) (p : Path U A B) (a : A) : B = comp p a [] -- This uses that the composition operations are heterogeneous. So the -- lower line of the square can be in type A while the constructed @@ -132,8 +130,7 @@ gencomp (A B : U) (P : Path U A B) (a b : A) (c d : B) -- We can use transport to define: subst (A : U) (P : A -> U) (a b : A) - (p : Path A a b) (e : P a) : P b = - transport ( P (p @ i)) e + (p : Path A a b) (e : P a) : P b = transport ( P (p @ i)) e -- Note that we are using transport and not trans. The reason is that -- we don't have implicit arguments, so we have a built-in transport @@ -155,13 +152,13 @@ J (A : U) (a : A) (P : (b : A) -> Path A a b -> U) -- In Univalent Foundations/Homotopy Type Theory there is a very -- important stratification of types called h-levels -- ("homotopy-levels"). This is different from the normal universe --- level stratification of types and instead of size the types are +-- level stratification of types and instead of the size the types are -- categorized by the complexity of their equality. -- A type of h-level 1 is called a "proposition" (written "mere -- proposition" in the HoTT book or simply "h-proposition"). In such a -- type all elements are equal, so the only information that it --- carries is whether it is inhabited or not. +-- carries is whether it is inhabited or not. isProp (A : U) : U = (x y : A) -> Path A x y @@ -179,15 +176,15 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) : isProp ((x : A) -> B x) = rem where rem (f0 f1 : (x : A) -> B x) : - Path ((x : A) -> B x) f0 f1 = + Path ((x : A) -> B x) f0 f1 = \(x : A) -> h x (f0 x) (f1 x) @ i --- Exercise: Prove that if A is a proposition then it is a set. (hint: --- use a composition in a suitable cube) +-- Exercise: Prove that if A is a proposition then it is a set. +-- (hint: use a composition in a suitable cube) propSet (A : U) (h : isProp A) : isSet A = undefined --- Exercise: Prove that being a proposition is a proposition. (hint: --- use propSet and function extensionality for binary functions) +-- Exercise: Prove that being a proposition is a proposition. +-- (hint: use propSet and function extensionality for binary functions) propIsProp (A : U) : isProp (isProp A) = undefined diff --git a/lectures/lecture4.ctt b/lectures/lecture4.ctt index c0adc64..bfad4e3 100644 --- a/lectures/lecture4.ctt +++ b/lectures/lecture4.ctt @@ -22,7 +22,7 @@ import lecture3 fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Path B y (f x) --- A map is an equivalence +-- A map is an equivalence if its fibers are contractible isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y) @@ -39,9 +39,8 @@ idIsEquiv (A : U) : isEquiv A A (idfun A) = idEquiv (A : U) : equiv A A = (idfun A,idIsEquiv A) --- Compute the inverse of an equivalence -invEquiv (A B : U) (e : equiv A B) (y : B) : A = - (e.2 y).1.1 +-- We can compute the inverse of an equivalence +invEquiv (A B : U) (e : equiv A B) (y : B) : A = (e.2 y).1.1 -- Exercises (easy): the inverse is really the inverse retEq (A B : U) (e : equiv A B) (y : B) : Path B (e.1 (invEquiv A B e y)) y = undefined @@ -51,21 +50,24 @@ secEq (A B : U) (e : equiv A B) (x : A) : Path A (invEquiv A B e (e.1 x)) x = un -- (hint: use a composition) isPropIsContr (A : U) : isProp (isContr A) = undefined --- Being an equivalence is hence a proposition. Note that propositions --- in HoTT is different from Prop of Coq as we cannot erase them. If --- we erase the proof that a map is an equivalence we cannot invert --- it! +-- So the property of being an equivalence is a proposition. Note that +-- propositions in HoTT are different from Prop in Coq as we cannot +-- erase them. If we erase the proof that a map is an equivalence we +-- cannot invert it! + isPropIsEquiv (A B : U) (f : A -> B) : isProp (isEquiv A B f) = \(u0 u1 : isEquiv A B f) -> \(y : B) -> isPropIsContr (fiber A B f y) (u0 y) (u1 y) @ i --- The "isoToEquiv": any isomorphism is an equivalence +-- The "isoToEquiv" lemma: any isomorphism is an equivalence isoToEquiv (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f = - \(y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> - lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) + \(y : B) -> ((g y, s y @ -i),\(z : fiber A B f y) -> + lemIso A B f g s t y (g y) z.1 ( s y @ -i) z.2) where + -- Exercise: draw all of the squares in the proof of lemIso to see + -- why sq1 makes sense lemIso (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) @@ -128,9 +130,9 @@ equivalence of types: (A = B) ~ (A ~ B) -Glueing is a weaker form of this for producing non-trivial equalities +Glueing is a variation of this for producing non-trivial equalities from equivalences. In particular Glueing gives a map from equiv A B to -A = B. This weak form of univalence is useful for developing a lot of +A = B. This form of univalence is useful for developing a lot of examples. If e : equiv A B then we can get a path between A and B by @@ -142,14 +144,14 @@ This can be illustrated as: G A - - - - > B | | - e| | idEquiv B + e | | idEquiv B | | V V B --------> B B The sides of this square are equivalence while the bottom and top are -lines in direction i. +lines in direction i (left-to-right). The Glue type allows us to do two very hard things: prove that the universe is fibrant (i.e. define composition for U) and prove the @@ -290,10 +292,11 @@ cyril : eats bool = substEquiv eats bool bool notEquiv anders -- (hint: use fill with the empty system) uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 = undefined --- One would expect this computation rule to hold judgmentally, but it --- doesn't as the algorithm for computation in the universe adds some --- compositions with the empty system. --- Open problem: construct a type theory where this holds judgmentally. +-- One could imagine this computation rule to hold judgmentally, but +-- it doesn't as the algorithm for computation in the universe adds +-- some compositions with the empty system. +-- Open problem: construct a type theory where this holds +-- judgmentally. -- A further reduction of these axioms to even simpler axioms have -- recently been found by Ian Orton and Andrew Pitts: @@ -328,7 +331,7 @@ flipbeta (A B : U) (C : A -> B -> U) (a : A) (b : B) (c : C a b) : What I didn't talk about: - o Id types: we can define a type from Path for which the + o Id types: we can define a type from Path types for which the computation rule for J holds judgmentally. See examples/idtypes.ctt -- 2.34.1