From e9370f94b96fd55550651d8866e3dc621dd671ce Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 20 May 2017 11:31:04 +0200 Subject: [PATCH] Add lecture 2 --- lectures/lecture2.ctt | 327 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 327 insertions(+) create mode 100644 lectures/lecture2.ctt diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt new file mode 100644 index 0000000..e15271d --- /dev/null +++ b/lectures/lecture2.ctt @@ -0,0 +1,327 @@ +{- + Lecture 2 on cubicaltt (Cubical Type Theory) +-------------------------------------------------------------------------- + Anders Mörtberg + +Contents: + o Path types part 2 + o Compositions + +Recall: + <- Path abstraction + p @ i <- Path application + refl A a := a + +-} +module lecture2 where + +import lecture1 + +{- + +We have an operation on II that corresponds to: + + -i "=" 1 - i + +for 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 + +-- Note that 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 J/eq_rect. This is useful +-- for formalizing mathematics, for example we get the judgmental +-- equality C^op^op = C for a category C. + + +{- + +We call the elements of the interval II by +names/directions/dimensions/colors and typically use i, j, k to denote +them: + +dir := i, j, k... + +The elements of the interval II are generated by the following grammar: + +r,s := 0 + | 1 + | dir + | - r + | r /\ s + | r \/ s + +So far we have seen the first four cases, the latter two are called +"connections". The intuition is that i /\ j corresponds to the min of +i and j, and that i \/ j corresponds to the max of i and j. + +II forms a bounded distributive lattice with 0 as bottom and 1 as top +together with /\ as meet and \/ as join. The - operation is a De +Morgan involution: + + - (r /\ s) = -r \/ -s + - (r \/ s) = -r /\ -s + - - r = r + +This kind of structure is called a De Morgan algebra: + + https://en.wikipedia.org/wiki/De_Morgan_algebra + +In particular the laws: + + - r /\ r = 0 + - 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) for any point r +in II. + +To test if two elements r and s in II are equal first push the +negations to the atoms and then compare their disjunctive normal forms +(in other words the equality is the one from the free bounded +distributive lattice on formal generators i and -i). This gives us the +following equations: + + 0 /\ r = 0 + 1 /\ r = r + r /\ s = s /\ r + +and similarily for \/. + + +Connections are very useful for constructing special squares, which is +something we want to do all the time when reasoning about higher +dimensional equalities. If p : Path A a b then: + + + p + a -----------------> b + ^ ^ + | | + | | + a | p @ i /\ j | p + | | + | | + | | + a -----------------> a + a + +Here i corresponds to the left-to-right dimension and j corresponds to +the down-to-up dimension. To compute the left and right end-point just +plug in i=0 and i=1 into the term inside the square: + + p @ 0 /\ j = p @ 0 = a (recall that p is a path from a to b) + p @ 1 /\ j = p @ j = p (note that we have eta for Path-types) + + +Applying p to a disjunction gives: + + + b + b -----------------> b + ^ ^ + | | + | | + p | p @ i \/ j | b + | | + | | + | | + a -----------------> b + p + + +Exercise: draw the squares for + + p @ -i /\ j + p @ -i /\ -j + p @ -i \/ j + p @ -i \/ -j + +-} + + +-- The ability to construct there squares makes it easy to prove some +-- basic results about Path-types. For instance we can prove +-- "contractibility of singletons": +singl (A : U) (a : A) : U = (x : A) * Path A a x + +contrSingl (A : U) (a b : A) (p : Path A a b) : + Path (singl A a) (a, a) (b,p) = + (p @ i, p @ i /\ j) + +-- The first component of the above pair has to be a path from a to b, +-- this is exactly what p @ i gives us (note that we are to the right +-- of so that i is now in context). The second component should be +-- a square connecting a to p and this is exactly what the above +-- square for p @ i /\ j gives us. + +{- + +As we have seen we can do a lot of nice things with Path-types +already, but we cannot yet compose paths (i.e. we cannot prove +transitivity). Another thing we cannot do is prove the elimination +principle for Path-types. + +Recall that equality/identity types are usually introduced as an +inductive family: + + Inductive eq (A : Type) (a : A) : A -> Type := + | refl : eq A a a. + +this means that this type 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 approach taken in cubicaltt is very different to this approach to +adding equality to type theory. Instead of adding equality as an +inductive family we add various more primitive operation that will +allow us to prove J for Path types and in this way we will get that +Path types model equality. This relies on the following observation: + + J = contractibility of singletons + transport + +So in order to prove J is suffices to prove that singletons are +contractible and that we have an operation: + + transport : Path U A B -> A -> B + +So we "only" need to define transport, to do this we introduce a very +general new operation called "composition". This will allow us to +define transport and do a lot of other things. + +-} + + + + +--------------------------------------------------------------------------- +-- Composition -- +--------------------------------------------------------------------------- + + +{- + +Given p : Path A a b and q : Path A b c the composite of the two paths +is obtained from a composition of this open square: + + + a - - - - - - - - > c + ^ ^ + | | + | | + a | | q + | | + | | + | | + a ----------------> b + p @ i + +The composition computes the dashed line at the top of the square. + +-} +trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = + comp (<_> A) (p @ i) + [ (i = 0) -> a + , (i = 1) -> q ] + +{- + +The first argument to the comp is a path in the universe (i.e. an +equality of types), as all of the paths are in the same type this path +is constantly A. The second argument is the bottom of the cube we are +computing the composition of and the third argument is a list of the +sides of the cube. As we are only doing a square there are only 2 +sides (apart from the bottom). + +Note that the direction j is implicit in this operation, so q is +automatically fixed to go in the direction that we are computing the +composition in. This is different from the paper where the operation +is written comp^j so that the direction is explicit. Note also that +the order of the two last arguments is swapped here compared to the +paper, there is no deep reason for this. + +The reason we need to add a is that we want the top-left to be a, +if we would have omitted it it would have been "transport (<_> A) a". +We had a version of the system where this was the same as a, this +relied on a property which we called "regularity". It was however +proved by Dan Licata that this property is not preserved by the +algorithm for composition for the universe, so we had to drop it and +the user now has to give the a explicitly. + +-} + + +-- Another example of a simple composition: compose p with its inverse +compinv (A : U) (a b : A) (p : Path A a b) : Path A a a = + comp (<_> A) (p @ i) [ (i = 0) -> a, (i = 1) -> p @ -j ] + +-- Exercise (hard): is "compinv A a b p" Path equal to a? +ex (A : U) (a b : A) (p : Path A a b) : + Path (Path A a a) (compinv A a b p) ( a) = undefined + +-- Hint: construct a cube with a square with these as sides as its +-- missing top and compute it as a composition (the exercise above +-- about which squares one can make using /\, \/ and - will be +-- useful). + + +-- We can use Path types and compositions to prove basic results about +-- natural numbers in new ways. Recall that addition is defined by +-- recursion on the second argument: +-- +-- add (m : nat) : nat -> nat = split +-- zero -> m +-- suc n -> suc (add m n) + +-- 0 + a = a +addZero : (a : nat) -> Path nat (add zero a) a = split + zero -> zero + suc a' -> suc (addZero a' @ i) + + -- To see that this proof works try the following more verbose + -- version of the second branch: + + -- let rec : Path nat (add zero a') a' = addZero a' + -- goal : Path nat (suc (add zero a')) (suc a') = + -- suc (rec @ i) in goal + -- in goal + +-- (suc a) + b = suc (a + b) +addSuc (a : nat) : (b : nat) -> Path nat (add (suc a) b) (suc (add a b)) = split + zero -> suc a + suc n -> suc (addSuc a n @ i) + +-- a + b = b + a +addC (a : nat) : (b : nat) -> Path nat (add a b) (add b a) = split + zero -> addZero a @ -i -- a = 0 + a + suc n -> comp (<_> nat) (suc (addC a n @ i)) + [ (i = 0) -> suc (add a n) + , (i = 1) -> addSuc n a @ -j ] + + +-- Exercises: + +-- a + (b + c) = (a + b) + c +addA (a b c : nat) : Path nat (add a (add b c)) (add (add a b) c) = undefined + +-- Hint: do induction on c (this means that the type has to be changed +-- a little for the split to work) + + +-- (a + b) + c = (a + c) + b +addAC (a b c : nat) : Path nat (add (add a b) c) (add (add a c) b) = undefined + +-- a + (b + c) = b + (a + c) +addCA (a b c : nat) : Path nat (add a (add b c)) (add b (add a c)) = undefined -- 2.34.1