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).
-}
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 _).
-- Path types
{-
+
We would like to prove: (b : bool) -> not (not b) = b
But what is =?
type we introduce a Path type called PathP together with a binder,
written <i>, 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
{-
The simplest path possible is the reflexivity path:
- <i>a
- a ------> a
+ <i> a
+ a -------> a
The intuition is that
- <i> u
+ <i> a
corresponds to
- \(i : II) -> u
+ \(i : II) -> a
So <i> 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 = <i> a
(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
import lecture1
-{-
+{-
We have an involutive operation on II that corresponds to:
-- 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
--- 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.
{-
- 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
0 /\ r = 0
1 /\ r = r
r /\ s = s /\ r
-
+
and similarly for \/.
| 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
| |
| |
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 <i> 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 =
-- 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
-
{-
That's all for this lecture. Next time we will do:
-- 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 =
If we substitute k for 0 in ex we get:
- <j> comp (<_> A) (p @ j /\ -0)
+ <j> comp (<_> A) (p @ j /\ -0)
[ (j = 0) -> <i> a
, (j = 1) -> <i> p @ -i /\ -0
, (0 = 1) -> <i> a ]
The face 0=1 is absurd and disappears by the rules of the system. We
hence get the following after simplifications:
- <j> comp (<_> A) (p @ j)
+ <j> comp (<_> A) (p @ j)
[ (j = 0) -> <i> a
, (j = 1) -> <i> p @ -i ]
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.
-}
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.
{-
-Given P : Path U A B we want to define
+Given P : Path U A B we want to define
transport P : A -> B
-}
-- 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
-- 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 (<i> P (p @ i)) e
+ (p : Path A a b) (e : P a) : P b = transport (<i> 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
-- 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
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 =
<i> \(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
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)
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
-- (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) ->
<i> \(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,<i>s y@-i),\ (z:fiber A B f y) ->
- lemIso A B f g s t y (g y) z.1 (<i>s y@-i) z.2)
+ \(y : B) -> ((g y,<i> s y @ -i),\(z : fiber A B f y) ->
+ lemIso A B f g s t y (g y) z.1 (<i> 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)
(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
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
-- (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:
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
projects / cubicaltt.git / commitdiff