From: Anders <mortberg@chalmers.se>
Date: Mon, 29 Jun 2015 11:31:21 +0000 (+0200)
Subject: Some lemmas about equivs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=433d6c56ea220ace37bcdcc3dd099b551cbfbb8a;p=cubicaltt.git

Some lemmas about equivs
---

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