{- Equivalence: - Surjective, Injective, Embedding, Hae; - Theorems, Gluening; - Univalence Type. Copyright (c) Groupoid Infinity, 2014-2018. HoTT 4.6 Surjections and Embedding -} module equiv where import proto_equiv import sigma import retract import trunc isSurjective (A B: U) (f: A -> B): U = (b: B) * pTrunc (fiber A B f b) surjective (A B: U): U = (f: A -> B) * isSurjective A B f isInjective (A B: U) (f: A -> B): U = (x y: A) -> Path B (f x) (f y) -> Path A x y isInjective' (A B: U) (f: A -> B): U = (b: B) -> isProp (fiber A B f b) injective (A B: U): U = (f: A -> B) * isInjective A B f isEmbedding (A B: U) (f: A -> B) : U = (x y: A) -> isEquiv (Path A x y) (Path B (f x) (f y)) (cong A B f x y) embedding (A B: U): U = (f: A -> B) * isEmbedding A B f isHae (A B: U) (f: A -> B): U = (g: B -> A) * (eta_: Path (id A) (o A B A g f) (idfun A)) * (eps_: Path (id B) (o B A B f g) (idfun B)) * ((x: A) -> Path B (f ((eta_ @ 0) x)) ((eps_ @ 0) (f x))) hae (A B: U): U = (f: A -> B) * isHae A B f 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) (propIsEquivDirect A B) equivPath (T A: U) (f: T -> A) (p: isEquiv T A f): Path U T A = Glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] invEq (A B:U)(w:equiv A B)(y:B): A = (w.2 y).1.1 retEq (A B:U)(w:equiv A B)(y:B): Path B (w.1 (invEq A B w y)) y = (w.2 y).1.2@-i secEq (A B:U)(w:equiv A B)(x:A): Path A (invEq A B w (w.1 x)) x = ((w.2(w.1 x)).2(x,w.1 x)@i).1 -- Univalence Formation univ_Formation (A B: U): U = equiv A B -> Path U A B -- Univalence Intro equivToPath (A B: U): univ_Formation A B = \(p: equiv A B) -> Glue B [(i=0) -> (A,p), (i=1) -> (B, subst U (equiv B) B B (<_>B) (idEquiv B)) ] -- Univalence Elim pathToEquiv (A B: U) (p: Path U A B): equiv A B = subst U (equiv A) A B p (idEquiv A) -- Univalence Computation eqToEq (A B : U) (p : Path U A B) : Path (Path U A B) (equivToPath A B (pathToEquiv A B p)) p = let Ai: U = p@i in Glue B [ (i=0) -> (A,pathToEquiv A B p), (i=1) -> (B,pathToEquiv B B ( B)), (j=1) -> (p@i,pathToEquiv Ai B ( p @ (i \/ k))) ] -- Univalence Uniqueness transPathFun (A B : U) (w : equiv A B) : Path (A -> B) w.1 (pathToEquiv A B (equivToPath A B w)).1 = \ (a:A) -> let b: B = w.1 a u: A = comp (A) a [] q: Path B (w.1 u) b = w.1 (comp (A) a [(i=1) -> a]) in comp ( B) (comp ( B) (comp ( B) (comp ( B) (w.1 u) [(i=0)->q]) [(i=0)->b]) [(i=0)->b]) [(i=0)->b] idToPath (A B: U) (w: equiv A B) : Path (equiv A B) (pathToEquiv A B (equivToPath A B w)) w = equivLemma A B (pathToEquiv A B (equivToPath A B w)) w (transPathFun A B w@-i) isEquivContr (A B:U) (a: isContr A) (b:isContr B) (f:A->B) : isEquiv A B f = \(y:B) -> sigmaIsContr A (\ (x:A) -> Path B y (f x)) a (\ (x:A) -> isPathContr B b y (f x)) funFib1 (A:U) (B C: A -> U) (f: (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u: fiber (B x0) (C x0) (f x0) z0) : fiber (Sigma A B) (Sigma A C) (total A B C f) (x0,z0) = ((x0,u.1),(x0,u.2@i)) funFib2 (A:U) (B C: A -> U) (f: (x:A) -> B x -> C x) (x0:A) (z0:C x0) (w: fiber (Sigma A B) (Sigma A C) (total A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s) where x : A = w.1.1 b : B x = w.1.2 p : Path A x0 x = (w.2@i).1 q : PathP (C (p@i)) z0 (f x b) = (w.2@i).2 b0 : B x0 = comp (B (p@-i)) b [] r : PathP (B (p@-i)) b b0 = comp (B (p@-j\/-i)) b [(i=0) -> b] s : Path (C x0) z0 (f x0 b0) = comp (C (p@(i/\-j))) (q@i) [(i=0) -> z0, (i=1) -> f (p@-k) (r@k)] compFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u: fiber (B x0) (C x0) (f x0) z0) : fiber (B x0) (C x0) (f x0) z0 = funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u) retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u: fiber (B x0) (C x0) (f x0) z0) : Path (fiber (B x0) (C x0) (f x0) z0) (funFib2 A B C f x0 z0 (funFib1 A B C f x0 z0 u)) u = (comp ( B x0) u.1 [(l=1) -> u.1], comp ( C x0) (u.2 @ i) [(l=1) -> u.2 @ i, (i=0) -> z0, (i=1) -> f x0 (comp ( B x0) u.1 [(j=0) -> u.1, (l=1) -> u.1 ])]) equivFunFib (A: U) (B C: A -> U) (f: (x:A) -> B x -> C x) (cB: isContr (Sigma A B)) (cC: isContr (Sigma A C)) (x: A) : isEquiv (B x) (C x) (f x) = \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (Sigma A B) (Sigma A C) (total A B C f) (x,z)) (funFib1 A B C f x z) (funFib2 A B C f x z) (retFunFib A B C f x z) (isEquivContr (Sigma A B) (Sigma A C) cB cC (total A B C f) (x,z))