v
b0 -----> b1
^ ^
- r0 | | r1
| |
+ r0 | | r1
| |
a0 -----> a1
u
-- 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
-- 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)
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
-- 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.
--------------------------------------------------------------------------
-- 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
-- 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:
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
projects / cubicaltt.git / commitdiff