From: Anders Mörtberg <andersmortberg@gmail.com>
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) -> <i> (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)