Some lemmas about equivs

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 036a0db2ef313641aa772fab1f5aae42e2748e3f..1e67a073cf678bcf14c98d0776c16388065dcb27 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -116,7 +116,13 @@ transDelta (A : U) : equiv A A = transEquiv A A (<_> A)
 \r
 \r
 \r
+invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1\r
 \r
+retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :\r
+  Id B (f (invEquiv A B f is y)) y = (is.1 y).2\r
+\r
+secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :\r
+  Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1\r
 \r
 \r
 \r