From 2042669361bd5384232aabfcf2d0ce5ecb659a3e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 26 Jul 2016 17:18:54 +0200 Subject: [PATCH] cleaning and a version of univalence for Id --- CTT.hs | 3 +++ examples/{eq.ctt => idtypes.ctt} | 44 ++++++++++++++++++++++---------- 2 files changed, 33 insertions(+), 14 deletions(-) rename examples/{eq.ctt => idtypes.ctt} (58%) diff --git a/CTT.hs b/CTT.hs index de3c8c7..0c14a12 100644 --- a/CTT.hs +++ b/CTT.hs @@ -450,6 +450,9 @@ showVal v = case v of VUnGlueElemU v b es -> text "unglue U" <+> showVals [v,b] <+> text (showSystem es) VCompU a ts -> text "comp (<_> U)" <+> showVal1 a <+> text (showSystem ts) + VId a u v -> text "Id" <+> showVals [a,u,v] + VIdPair b ts -> text "IdC" <+> showVal1 b <+> text (showSystem ts) + VIdJ a t c d x p -> text "IdJ" <+> showVals [a,t,c,d,x,p] showPLam :: Val -> Doc showPLam e = case e of diff --git a/examples/eq.ctt b/examples/idtypes.ctt similarity index 58% rename from examples/eq.ctt rename to examples/idtypes.ctt index d093797..e090176 100644 --- a/examples/eq.ctt +++ b/examples/idtypes.ctt @@ -1,6 +1,6 @@ -module eq where +module idtypes where -import prelude +import univalence refId (A : U) (a : A) : Id A a a = idC ( a) [ -> a ] @@ -33,36 +33,52 @@ 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) ( a) b p -idToId (A : U) (a b : A) (p : Path A a b) : Id A a b = +pathToId (A : U) (a b : A) (p : Path A a b) : Id A a b = -- idC p [] J A a (\ (b : A) (p : Path A a b) -> Id A a b) (refId A a) b p -idToIdRef (A : U) (a : A) : Path (Id A a a) (refId A a) (idToId A a a (<_> a)) = +pathToIdRef (A : U) (a : A) : Path (Id A a a) (refId A a) (pathToId A a a (<_> a)) = JEq A a (\ (b : A) (p : Path A a b) -> Id A a b) (refId A a) idToPathRef (A : U) (a : A) : Path (Path A a a) (<_> a) (idToPath A a a (refId A a)) = a - -idToIdToPath (A : U) (a b : A) (p : Path A a b) : - Path (Path A a b) p (idToPath A a b (idToId A a b p)) = +pathToIdToPath (A : U) (a b : A) (p : Path A a b) : + Path (Path A a b) p (idToPath A a b (pathToId A a b p)) = J A a (\ (b : A) (p : Path A a b) -> - Path (Path A a b) p (idToPath A a b (idToId A a b p))) - ( idToPath A a a (idToIdRef A a @ j)) b p + Path (Path A a b) p (idToPath A a b (pathToId A a b p))) + ( idToPath A a a (pathToIdRef A a @ j)) b p lem (A : U) (a : A) : - Path (Id A a a) (refId A a) (idToId A a a (idToPath A a a (refId A a))) = + Path (Id A a a) (refId A a) (pathToId A a a (idToPath A a a (refId A a))) = compPath (Id A a a) - (refId A a) (idToId A a a (<_> a)) (idToId A a a (idToPath A a a (refId A a))) - (idToIdRef A a) ( idToId A a a (idToPathRef A a @ k)) + (refId A a) (pathToId A a a (<_> a)) (pathToId A a a (idToPath A a a (refId A a))) + (pathToIdRef A a) ( pathToId A a a (idToPathRef A a @ k)) idToPathToId (A : U) (a b : A) (p : Id A a b) : - Path (Id A a b) p (idToId A a b (idToPath A a b p)) = + Path (Id A a b) p (pathToId A a b (idToPath A a b p)) = idJ A a (\ (b : A) (p : Id A a b) -> - Path (Id A a b) p (idToId A a b (idToPath A a b p))) + Path (Id A a b) p (pathToId A a b (idToPath A a b p))) (lem A a) b p +PathIdPath (A B : U) : Path U (Id U A B) (Path U A B) = + equivPath (Id U A B) (Path U A B) (idToPath U A B) rem + where rem : isEquiv (Id U A B) (Path U A B) (idToPath U A B) = + gradLemma (Id U A B) (Path U A B) (idToPath U A B) (pathToId U A B) + (\(p : Path U A B) -> pathToIdToPath U A B p @ - i) + (\(p : Id U A B) -> idToPathToId U A B p @ - i) + +-- One version of univalence for Id +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) + +-- TODO: prove the following: + +-- equivIdEquiv (A B : U) : equiv (Id U A B) (equiv A B) = undefined + +-- IdUnivalence2 (A B : U) : Id U (Id U A B) (equiv A B) = undefined + -------------------------------------------------------------------------------- -- Some tests -- 2.34.1