From: Anders Mörtberg Date: Sat, 18 Nov 2017 15:45:09 +0000 (-0500) Subject: update lectures X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d7751c7bccdd8b79b0b0d985e1aa49886553bb47;p=cubicaltt.git update lectures --- diff --git a/lectures/lecture3.ctt b/lectures/lecture3.ctt index 812489f..f96f3a9 100644 --- a/lectures/lecture3.ctt +++ b/lectures/lecture3.ctt @@ -85,8 +85,8 @@ We can also define the type of squares: v b0 -----> b1 ^ ^ - r0 | | r1 | | + r0 | | r1 | | a0 -----> a1 u @@ -120,6 +120,12 @@ This is like a cast operation (compare with castmx of MathComp). -- 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 [] +-- Note that transporting a along a constant family is only Path (and +-- not judgmentally) equal to a. This implies that the computation +-- rule for J only holds up to a Path equality, see JEq below. +transEq (A : U) (a : A) : Path A a (trans A A (<_> A) a) = + fill (<_> A) a [] + -- This uses that the composition operations are heterogeneous. So the -- lower line of the square can be in type A while the constructed -- line is in B. The sides then have to connect elements in A to @@ -136,6 +142,9 @@ subst (A : U) (P : A -> U) (a b : A) -- we don't have implicit arguments, so we have a built-in transport -- function with the first two arguments implicit. +substEq (A : U) (P : A -> U) (a : A) (e : P a) : + Path (P a) e (subst A P a a (refl A a) e) = transEq (P a) e + -- Combined with the contractibility of singletons this gives us the J -- eliminator: J (A : U) (a : A) (P : (b : A) -> Path A a b -> U) @@ -145,6 +154,29 @@ J (A : U) (a : A) (P : (b : A) -> Path A a b -> U) B : U = (b : A) * Path A a b T (y : B) : U = P y.1 y.2 +-- Computation rule only holds up to Path equality: +JEq (A : U) (a : A) (C : (x : A) -> Path A a x -> U) + (d : C a (refl A a)) : + Path (C a (refl A a)) d (J A a C d a (refl A a)) = + substEq (singl A a) T (a, refl A a) d + where T (z : singl A a) : U = C (z.1) (z.2) + +-- Open problem: define a type theory or constructive model where this +-- holds judgmentally. + +-- We tried to do this by enforcing a "regularity condition": if the +-- type we are transporting in doesn't depend on the direction then it +-- is the identity function, so "comp (<_> A) a [] == a" and we get +-- the computation rule judgmentally. However this condition is not +-- preserved by the universe as noted by Dan Licata from discussions +-- with Carlo Angiuli and Bob Harper) and discussed in this thread: +-- +-- https://groups.google.com/forum/#!topic/homotopytypetheory/oXQe5u_Mmtk + +-- Note that we can define Id types in terms of Path types for which +-- this holds judgmentally, however we don't get all of the nice +-- syntax that we have for Path types for Id types. + -------------------------------------------------------------------------- -- H-levels @@ -223,6 +255,6 @@ isContrProp (A : U) (h : isContr A) : isProp A = undefined -- sets. The next level is called groupoids, we then have 2-groupoids, -- 3-groupoids, etc. --- Remark: Some people (usually homotopy theorists) use the word --- "n-type" and start counting from -2. So a -2-type is contractible, --- a -1-type is a proposition, a 0-type is a set, etc. +-- Remark: homotopy theorists use the word "n-type" and start counting +-- from -2. So a -2-type is contractible, a -1-type is a proposition, +-- a 0-type is a set, etc. diff --git a/lectures/lecture4.ctt b/lectures/lecture4.ctt index bfad4e3..c46d98b 100644 --- a/lectures/lecture4.ctt +++ b/lectures/lecture4.ctt @@ -275,11 +275,39 @@ cyril : eats bool = substEquiv eats bool bool notEquiv anders -------------------------------------------------------------------------- -- Univalence --- The file examples/univalence.ctt contains 3 proofs of univalence. --- The simplest one is based on an idea of Dan Licata: +-- The file examples/univalence.ctt contains 3 proofs of univalence +-- that are all in the paper: -- --- https://groups.google.com/forum/#!topic/homotopytypetheory/j2KBIvDw53s +-- 1. Direct proof that transEquiv : A = B -> equiv A B is an +-- equivalence. Inverse map defined using Glue. Uses a higher +-- dimensional Glue to prove one of the equalities. +-- +-- 2. unglue is an equivalence. Conceptually the nicest. Very closely +-- related to the proof that the universe is univalent in the +-- simplicial set model (see theorem 3.4.1). +-- +-- 3. ua + uabeta: sufficient condition as noted by Dan Licata on the +-- HoTT google group (implicit in various earlier messages by +-- Egbert Rijke and Martin Escardo): +-- +-- https://groups.google.com/forum/#!topic/homotopytypetheory/j2KBIvDw53s + +-- In 2 and 3 we prove that (X : U) * equiv A X is contractible which +-- is equivalent to: +-- thmUniv (t : (X A : U) -> Path U X A -> equiv X A) (A : U) : +-- (X : U) -> isEquiv (Path U X A) (equiv X A) (t X A) = + +-- In particular this implies the traditional formulation of +-- univalence. I learned this from a post by Martin Escardo on the +-- HoTT google group and the proof is now in the HoTT book. Note that +-- this the above formulation is like contractible singletons for +-- equivalences and hence implies the elimination principle for +-- equivalences. + + +-- Here is a sketch of proof 3: +-- -- The idea is to reduce univalence to two simple axioms: -- -- ua (A B : U) (e : equiv A B) : Path U A B @@ -295,8 +323,18 @@ uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 = un -- 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. + +-- Open problem: construct a type theory where this holds judgmentally. + +-- Once we have proved uabeta we have that equiv A B is a retract of Path U A B. +-- +-- So (X : U) * equiv A X is a retract of (X : U) * Path U A X +-- +-- But (X : U) * Path U A X is contractible +-- +-- So (X : U) * equiv A X is contractible as well. + + -- A further reduction of these axioms to even simpler axioms have -- recently been found by Ian Orton and Andrew Pitts: @@ -332,8 +370,10 @@ flipbeta (A B : U) (C : A -> B -> U) (a : A) (b : B) (c : C a b) : What I didn't talk about: o Id types: we can define a type from Path types for which the - computation rule for J holds judgmentally. See - examples/idtypes.ctt + computation rule for J holds judgmentally. We call these types Id + types and they are equivalent to Path types, so we get univalence + for them as well and cubicaltt+Id is an extension of MLTT+UA. + For details see examples/idtypes.ctt o Higher inductive types: we can define some higher inductive types directly in the system. Non-recursive HITs like the circle or the