From a7d01e2dc0a231d60de9dea07f616ba29c284eab Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 19 Apr 2018 10:47:39 -0400 Subject: [PATCH] opaque uaret --- examples/univalence.ctt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/examples/univalence.ctt b/examples/univalence.ctt index ec4675a..4c46d8a 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -227,9 +227,13 @@ uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) = f1 (A : U) (p : (B : U) * equiv A B) : ((B : U) * Path U A B) = (p.1,ua A p.1 p.2) f2 (A : U) (p : (B : U) * Path U A B) : ((B : U) * equiv A B) = (p.1,transEquiv A p.1 p.2) +opaque uaret + uaretsig (A : U) : retract ((B : U) * equiv A B) ((B : U) * Path U A B) (f1 A) (f2 A) = \(p : (B : U) * equiv A B) -> (p.1,uaret A p.1 p.2 @ i) +transparent uaret + -- But (B : U) x Path U A B is contractible isContrPath (A : U) : isContr ((B : U) * Path U A B) = let ctr : (B : U) * Path U A B = (A,<_> A) -- 2.34.1