From 553815428a8d07a6510bc4623a331313ce5ecb78 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 26 Jul 2016 17:26:34 +0200 Subject: [PATCH] minor changes --- examples/idtypes.ctt | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index e090176..b82050b 100644 --- a/examples/idtypes.ctt +++ b/examples/idtypes.ctt @@ -69,16 +69,17 @@ PathIdPath (A B : U) : Path U (Id U A B) (Path 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 +-- A few different versions 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: +IdUnivalence2 (A B : U) : equiv (Id U A B) (equiv A B) = + transEquiv' (equiv A B) (Id U A B) (IdUnivalence1 A B) --- 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 +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? -------------------------------------------------------------------------------- -- Some tests -- 2.34.1