From cc5cc3ca39136962318b0f63cd84be056caf5090 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 19 Jan 2017 14:44:29 +0100 Subject: [PATCH] experiment with Id --- examples/idtypes.ctt | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index d2bb65e..be8c80f 100644 --- a/examples/idtypes.ctt +++ b/examples/idtypes.ctt @@ -26,11 +26,17 @@ substId (A : U) (F : A -> U) (a b : A) (p : Id A a b) (e : F a) : F b = substIdRef (A : U) (F : A -> U) (a : A) (e : F a) : F a = substId A F a a (refId A a) e -transId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = +transId (A B : U) (p : Id U A B) (a : A) : B = + substId U (idfun U) A B p a + +transIdRef (A B : U) (p : Id U A B) (a : A) : + Id A (transId A A (refId U A) a) a = refId A a + +compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = substId A (\ (z : A) -> Id A a z) b c q p -transIdRef (A : U) (a b : A) (p : Id A a b): Id A a b = - transId A a a b (refId A a) p +compIdRef (A : U) (a b : A) (p : Id A a b): Id A a b = + compId A a a b (refId A a) p idToPath (A : U) (a b : A) (p : Id A a b) : Path A a b = idJ A a (\ (b : A) (p : Id A a b) -> Path A a b) @@ -94,6 +100,8 @@ 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 +invEquivId (A B : U) (w : equivId A B) (b : B) : A = (w.2 b).1.1 + 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 @@ -174,6 +182,17 @@ univalenceId (A B : U) : equivId (Id U A B) (equivId A B) = transEquiv' (equivId A B) (Id U A B) rem +-- Experiment to define ua and uabeta for Id: + +uaId (A B : U) (e : equivId A B) : Id U A B = + invEquivId (Id U A B) (equivId A B) (univalenceId A B) e + +-- Can we get this to typecheck? +-- uabetaId (A B : U) (e : equivId A B) (a : A) : +-- Id B (transId A B (uaId A B e) a) (e.1 a) = +-- refId B (e.1 a) + + -------------------------------------------------------------------------------- -- Some tests -- 2.34.1