From 433d6c56ea220ace37bcdcc3dd099b551cbfbb8a Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 29 Jun 2015 13:31:21 +0200 Subject: [PATCH] Some lemmas about equivs --- examples/equiv.ctt | 6 ++++++ 1 file changed, 6 insertions(+) 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 = (is.2 (f x) (x, <_> f x) @ i).1 -- 2.34.1