From: Anders Mörtberg Date: Thu, 19 Apr 2018 14:47:39 +0000 (-0400) Subject: opaque uaret X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a7d01e2dc0a231d60de9dea07f616ba29c284eab;p=cubicaltt.git opaque uaret --- 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)