Anders Mörtberg
Contents:
- o Path types part 2
+ o Path types part 2 (symmetry and connections)
o Compositions
Recall:
{-
-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 = <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
+-- 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...
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
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 <i j> p @ i /\ j is the
+interior of the square:
p
<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:
+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:
<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)
-}
--- 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
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
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
[ (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.
-
--}
+-- 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 <j> 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 <j> a
+-- explicitly.
-- Another example of a simple composition: compose p with its inverse
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).
+-- 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
-- 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
+
+-}
projects / cubicaltt.git / commitdiff