From: Anders Mörtberg Date: Fri, 29 Jul 2016 12:12:07 +0000 (+0200) Subject: define equivalence using Id and prove univalence with Id everywhere X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=53541cdc8e06d291dfbf614a3b00f15935f81d4f;p=cubicaltt.git define equivalence using Id and prove univalence with Id everywhere --- diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index b82050b..d0705dd 100644 --- a/examples/idtypes.ctt +++ b/examples/idtypes.ctt @@ -1,5 +1,6 @@ module idtypes where +import sigma import univalence refId (A : U) (a : A) : Id A a a = @@ -70,7 +71,7 @@ PathIdPath (A B : U) : Path U (Id U A B) (Path U A B) = (\(p : Id U A B) -> idToPathToId U A B p @ - i) -- A few different versions of univalence for Id: -IdUnivalence1 (A B : U) : Path U (Id U A B) (equiv A B) = +IdUnivalence1 (A B : U) : Path U (Id U A B) (equiv A B) = compPath U (Id U A B) (Path U A B) (equiv A B) (PathIdPath A B) (corrUniv A B) IdUnivalence2 (A B : U) : equiv (Id U A B) (equiv A B) = @@ -79,7 +80,97 @@ IdUnivalence2 (A B : U) : equiv (Id U A B) (equiv A B) = IdUnivalence3 (A B : U) : Id U (Id U A B) (equiv A B) = pathToId U (Id U A B) (equiv A B) (IdUnivalence1 A B) --- TODO: redefine equiv using Id? + +-- Redefine equivalence using Id and prove univalence with this formulation + +fiberId (A B : U) (f : A -> B) (y : B) : U = + (x : A) * Id B y (f x) + +isContrId (A : U) : U = (x : A) * ((y : A) -> Id A x y) + +isEquivId (A B : U) (f : A -> B) : U = (y : B) -> isContrId (fiberId A B f y) + +equivId (A B : U) : U = (f : A -> B) * isEquivId A B f + +fiberToFiberId (A B : U) (f : A -> B) (y : B) : + Path U (fiber A B f y) (fiberId A B f y) = + isoPath (fiber A B f y) (fiberId A B f y) f1 f2 rem1 rem2 + where + f1 (t : fiber A B f y) : fiberId A B f y = (t.1,pathToId B y (f t.1) t.2) + f2 (t : fiberId A B f y) : fiber A B f y = (t.1,idToPath B y (f t.1) t.2) + rem1 (x : fiberId A B f y) : Path (fiberId A B f y) (f1 (f2 x)) x = + (x.1,idToPathToId B y (f x.1) x.2 @ -i) + rem2 (x : fiber A B f y) : Path (fiber A B f y) (f2 (f1 x)) x = + (x.1,pathToIdToPath B y (f x.1) x.2 @ -i) + +isContrToIsContrId (A : U) (p : isContr A) : isContrId A = + (p.1,\(y : A) -> pathToId A p.1 y (p.2 y)) + +equivToEquivId (A B : U) (e : equiv A B) : equivId A B = (f,rem) + where + f : A -> B = e.1 + rem (y : B) : isContrId (fiberId A B f y) = + transport ( isContrId (fiberToFiberId A B f y @ i)) + (isContrToIsContrId (fiber A B f y) (e.2 y)) + +isContrToIsContrIdU (A : U) : Path U (isContr A) (isContrId A) = + isoPath (isContr A) (isContrId A) f1 f2 rem1 rem2 + where + f1 : isContr A -> isContrId A = isContrToIsContrId A + f2 (p : isContrId A) : isContr A = (p.1,\(y : A) -> idToPath A p.1 y (p.2 y)) + + rem1 (x : isContrId A) : Path (isContrId A) (f1 (f2 x)) x = + (x.1,\(y : A) -> idToPathToId A x.1 y (x.2 y) @ - i) + rem2 (x : isContr A) : Path (isContr A) (f2 (f1 x)) x = + (x.1,\(y : A) -> pathToIdToPath A x.1 y (x.2 y) @ - i) + +isContrFiberToIsContrFiberId (A B : U) (f : A -> B) (y : B) : + Path U (isContr (fiber A B f y)) (isContrId (fiberId A B f y)) = goal + where + rem1 : Path U (isContr (fiber A B f y)) (isContr (fiberId A B f y)) = + isContr (fiberToFiberId A B f y @ i) + rem2 : Path U (isContr (fiberId A B f y)) (isContrId (fiberId A B f y)) = + isContrToIsContrIdU (fiberId A B f y) + goal : Path U (isContr (fiber A B f y)) (isContrId (fiberId A B f y)) = + compPath U (isContr (fiber A B f y)) (isContr (fiberId A B f y)) + (isContrId (fiberId A B f y)) rem1 rem2 + +opaque isContrFiberToIsContrFiberId + +equivEquivIdU (A B : U) : Path U (equiv A B) (equivId A B) = + isoPath (equiv A B) (equivId A B) f1 f2 rem1 rem2 + where + f1 (p : equiv A B) : equivId A B = + (p.1,\(y : B) -> trans (isContr (fiber A B p.1 y)) + (isContrId (fiberId A B p.1 y)) + (isContrFiberToIsContrFiberId A B p.1 y) (p.2 y)) + f2 (p : equivId A B) : equiv A B = + (p.1,\(y : B) -> transNeg (isContr (fiber A B p.1 y)) + (isContrId (fiberId A B p.1 y)) + (isContrFiberToIsContrFiberId A B p.1 y) (p.2 y)) + + rem1 (x : equivId A B) : Path (equivId A B) (f1 (f2 x)) x = + (x.1,\(y : B) -> transK (isContr (fiber A B x.1 y)) + (isContrId (fiberId A B x.1 y)) + (isContrFiberToIsContrFiberId A B x.1 y) (x.2 y) @ -i) + + rem2 (x : equiv A B) : Path (equiv A B) (f2 (f1 x)) x = + (x.1,\(y : B) -> transNegK (isContr (fiber A B x.1 y)) + (isContrId (fiberId A B x.1 y)) + (isContrFiberToIsContrFiberId A B x.1 y) (x.2 y) @ -i) + +transparent isContrFiberToIsContrFiberId + +-- Univalence expressed using Id everywhere: +univalenceId (A B : U) : equivId (Id U A B) (equivId A B) = + equivToEquivId (Id U A B) (equivId A B) rem1 + where + rem : Path U (Id U A B) (equivId A B) = + compPath U (Id U A B) (equiv A B) (equivId A B) + (IdUnivalence1 A B) (equivEquivIdU A B) + rem1 : equiv (Id U A B) (equivId A B) = + transEquiv' (equivId A B) (Id U A B) rem + -------------------------------------------------------------------------------- -- Some tests diff --git a/examples/prelude.ctt b/examples/prelude.ctt index f9b0b31..ce9a07b 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -17,6 +17,27 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) -- Transport can be defined using comp trans (A B : U) (p : Path U A B) (a : A) : B = comp p a [] +transNeg (A B : U) (p : Path U A B) (b : B) : A = comp ( p @ - i) b [] + +transK (A B : U) (p : Path U A B) (y : B) : + Path B y (trans A B p (transNeg A B p y)) = + comp p (transNeg A B p y) [(i=0) -> rem1 + ,(i=1) -> rem2 (transNeg A B p y)] + where + rem1 : PathP p (transNeg A B p y) y = + comp ( p @ (i\/-j)) y [(i=1) -> y] + rem2 (x:A) : PathP p x (trans A B p x) = + comp ( p @ (i/\j)) x [(i=0) -> x] + +transNegK (A B : U) (p : Path U A B) (a : A) : + Path A a (transNeg A B p (trans A B p a)) = + comp ( p @ -j) (trans A B p a) [(i=0) -> rem1 + ,(i=1) -> rem2 (trans A B p a) ] + where + rem1 : PathP ( p@-i) (trans A B p a) a = + comp ( p @ (-i /\ j)) a [(i=1) -> a] + rem2 (b:B) : PathP ( p@-i) b (transNeg A B p b) = + comp ( p @ (-i \/ -j)) b [(i=0) -> b] -- subst can be defined using trans: substTrans (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b =