--- /dev/null
+{-
+ Lecture 2 on cubicaltt (Cubical Type Theory)
+--------------------------------------------------------------------------
+ Anders Mörtberg
+
+Contents:
+ o Path types part 2
+ o Compositions
+
+Recall:
+ <i> <- Path abstraction
+ p @ i <- Path application
+ refl A a := <i> 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 = <i> 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
+ ^ ^
+ | |
+ | |
+ <j> a | <i j> p @ i /\ j | p
+ | |
+ | |
+ | |
+ a -----------------> a
+ <i> 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:
+
+<j> p @ 0 /\ j = <j> p @ 0 = <j> a (recall that p is a path from a to b)
+<j> p @ 1 /\ j = <j> p @ j = p (note that we have eta for Path-types)
+
+
+Applying p to a disjunction gives:
+
+
+ <i> b
+ b -----------------> b
+ ^ ^
+ | |
+ | |
+ p | <i j> p @ i \/ j | <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,<i> a) (b,p) =
+ <i> (p @ i,<j> 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 <i> so that i is now in context). The second component should be
+-- a square connecting <i> 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
+ ^ ^
+ | |
+ | |
+ <j> 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 =
+ <i> comp (<_> A) (p @ i)
+ [ (i = 0) -> <j> 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 <j> 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 <j> 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 =
+ <i> comp (<_> A) (p @ i) [ (i = 0) -> <j> a, (i = 1) -> <j> p @ -j ]
+
+-- Exercise (hard): is "compinv A a b p" Path equal to <j> a?
+ex (A : U) (a b : A) (p : Path A a b) :
+ Path (Path A a a) (compinv A a b p) (<j> 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 -> <i> zero
+ suc a' -> <i> 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') =
+ -- <i> 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 -> <i> suc a
+ suc n -> <i> suc (addSuc a n @ i)
+
+-- a + b = b + a
+addC (a : nat) : (b : nat) -> Path nat (add a b) (add b a) = split
+ zero -> <i> addZero a @ -i -- a = 0 + a
+ suc n -> <i> comp (<_> nat) (suc (addC a n @ i))
+ [ (i = 0) -> <j> suc (add a n)
+ , (i = 1) -> <j> 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
projects / cubicaltt.git / commitdiff