From: Anders Mörtberg Date: Mon, 20 Nov 2017 23:52:30 +0000 (-0500) Subject: comments X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=55af742271f56ecb22eac8b6a5739a1193ed8a7e;p=cubicaltt.git comments --- diff --git a/examples/univalence.ctt b/examples/univalence.ctt index b015cef..ec4675a 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -211,16 +211,17 @@ uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 = -- uabeta implies that equiv A B is a retract of Path U A B --- We don't have to use transEquivDirect: +-- We don't have to use transEquivDirect as below: -- uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquivDirect A B) = -- \(e : equiv A B) -> -- equivLemma A B (transEquivDirect A B (ua A B e)) e (uabeta A B e) +-- Instead we prove uabeta for transEquiv: +uabetaTransEquiv (A B : U) (e : equiv A B) : Path (A -> B) (transEquiv A B (ua A B e)).1 e.1 = + \(a : A) -> (uabeta A B e @ i) (fill (<_> A) a [] @ -i) + uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) = - \(e : equiv A B) -> - let rem (a : A) : Path B ((transEquiv A B (ua A B e)).1 a) (e.1 a) = - (uabeta A B e @ i) (fill (<_> A) a [] @ -i) - in equivLemma A B (transEquiv A B (ua A B e)) e ( \(a : A) -> rem a @ i) + \(e : equiv A B) -> equivLemma A B (transEquiv A B (ua A B e)) e (uabetaTransEquiv A B e) -- So (B:U) x equiv A B is a retract of (B:U) x Path U 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)