From: Anders Mörtberg Date: Sat, 11 Nov 2017 15:46:28 +0000 (-0500) Subject: direct proof that being an equiv is a prop X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c3612560fa30cecc86902daf097c8dd77b9b0b7d;p=cubicaltt.git direct proof that being an equiv is a prop --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index d5a80c0..d4877eb 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -16,6 +16,28 @@ propIsEquiv (A B : U) (f : A -> B) \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i +propIsEquivDirect (A B : U) (f : A -> B) : prop (isEquiv A B f) = + \(p q : isEquiv A B f) -> + \(y : B) -> + let p0 : A = (p y).1.1 + p1 : Path B y (f p0) = (p y).1.2 + p2 : (w1 : fiber A B f y) -> Path (fiber A B f y) (p0,p1) w1 = + (p y).2 + q0 : A = (q y).1.1 + q1 : Path B y (f q0) = (q y).1.2 + q2 : (w1 : fiber A B f y) -> Path (fiber A B f y) (q0,q1) w1 = + (q y).2 + in (p2 (q0,q1) @ i, + \(w : fiber A B f y) -> + let sq : PathP ( Path (fiber A B f y) (p2 (q0,q1) @ j) w) (p2 w) (q2 w) = + comp (<_> fiber A B f y) (p2 w @ i \/ j) + [ (i = 0) -> p2 w @ j + , (i = 1) -> q2 w @ j \/ -k + , (j = 0) -> p2 (q2 w @ -k) @ i + , (j = 1) -> w ] + in sq @ i) + + equivLemma (A B : U) : (v w : equiv A B) -> Path (A -> B) v.1 w.1 -> Path (equiv A B) v w = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)