{- Category Theory: - Structure; - Structure Identity Principle. Copyright (c) Groupoid Infinity, 2014-2018. HoTT 9.8 The structure identity principle. -} module sip where import cat import prop import iso_sigma structure (X: precategory): U = (P: carrier X -> U) * (H: (x y: carrier X) (a: P x) (b: P y) (f: hom X x y) -> U) * (propH: (x y: carrier X) (a: P x) (b: P y) (f: hom X x y) -> isProp (H x y a b f)) * (Hid: (x: carrier X) (a: P x) -> H x x a a (path X x)) * ((x y z : carrier X) (a: P x) (b: P y) (c: P z) (f: hom X x y) (g: hom X y z) -> H x y a b f -> H y z b c g -> H x z a c (compose X x y z f g)) sP (X: precategory) (S: structure X): carrier X -> U = S.1 sH (X: precategory) (S: structure X): (x y: carrier X) -> (a: sP X S x) -> (b: sP X S y) -> (f: hom X x y) -> U = S.2.1 sHPath (X: precategory) (S: structure X): (x: carrier X) -> (a: sP X S x) -> sH X S x x a a (path X x) = S.2.2.2.1 sHProp (X: precategory) (S: structure X): (x y: carrier X) -> (a: sP X S x) -> (b: sP X S y) -> (f: hom X x y) -> isProp (sH X S x y a b f) = S.2.2.1 sHComp (X: precategory) (S: structure X): (x y z: carrier X) -> (a: sP X S x) -> (b: sP X S y) -> (c: sP X S z) -> (f: hom X x y) -> (g: hom X y z) -> sH X S x y a b f -> sH X S y z b c g -> sH X S x z a c (compose X x y z f g) = S.2.2.2.2 isStandardStructure (X: precategory) (S: structure X): U = (x: carrier X) -> (a b: sP X S x) -> sH X S x x a b (path X x) -> sH X S x x b a (path X x) -> Path (sP X S x) a b lemPathPProp (A B: U) (AProp: isProp A) (p: Path U A B): (x: A) -> (y: B) -> PathP p x y = J U A (\(B: U) -> \(p: Path U A B) -> (x: A) -> (y: B) -> PathP p x y) AProp B p lemPathPSet (A B: U) (ASet: isSet A) (p: Path U A B): (x : A) (y : B) (s t : PathP p x y) -> Path (PathP p x y) s t = J U A (\(B : U) -> \(p : Path U A B) -> (x : A) (y : B) (s t : PathP p x y) -> Path (PathP p x y) s t) ASet B p lemIsCategory (C: precategory) (isC: isCategory C) (A B: carrier C) (e: iso C A B): Path ((B: carrier C) * iso C A B) (A, idIso C A) (B, e) = (isContrProp ((B : carrier C) * iso C A B) (isC A) (A, idIso C A) (B, e) @ i) isContrProp (A:U) (p: isContr A) (x y: A): Path A x y = composition A x p.1 y ( p.2 x @ -i) (p.2 y) isContrSig (A:U) (B:A-> U) (cA:isContr A) (cB: (x:A) -> isContr (B x)) : isContr (Sigma A B) = ((cA.1, (cB cA.1).1),\(x:Sigma A B) -> propSig A B (isContrProp A cA) (\(x:A) -> isContrProp (B x) (cB x)) (cA.1, (cB cA.1).1) x) sipPrecategory (C: precategory) (S: structure C): precategory = ((Ob, Hom), (id, cmp, HomSet, idL, idR, idC')) where Ob: U = Sigma (carrier C) (sP C S) Hom (X Y: Ob) : U = (f: hom C X.1 Y.1) * sH C S X.1 Y.1 X.2 Y.2 f HomSet (X Y: Ob) : isSet (Hom X Y) = setSig (hom C X.1 Y.1) (sH C S X.1 Y.1 X.2 Y.2) (homSet C X.1 Y.1) (\(f: hom C X.1 Y.1) -> propSet (sH C S X.1 Y.1 X.2 Y.2 f) (sHProp C S X.1 Y.1 X.2 Y.2 f)) id (X: Ob): Hom X X = (path C X.1, sHPath C S X.1 X.2) cmp (x y z: Ob) (f: Hom x y) (g: Hom y z): Hom x z = (compose C x.1 y.1 z.1 f.1 g.1, sHComp C S x.1 y.1 z.1 x.2 y.2 z.2 f.1 g.1 f.2 g.2) idL (x y: Ob) (f: Hom x y) : Path (Hom x y) (cmp x x y (id x) f) f = (pathL C x.1 y.1 f.1 @ i, lemPathPProp (sH C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1) (sH C S x.1 y.1 x.2 y.2 f.1) (sHProp C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1) (sH C S x.1 y.1 x.2 y.2 (pathL C x.1 y.1 f.1 @ i)) (cmp x x y (id x) f).2 f.2 @ i) idR (x y: Ob) (f: Hom x y) : Path (Hom x y) (cmp x y y f (id y)) f = (pathR C x.1 y.1 f.1 @ i, lemPathPProp (sH C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1) (sH C S x.1 y.1 x.2 y.2 f.1) (sHProp C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1) (sH C S x.1 y.1 x.2 y.2 (pathR C x.1 y.1 f.1 @ i)) (cmp x y y f (id y)).2 f.2 @ i) idC' (x y z w: Ob) (f: Hom x y) (g: Hom y z) (h: Hom z w): Path (Hom x w) (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h)) = (pathC C x.1 y.1 z.1 w.1 f.1 g.1 h.1 @ i, lemPathPProp (sH C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1) (sH C S x.1 w.1 x.2 w.2 (cmp x y w f (cmp y z w g h)).1) (sHProp C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1) (sH C S x.1 w.1 x.2 w.2 (pathC C x.1y.1 z.1 w.1 f.1 g.1 h.1 @ i)) (cmp x z w (cmp x y z f g) h).2 (cmp x y w f (cmp y z w g h)).2 @ i) sip (X: precategory) (isC: isCategory X) (S: structure X) (isS: isStandardStructure X S): isCategory (sipPrecategory X S) = hole where D : precategory = sipPrecategory X S eq1 (A: carrier D): Path U ((B : carrier D) * iso D A B) ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) = isoPath ((B : carrier D) * iso D A B) ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) F G FG GF where F (C : (B : carrier D) * iso D A B) : ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) = ((C.1.1, C.2.1.1, C.2.2.1.1, (C.2.2.2.1@i).1, (C.2.2.2.2@i).1), C.1.2, C.2.1.2, C.2.2.1.2) G (C : ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)) : (B : carrier D) * iso D A B = ((C.1.1, C.2.1), (C.1.2.1, C.2.2.1), (C.1.2.2.1, C.2.2.2) , (C.1.2.2.2.1 @ i ,lemPathPProp (sH X S A.1 A.1 A.2 A.2 (compose X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1)) (sH X S A.1 A.1 A.2 A.2 (path X A.1)) (sHProp X S A.1 A.1 A.2 A.2 (compose X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1)) (sH X S A.1 A.1 A.2 A.2 (C.1.2.2.2.1 @ i)) (sHComp X S A.1 C.1.1 A.1 A.2 C.2.1 A.2 C.1.2.1 C.1.2.2.1 C.2.2.1 C.2.2.2) (sHPath X S A.1 A.2) @ i) , (C.1.2.2.2.2 @ i ,lemPathPProp (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (compose X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1)) (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (path X C.1.1)) (sHProp X S C.1.1 C.1.1 C.2.1 C.2.1 (compose X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1)) (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (C.1.2.2.2.2 @ i)) (sHComp X S C.1.1 A.1 C.1.1 C.2.1 A.2 C.2.1 C.1.2.2.1 C.1.2.1 C.2.2.2 C.2.2.1) (sHPath X S C.1.1 C.2.1) @ i)) FG (C : ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)) : Path ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) (F (G C)) C = <_> C GF (C : (B : carrier D) * iso D A B) : Path ((B : carrier D) * iso D A B) (G (F C)) C = (C.1, C.2.1, C.2.2.1 , ((C.2.2.2.1 @ j).1 ,lemPathPSet (sH X S A.1 A.1 A.2 A.2 (compose X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1)) (sH X S A.1 A.1 A.2 A.2 (path X A.1)) (propSet (sH X S A.1 A.1 A.2 A.2 (compose X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1)) (sHProp X S A.1 A.1 A.2 A.2 (compose X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1))) (sH X S A.1 A.1 A.2 A.2 (C.2.2.2.1 @ j).1) (sHComp X S A.1 C.1.1 A.1 A.2 C.1.2 A.2 C.2.1.1 C.2.2.1.1 C.2.1.2 C.2.2.1.2) (sHPath X S A.1 A.2) (((G (F C)).2.2.2.1 @ j).2) ((C.2.2.2.1 @ j).2) @i@j) , ((C.2.2.2.2 @ j).1 ,lemPathPSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (compose X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1)) (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (path X C.1.1)) (propSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (compose X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1)) (sHProp X S C.1.1 C.1.1 C.1.2 C.1.2 (compose X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1))) (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (C.2.2.2.2 @ j).1) (sHComp X S C.1.1 A.1 C.1.1 C.1.2 A.2 C.1.2 C.2.2.1.1 C.2.1.1 C.2.2.1.2 C.2.1.2) (sHPath X S C.1.1 C.1.2) (((G (F C)).2.2.2.2 @ j).2) ((C.2.2.2.2 @ j).2) @i@j)) hole0 (A : carrier D) : isContr ((C : (B1 : carrier X) * ( iso X A.1 B1)) * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) = isContrSig ((B1 : carrier X) * ( iso X A.1 B1)) (\(C : (B1 : carrier X) * ( iso X A.1 B1)) -> (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) (isC A.1) (\(C : (B1 : carrier X) * ( iso X A.1 B1)) -> let p : Path ((B1 : carrier X) * ( iso X A.1 B1)) (A.1, idIso X A.1) C = lemIsCategory X isC A.1 C.1 C.2 in transport ( isContr ((B2 : sP X S (p@i).1) * (_ : sH X S A.1 (p@i).1 A.2 B2 (p@i).2.1) * sH X S (p@i).1 A.1 B2 A.2 (p@i).2.2.1)) ((A.2,sHPath X S A.1 A.2,sHPath X S A.1 A.2) ,\(Y : (B2 : sP X S A.1) * (_ : sH X S A.1 A.1 A.2 B2 (path X A.1)) * sH X S A.1 A.1 B2 A.2 (path X A.1)) -> (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i ,lemPathPProp (sH X S A.1 A.1 A.2 A.2 (path X A.1)) (sH X S A.1 A.1 A.2 Y.1 (path X A.1)) (sHProp X S A.1 A.1 A.2 A.2 (path X A.1)) (sH X S A.1 A.1 A.2 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) (path X A.1)) (sHPath X S A.1 A.2) Y.2.1 @ i ,lemPathPProp (sH X S A.1 A.1 A.2 A.2 (path X A.1)) (sH X S A.1 A.1 Y.1 A.2 (path X A.1)) (sHProp X S A.1 A.1 A.2 A.2 (path X A.1)) (sH X S A.1 A.1 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) A.2 (path X A.1)) (sHPath X S A.1 A.2) Y.2.2 @ i))) hole (A : carrier D) : isContr ((B : carrier D) * iso D A B) = transport (isContr(eq1 A@-i)) (hole0 A)