From: Simon Huber Date: Fri, 11 Sep 2015 20:18:54 +0000 (+0200) Subject: Another formulation of univalence X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=84b57eb06f65b4d02d05858d0a81202135acbb21;p=cubicaltt.git Another formulation of univalence --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index e3edaed..3e5d933 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -27,6 +27,10 @@ propIsEquiv (A B : U) (f : A -> B) \ (y : B) (w : fibf y) -> propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i +equivLemma (A B : U) + : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w + = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) + -- The identity function is an equivalence idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y) diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 73ead54..ac236fa 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -30,13 +30,16 @@ transIdFun (A B : U) (w : equiv A B) idToId (A B : U) (w : equiv A B) : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w - = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) - (transEquiv A B (transEquivToId A B w)) w + = equivLemma A B (transEquiv A B (transEquivToId A B w)) w (transIdFun A B w) +transEquivIsEquiv (A B : U) + : isEquiv (Id U A B) (equiv A B) (transEquiv A B) + = gradLemma (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + univalence (A B : U) : equiv (Id U A B) (equiv A B) = - (transEquiv A B,gradLemma (Id U A B) (equiv A B) (transEquiv A B) - (transEquivToId A B) (idToId A B) (eqToEq A B)) + (transEquiv A B,transEquivIsEquiv A B) univalence1 (A B:U) : Id U (Id U A B) (equiv A B) = isoId (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B) (idToId A B) (eqToEq A B) @@ -47,3 +50,35 @@ test (A : U) : Id (equiv A A) (transEquiv A A (transEquivToId A A (idEquiv A))) idToId A A (idEquiv A) +-- The canonical map defined using J +canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B = + J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A) + +canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) = + fill (<_> A -> A) (idfun A) [] @ -i + +transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) = + \ (a : A) -> fill (<_> A) a [] @ i + +canIdToEquivLem (A : U) : (B : U) (p : Id U A B) -> + Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1 + = J U A + (\ (B : U) (p : Id U A B) -> + Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1) + (compId (A -> A) + (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A)) + (canDiagTrans A) (transDiagTrans A)) + +canIdToEquivIsTransEquiv (A B : U) : + Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) = + \ (p : Id U A B) -> + equivLemma A B (canIdToEquiv A B p) (transEquiv A B p) + (canIdToEquivLem A B p) @ i + +-- The canonical map is an equivalence +univalence2 (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) = + substInv (Id U A B -> equiv A B) + (isEquiv (Id U A B) (equiv A B)) + (canIdToEquiv A B) (transEquiv A B) + (canIdToEquivIsTransEquiv A B) + (transEquivIsEquiv A B) \ No newline at end of file