From: Anders Mörtberg Date: Sat, 20 May 2017 09:49:16 +0000 (+0200) Subject: minor update to lecture 2 X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=28ae754fded3b105e1177d06139a21f99f82ac0f;p=cubicaltt.git minor update to lecture 2 --- diff --git a/lectures/lecture2.ctt b/lectures/lecture2.ctt index e15271d..607397e 100644 --- a/lectures/lecture2.ctt +++ b/lectures/lecture2.ctt @@ -4,7 +4,7 @@ Anders Mörtberg Contents: - o Path types part 2 + o Path types part 2 (symmetry and connections) o Compositions Recall: @@ -19,30 +19,31 @@ import lecture1 {- -We have an operation on II that corresponds to: +We have an involutive operation on II that corresponds to: - -i "=" 1 - i + -i = 1 - i -for the real interval [0,1]. +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 --- 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 +-- As 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. +-- 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. {- -We call the elements of the interval II by -names/directions/dimensions/colors and typically use i, j, k to denote -them: +We call the elements of the interval II names/directions/dimensions +and typically use i, j, k to denote them: dir := i, j, k... @@ -57,7 +58,8 @@ r,s := 0 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. +i and j, and that i \/ j corresponds to the max of i and j, for i and +j in [0,1]. 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 @@ -79,25 +81,26 @@ In particular the laws: 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. +we of course cannot have min(1-r,r) = 0 or max(1-r,r) = 1 for a point +r in [0,1]. -To test if two elements r and s in II are equal first push the +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 (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: +distributive lattice on formal generators i and -i). This gives us for +example the following equations: 0 /\ r = 0 1 /\ r = r r /\ s = s /\ r -and similarily for \/. +and similarly 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: +dimensional equalities. If p : Path A a b then p @ i /\ j is the +interior of the square: p @@ -113,8 +116,8 @@ dimensional equalities. If p : Path A a b then: 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: +the down-to-up dimension. To compute the left and right endpoints just +plug in i=0 and i=1 in 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) @@ -146,7 +149,7 @@ Exercise: draw the squares for -} --- The ability to construct there squares makes it easy to prove some +-- The ability to construct these 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 @@ -174,7 +177,7 @@ 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: +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 @@ -188,7 +191,8 @@ 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: +Path types model equality. Our approach relies on the following +observation: J = contractibility of singletons + transport @@ -236,31 +240,30 @@ trans (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = [ (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. - --} +-- The first argument to the comp is a path in the universe (i.e. an +-- equality of types), as all of the paths in the example 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). If +-- it would have been an open box we would have to give 4 sides (that +-- have to be squares), and so on. + +-- 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 point +-- to be a, if we would have omitted it it would instead have been +-- "transport (<_> A) a". We used to have 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 a +-- explicitly. -- Another example of a simple composition: compose p with its inverse @@ -272,9 +275,9 @@ 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). +-- missing top and compute it as a composition (the exercise about +-- which squares one can make using /\, \/ and - will be very useful +-- for this). -- We can use Path types and compositions to prove basic results about @@ -325,3 +328,16 @@ 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 + + + + +{- + +That's all for this lecture. Next time we will do: + + o Examples of higher dimensional compositions + o Transport and J for Path types + o Fill + +-}