{- Set Theory: - Injectivity; Copyright (c) Groupoid Infinity, 2014-2018. HoTT 3.1 Sets and n-types -} module set where import proto import path import prop import pi import sigma import equiv -- Contractible is a Prop setIsProp (A : U) : isProp (isSet A) = \(f g : isSet A) -> \(a b :A) -> propIsProp (Path A a b) (f a b) (g a b) @ i setUnit : isSet unit = propSet unit propUnit setInj (A B : U) (f : A -> B) (sA : isSet A) (sB : isSet B) : U = (b : B) -> isProp ((a : A) * Path B (f a) b) prop_inj (A B: U) (f: A -> B) (sA: isSet A) (sB: isSet B): isProp (setInj A B f sA sB) = propPi B Q h where P: B -> U = \(b: B) -> (a: A) * Path B (f a) b Q: B -> U = \(b: B) -> isProp (P b) h: (b: B) -> isProp (Q b) = \(b: B) -> propIsProp (P b) {- sqDepPath (A:U) (F:A->U) (sF: (x:A) -> (F x)) (a0 a1:A) (p: Path A a0 a1) (u0 : F a0) (u1 : F a1) (q r : PathP ( F (p@i)) u0 u1) : Path (PathP ( F (p@i)) u0 u1) q r = rem @ j @ i where rem : PathP ( Path (F (p@i)) (q@i) (r@i)) (u0) (u1) = let xi : A = p@i ui0 : F xi = transport (F (p @ i/\j)) u0 ui1 : F xi = transport (F (p @ i\/-j)) u1 qi : Id (F xi) ui0 ui1 = transport (F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (q@j) ri : Id (F xi) ui0 ui1 = transport (F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j) in (sF xi ui0 ui1 qi ri @ j @ i) -}