Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(** * Classification of path spaces of precategories *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics.Require Import HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall.Require Import HoTT.Tactics.Set Universe Polymorphism.Set Implicit Arguments.Generalizable All Variables.Set Asymmetric Patterns.LocalOpen Scope morphism_scope.LocalOpen Scope category_scope.Sectionpath_category.LocalOpen Scope path_scope.(** We add a prime ([']) as an arbitrary convention to denote that we are talking about equality of functions (less convenient for use) rather than pointwise equality of functions (more convenient for use, but more annoying for proofs). We add two primes to denote the even less convenient version, which requires an identity equality proof. *)Local Notationpath_precategory''_T C D
:= { Hobj : object C = object D
| { Hmor : transport (funobj => obj -> obj -> Type)
Hobj
(morphism C)
= morphism D
| transport _
Hmor
(transportD (funobj => obj -> obj -> Type)
(funobjmor => forallsdd', mor d d' -> mor s d -> mor s d')
Hobj
(morphism C)
(@compose C))
= @compose D
/\ transport _
Hmor
(transportD (funobj => obj -> obj -> Type)
(funobjmor => forallx, mor x x)
Hobj
(morphism C)
(@identity C))
= @identity D }}.Local Notationpath_precategory'_T C D
:= { Hobj : object C = object D
| { Hmor : transport (funobj => obj -> obj -> Type)
Hobj
(morphism C)
= morphism D
| transport _
Hmor
(transportD (funobj => obj -> obj -> Type)
(funobjmor => forallsdd', mor d d' -> mor s d -> mor s d')
Hobj
(morphism C)
(@compose C))
= @compose D }}.(** ** Classify sufficient conditions to prove precategories equal *)
H: Funext C, D: PreCategory Heq: path_precategory'_T C D
transport
(funmor : (funobj : Type => obj -> obj -> Type) D
=> forallx : D, mor x x) (Heq.2).1
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallx : obj, mor x x) Heq.1 (morphism C)
identity) = identity
H: Funext C, D: PreCategory Heq: path_precategory'_T C D
transport
(funmor : (funobj : Type => obj -> obj -> Type) D
=> forallx : D, mor x x) (Heq.2).1
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallx : obj, mor x x) Heq.1 (morphism C)
identity) = identity
H: Funext C, D: PreCategory proj1: C = D proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
(morphism C) = morphism D proj2: transport
(funmor : D -> D -> Type =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
(morphism C) (@compose C)) =
@compose D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
proj0
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) proj1 (morphism C)
identity) = identity
H: Funext C, D: PreCategory proj1: C = D proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
(morphism C) = morphism D proj2: transport
(funmor : D -> D -> Type =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
(morphism C) (@compose C)) =
@compose D x: D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
proj0
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) proj1 (morphism C)
identity) x = 1%morphism
H: Funext C, D: PreCategory proj1: C = D proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
(morphism C) = morphism D proj2: transport
(funmor : D -> D -> Type =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
(morphism C) (@compose C)) =
@compose D x: D
forall (sd : D) (m : morphism D s d),
m
o transport
(funmor : D -> D -> Type => forallx : D, mor x x)
proj0
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) proj1 (morphism C)
identity) s = m
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) object0: Type morphism0: object0 -> object0 -> Type identity0: forallx : object0, morphism0 x x compose0: forallsdd' : object0,
morphism0 d d' ->
morphism0 s d -> morphism0 s d' associativity0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a b b (identity0 b) f = f right_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a a b f (identity0 a) = f identity_identity0: forallx : object0,
compose0 x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object0,
IsHSet (morphism0 s d) proj1: object = object0 proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
morphism = morphism0 proj2: transport
(funmor : object0 -> object0 -> Type =>
forallsdd' : object0,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
morphism compose) = compose0 x: object0
forall (sd : object0) (m : morphism0 s d),
compose0 s s d m
(transport
(funmor : object0 -> object0 -> Type =>
forallx : object0, mor x x) proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=> forallx : obj, mor x x) proj1 morphism
identity) s) = m
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) identity0: forallx : object, morphism x x associativity0: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object)
(f : morphism a b),
compose a b b (identity0 b) f = f right_identity0: forall (ab : object)
(f : morphism a b),
compose a a b f (identity0 a) = f identity_identity0: forallx : object,
compose x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object,
IsHSet (morphism s d) x, s, d: object m: morphism s d
compose s s d m (identity s) = m
auto.Qed.Definitionpath_precategory''_T__of__path_precategory'_T `{Funext} C D
: path_precategory'_T C D -> path_precategory''_T C D
:= funH => (H.1; (H.2.1; (H.2.2, path_precategory_uncurried__identity_helper C D H))).
A: Type B: A -> Type P, Q: forallx : A, B x -> Type H: forall (a : A) (b : B a), IsHProp (Q a b) x: {a : A & {b : B a & P a b * Q a b}} q': Q x.1 (x.2).1
(x.1; (x.2).1; (fst (x.2).2, q')) = x
A: Type B: A -> Type P, Q: forallx : A, B x -> Type H: forall (a : A) (b : B a), IsHProp (Q a b) x: {a : A & {b : B a & P a b * Q a b}} q': Q x.1 (x.2).1
(x.1; (x.2).1; (fst (x.2).2, q')) = x
A: Type B: A -> Type P, Q: forallx : A, B x -> Type H: forall (a : A) (b : B a), IsHProp (Q a b) proj1: A proj0: B proj1 fst: P proj1 proj0 snd, q': Q proj1 proj0
repeat f_ap; apply path_ishprop.Defined.Global Instanceisequiv__path_precategory''_T__of__path_precategory'_T `{fs : Funext} C D
: IsEquiv (@path_precategory''_T__of__path_precategory'_T fs C D)
:= isequiv_adjointify
(@path_precategory''_T__of__path_precategory'_T fs C D)
(funH => (H.1; (H.2.1; fst H.2.2)))
(funx => eta2_sigma_helper _ _ _ x _)
eta2_sigma.
fs: Funext C, D: PreCategory
path_precategory''_T C D -> C = D
fs: Funext C, D: PreCategory
path_precategory''_T C D -> C = D
fs: Funext C, D: PreCategory proj1: C = D proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
(morphism C) = morphism D fst: transport
(funmor : D -> D -> Type =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
(morphism C) (@compose C)) =
@compose D snd: transport
(funmor : D -> D -> Type =>
forallx : D, mor x x) proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallx : obj, mor x x) proj1
(morphism C) identity) = identity
C = D
fs: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) object0: Type morphism0: object0 -> object0 -> Type identity0: forallx : object0, morphism0 x x compose0: forallsdd' : object0,
morphism0 d d' ->
morphism0 s d -> morphism0 s d' associativity0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a b b (identity0 b) f = f right_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a a b f (identity0 a) = f identity_identity0: forallx : object0,
compose0 x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object0,
IsHSet (morphism0 s d) proj1: object = object0 proj0: transport
(funobj : Type => obj -> obj -> Type) proj1
morphism = morphism0 fst: transport
(funmor : object0 -> object0 -> Type =>
forallsdd' : object0,
mor d d' -> mor s d -> mor s d') proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') proj1
morphism compose) = compose0 snd: transport
(funmor : object0 -> object0 -> Type =>
forallx : object0, mor x x) proj0
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallx : obj, mor x x) proj1 morphism
identity) = identity0
H: Funext C, D: PreCategory HO: C = D HM: transport (funobj : Type => obj -> obj -> Type)
HO (morphism C) = morphism D HC: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') HO
(morphism C) (@compose C)) = @compose D HI: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D => forallx : D, mor x x) HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallx : obj, mor x x) HO (morphism C)
identity) = identity
ap object
(path_precategory_uncurried' C D (HO; HM; (HC, HI))) =
HO
H: Funext C, D: PreCategory HO: C = D HM: transport (funobj : Type => obj -> obj -> Type)
HO (morphism C) = morphism D HC: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') HO
(morphism C) (@compose C)) = @compose D HI: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D => forallx : D, mor x x) HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallx : obj, mor x x) HO (morphism C)
identity) = identity
ap object
(path_precategory_uncurried' C D (HO; HM; (HC, HI))) =
HO
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) object0: Type morphism0: object0 -> object0 -> Type identity0: forallx : object0, morphism0 x x compose0: forallsdd' : object0,
morphism0 d d' ->
morphism0 s d -> morphism0 s d' associativity0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a b b (identity0 b) f = f right_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a a b f (identity0 a) = f identity_identity0: forallx : object0,
compose0 x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object0,
IsHSet (morphism0 s d) HO: object = object0 HM: transport (funobj : Type => obj -> obj -> Type)
HO morphism = morphism0 HC: transport
(funmor : object0 -> object0 -> Type =>
forallsdd' : object0,
mor d d' -> mor s d -> mor s d') HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') HO
morphism compose) = compose0 HI: transport
(funmor : object0 -> object0 -> Type =>
forallx : object0, mor x x) HM
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=> forallx : obj, mor x x) HO morphism
identity) = identity0
path_induction_hammer.Qed.(** *** Said proof respects [idpath] *)
H: Funext C: PreCategory
path_precategory_uncurried' C C (1; 1; (1, 1)) = 1
H: Funext C: PreCategory
path_precategory_uncurried' C C (1; 1; (1, 1)) = 1
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d)
ap11
(ap11
(ap11
(ap11
(ap11
match
center (associativity = associativity)
in (_ = a)
return
(Build_PreCategory' morphism
identity compose associativity =
Build_PreCategory' morphism
identity compose a)
with
| 1 => 1end
(center
(associativity_sym =
associativity_sym)))
(center (left_identity = left_identity)))
(center (right_identity = right_identity)))
(center (identity_identity = identity_identity)))
(center (trunc_morphism = trunc_morphism)) = 1
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d)
ap11 (ap11 (ap11 (ap11 (ap11 11) 1) 1) 1) 1 = 1
reflexivity.Qed.(** ** Equality of precategorys gives rise to an inhabitant of the path-classifying-type *)
C, D: PreCategory
C = D -> path_precategory''_T C D
C, D: PreCategory
C = D -> path_precategory''_T C D
C, D: PreCategory H': C = D
path_precategory''_T C D
C, D: PreCategory H': C = D
{Hmor
: transport (funobj : Type => obj -> obj -> Type)
(ap object H') (morphism C) = morphism D &
(transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') (ap object H')
(morphism C) (@compose C)) = @compose D) *
(transport
(funmor : D -> D -> Type => forallx : D, mor x x)
Hmor
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) (ap object H')
(morphism C) identity) = identity)}
C, D: PreCategory H': C = D
(transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
((transport_compose
(funobj : Type => obj -> obj -> Type) object
H' (morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') (ap object H')
(morphism C) (@compose C)) = @compose D) *
(transport
(funmor : D -> D -> Type => forallx : D, mor x x)
((transport_compose
(funobj : Type => obj -> obj -> Type) object
H' (morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) (ap object H')
(morphism C) identity) = identity)
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') (ap object H')
(morphism C) (@compose C)) = @compose D
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) (ap object H')
(morphism C) identity) = identity
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') (ap object H')
(morphism C) (@compose C)) = @compose D
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') (ap object H')
(morphism C) (@compose C)) =
transport
(funC : PreCategory =>
forallsdd' : C,
morphism C d d' ->
morphism C s d -> morphism C s d') H' (@compose C)
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
(apD morphism H')
(transport
(funmor : D -> D -> Type =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d')
(transport_compose
(funobj : Type => obj -> obj -> Type) object
H' (morphism C))^
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
(ap object H') (morphism C) (@compose C))) =
transport
(funC : PreCategory =>
forallsdd' : C,
morphism C d d' ->
morphism C s d -> morphism C s d') H' (@compose C)
refine ((ap _ (transportD_compose
(funobj => obj -> obj -> Type)
(funobjmor =>
forallsdd' : obj, mor d d' -> mor s d -> mor s d') object H'
(morphism C) (@compose C))^)
@ (transport_apD_transportD
_
morphism
(funxmor => forallsdd' : x, mor d d' -> mor s d -> mor s d') H'
(@compose C))).
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) (ap object H')
(morphism C) identity) = identity
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
((transport_compose
(funobj : Type => obj -> obj -> Type) object H'
(morphism C))^ @ apD morphism H')
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallx : obj, mor x x) (ap object H')
(morphism C) identity) =
transport
(funC : PreCategory => forallx : C, morphism C x x)
H' identity
C, D: PreCategory H': C = D
transport
(funmor : D -> D -> Type => forallx : D, mor x x)
(apD morphism H')
(transport
(funmor : D -> D -> Type =>
forallx : D, mor x x)
(transport_compose
(funobj : Type => obj -> obj -> Type) object
H' (morphism C))^
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=> forallx : obj, mor x x) (ap object H')
(morphism C) identity)) =
transport
(funC : PreCategory => forallx : C, morphism C x x)
H' identity
refine ((ap _ (transportD_compose
(funobj => obj -> obj -> Type)
(funobjmor =>
forallx : obj, mor x x) object H'
(morphism C) (@identity C))^)
@ (transport_apD_transportD
_
morphism
(funxmor => foralls : x, mor s s) H'
(@identity C))).Defined.(** ** Classify equality of precategorys up to equivalence *)
H: Funext C, D: PreCategory
forallx : path_precategory''_T C D,
path_precategory_uncurried'_inv
(path_precategory_uncurried' C D x) = x
H: Funext C, D: PreCategory
forallx : path_precategory''_T C D,
path_precategory_uncurried'_inv
(path_precategory_uncurried' C D x) = x
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) object0: Type morphism0: object0 -> object0 -> Type identity0: forallx : object0, morphism0 x x compose0: forallsdd' : object0,
morphism0 d d' ->
morphism0 s d -> morphism0 s d' associativity0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a b b (identity0 b) f = f right_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a a b f (identity0 a) = f identity_identity0: forallx : object0,
compose0 x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object0,
IsHSet (morphism0 s d)
forallx : {Hobj : object = object0 &
{Hmor
: transport (funobj : Type => obj -> obj -> Type)
Hobj morphism = morphism0 &
(transport
(funmor : object0 -> object0 -> Type =>
forallsdd' : object0,
mor d d' -> mor s d -> mor s d') Hmor
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
morphism compose) = compose0) *
(transport
(funmor : object0 -> object0 -> Type =>
forallx : object0, mor x x) Hmor
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type)
=> forallx : obj, mor x x) Hobj morphism
identity) = identity0)}},
path_precategory_uncurried'_inv
(path_precategory_uncurried'
{|
object := object;
morphism := morphism;
identity := identity;
compose := compose;
associativity := associativity;
associativity_sym := associativity_sym;
left_identity := left_identity;
right_identity := right_identity;
identity_identity := identity_identity;
trunc_morphism := trunc_morphism
|}
{|
object := object0;
morphism := morphism0;
identity := identity0;
compose := compose0;
associativity := associativity0;
associativity_sym := associativity_sym0;
left_identity := left_identity0;
right_identity := right_identity0;
identity_identity := identity_identity0;
trunc_morphism := trunc_morphism0
|} x) = x
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) object0: Type morphism0: object0 -> object0 -> Type identity0: forallx : object0, morphism0 x x compose0: forallsdd' : object0,
morphism0 d d' ->
morphism0 s d -> morphism0 s d' associativity0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 =
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) associativity_sym0: forall (x1x2x3x4 : object0)
(m1 : morphism0 x1 x2)
(m2 : morphism0 x2 x3)
(m3 : morphism0 x3 x4),
compose0 x1 x3 x4 m3
(compose0 x1 x2 x3 m2 m1) =
compose0 x1 x2 x4
(compose0 x2 x3 x4 m3 m2) m1 left_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a b b (identity0 b) f = f right_identity0: forall (ab : object0)
(f : morphism0 a b),
compose0 a a b f (identity0 a) = f identity_identity0: forallx : object0,
compose0 x x x (identity0 x)
(identity0 x) = identity0 x trunc_morphism0: forallsd : object0,
IsHSet (morphism0 s d) H0': object = object0 H1': transport (funobj : Type => obj -> obj -> Type)
H0' morphism = morphism0 H2': transport
(funmor : object0 -> object0 -> Type =>
forallsdd' : object0,
mor d d' -> mor s d -> mor s d') H1'
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') H0'
morphism compose) = compose0 H3': transport
(funmor : object0 -> object0 -> Type =>
forallx : object0, mor x x) H1'
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallx : obj, mor x x) H0' morphism
identity) = identity0
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) left_identity0: forall (ab : object)
(f : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism a b),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) a b b
(transport
(funmor : object ->
object -> Type =>
forallx : object, mor x x) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=> forallx : obj, mor x x)
1 morphism identity) b) f = f right_identity0: forall (ab : object)
(f : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism a b),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) a a b f
(transport
(funmor : object ->
object -> Type =>
forallx : object, mor x x) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=> forallx : obj, mor x x)
1 morphism identity) a) = f identity_identity0: forallx : object,
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x x x
(transport
(funmor : object ->
object -> Type =>
forallx0 : object,
mor x0 x0) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallx0 : obj,
mor x0 x0) 1 morphism
identity) x)
(transport
(funmor : object ->
object -> Type =>
forallx0 : object,
mor x0 x0) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallx0 : obj,
mor x0 x0) 1 morphism
identity) x) =
transport
(funmor : object ->
object -> Type =>
forallx0 : object, mor x0 x0)
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallx0 : obj, mor x0 x0)
1 morphism identity) x associativity0: forall (x1x2x3x4 : object)
(m1 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x1 x2)
(m2 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x2 x3)
(m3 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x3 x4),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) x1 x2 x4
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x2 x3 x4 m3
m2) m1 =
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) x1 x3 x4 m3
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2 x3 m2
m1) associativity_sym0: forall (x1x2x3x4 : object)
(m1 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x1 x2)
(m2 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x2 x3)
(m3 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x3 x4),
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x3 x4
m3
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2
x3 m2 m1) =
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2 x4
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x2 x3
x4 m3 m2) m1 trunc_morphism0: forallsd : object,
IsHSet
(transport
(funobj : Type =>
obj -> obj -> Type) 1 morphism
s d)
path_precategory_uncurried'_inv
(path_precategory_uncurried'
{|
object := object;
morphism := morphism;
identity := identity;
compose := compose;
associativity := associativity;
associativity_sym := associativity_sym;
left_identity := left_identity;
right_identity := right_identity;
identity_identity := identity_identity;
trunc_morphism := trunc_morphism
|}
{|
object := object;
morphism :=
transport
(funobj : Type => obj -> obj -> Type) 1
morphism;
identity :=
transport
(funmor : object -> object -> Type =>
forallx : object, mor x x) 1
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallx : obj, mor x x) 1 morphism
identity);
compose :=
transport
(funmor : object -> object -> Type =>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') 1
morphism compose);
associativity := associativity0;
associativity_sym := associativity_sym0;
left_identity := left_identity0;
right_identity := right_identity0;
identity_identity := identity_identity0;
trunc_morphism := trunc_morphism0
|} (1; 1; (1, 1))) = (1; 1; (1, 1))
H: Funext object: Type morphism: object -> object -> Type identity: forallx : object, morphism x x compose: forallsdd' : object,
morphism d d' ->
morphism s d -> morphism s d' associativity: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 =
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) associativity_sym: forall (x1x2x3x4 : object)
(m1 : morphism x1 x2)
(m2 : morphism x2 x3)
(m3 : morphism x3 x4),
compose x1 x3 x4 m3
(compose x1 x2 x3 m2 m1) =
compose x1 x2 x4
(compose x2 x3 x4 m3 m2) m1 left_identity: forall (ab : object)
(f : morphism a b),
compose a b b (identity b) f = f right_identity: forall (ab : object)
(f : morphism a b),
compose a a b f (identity a) = f identity_identity: forallx : object,
compose x x x (identity x)
(identity x) = identity x trunc_morphism: forallsd : object,
IsHSet (morphism s d) left_identity0: forall (ab : object)
(f : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism a b),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) a b b
(transport
(funmor : object ->
object -> Type =>
forallx : object, mor x x) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=> forallx : obj, mor x x)
1 morphism identity) b) f = f right_identity0: forall (ab : object)
(f : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism a b),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) a a b f
(transport
(funmor : object ->
object -> Type =>
forallx : object, mor x x) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=> forallx : obj, mor x x)
1 morphism identity) a) = f identity_identity0: forallx : object,
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x x x
(transport
(funmor : object ->
object -> Type =>
forallx0 : object,
mor x0 x0) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallx0 : obj,
mor x0 x0) 1 morphism
identity) x)
(transport
(funmor : object ->
object -> Type =>
forallx0 : object,
mor x0 x0) 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallx0 : obj,
mor x0 x0) 1 morphism
identity) x) =
transport
(funmor : object ->
object -> Type =>
forallx0 : object, mor x0 x0)
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallx0 : obj, mor x0 x0)
1 morphism identity) x associativity0: forall (x1x2x3x4 : object)
(m1 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x1 x2)
(m2 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x2 x3)
(m3 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x3 x4),
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) x1 x2 x4
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x2 x3 x4 m3
m2) m1 =
transport
(funmor : object -> object -> Type
=>
forallsdd' : object,
mor d d' -> mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d')
1 morphism compose) x1 x3 x4 m3
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' -> mor s d -> mor s d')
1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2 x3 m2
m1) associativity_sym0: forall (x1x2x3x4 : object)
(m1 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x1 x2)
(m2 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x2 x3)
(m3 : transport
(funobj : Type =>
obj -> obj -> Type) 1
morphism x3 x4),
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x3 x4
m3
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2
x3 m2 m1) =
transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj -> obj -> Type)
=>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x1 x2 x4
(transport
(funmor : object ->
object -> Type =>
forallsdd' : object,
mor d d' ->
mor s d -> mor s d') 1
(transportD
(funobj : Type =>
obj -> obj -> Type)
(fun (obj : Type)
(mor : obj ->
obj -> Type) =>
forallsdd' : obj,
mor d d' ->
mor s d -> mor s d') 1
morphism compose) x2 x3
x4 m3 m2) m1 trunc_morphism0: forallsd : object,
IsHSet
(transport
(funobj : Type =>
obj -> obj -> Type) 1 morphism
s d)
path_precategory_uncurried'_inv
(ap11
(ap11
(ap11
(ap11
(ap11
match
center
(associativity = associativity0)
in (_ = a)
return
(Build_PreCategory' morphism
identity compose associativity =
Build_PreCategory' morphism
identity compose a)
with
| 1 => 1end
(center
(associativity_sym =
associativity_sym0)))
(center (left_identity = left_identity0)))
(center (right_identity = right_identity0)))
(center
(identity_identity = identity_identity0)))
(center (trunc_morphism = trunc_morphism0))) =
(1; 1; (1, 1))
(funx : C = D =>
path_precategory_uncurried' C D
(path_precategory_uncurried'_inv x)) == idmap
H: Funext C, D: PreCategory
(funx : path_precategory''_T C D =>
path_precategory_uncurried'_inv
(path_precategory_uncurried' C D x)) == idmap
H: Funext C, D: PreCategory
(funx : C = D =>
path_precategory_uncurried' C D
(path_precategory_uncurried'_inv x)) == idmap
H: Funext C, D: PreCategory
forallx : C = D,
path_precategory_uncurried' C D
(path_precategory_uncurried'_inv x) = x
H: Funext C, D: PreCategory
path_precategory_uncurried' C C
(path_precategory_uncurried'_inv 1) = 1
apply path_precategory_uncurried'_idpath.
H: Funext C, D: PreCategory
(funx : path_precategory''_T C D =>
path_precategory_uncurried'_inv
(path_precategory_uncurried' C D x)) == idmap
H: Funext C, D: PreCategory
forallx : path_precategory''_T C D,
path_precategory_uncurried'_inv
(path_precategory_uncurried' C D x) = x
apply equiv_path_precategory_uncurried'__eissect.Defined.Definitionequiv_path_precategory_uncurried `{Funext} (C D : PreCategory)
: path_precategory'_T C D <~> C = D
:= ((equiv_path_precategory_uncurried' C D)
oE (Build_Equiv
_ _ _
(isequiv__path_precategory''_T__of__path_precategory'_T C D))).Definitionpath_precategory_uncurried `{Funext} C D : _ -> _
:= equiv_path_precategory_uncurried C D.(** ** Curried version of path classifying lemma *)
fs: Funext C, D: PreCategory
forall (Hobj : C = D)
(Hmor : transport
(funobj : Type => obj -> obj -> Type) Hobj
(morphism C) = morphism D),
transport
(funmor : (funobj : Type => obj -> obj -> Type) D
=>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) = @compose D -> C = D
fs: Funext C, D: PreCategory
forall (Hobj : C = D)
(Hmor : transport
(funobj : Type => obj -> obj -> Type) Hobj
(morphism C) = morphism D),
transport
(funmor : (funobj : Type => obj -> obj -> Type) D
=>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) = @compose D -> C = D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: transport
(funobj : Type => obj -> obj -> Type) Hobj
(morphism C) = morphism D X: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') Hmor
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) =
@compose D
C = D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: transport
(funobj : Type => obj -> obj -> Type) Hobj
(morphism C) = morphism D X: transport
(funmor : (funobj : Type => obj -> obj -> Type)
D =>
forallsdd' : D,
mor d d' -> mor s d -> mor s d') Hmor
(transportD
(funobj : Type => obj -> obj -> Type)
(fun (obj : Type)
(mor : (funobj0 : Type =>
obj0 -> obj0 -> Type) obj) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) =
@compose D
path_precategory'_T C D
repeatesplit; eassumption.Defined.(** ** Curried version of path classifying lemma, using [forall] in place of equality of functions *)
fs: Funext C, D: PreCategory
forall (Hobj : C = D)
(Hmor : forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) = morphism D s d),
(forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') = m o m') ->
C = D
fs: Funext C, D: PreCategory
forall (Hobj : C = D)
(Hmor : forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) = morphism D s d),
(forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') = m o m') ->
C = D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d Hcomp: forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') =
m o m'
C = D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d Hcomp: forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') =
m o m' Hmor':= path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C)) (morphism D)
(funs : D =>
path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C) s) (morphism D s)
(fund : D =>
((ap10
(transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s))
d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @
Hmor s d)): transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C) = morphism D
C = D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d Hcomp: forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') =
m o m' Hmor':= path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C)) (morphism D)
(funs : D =>
path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C) s) (morphism D s)
(fund : D =>
((ap10
(transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s))
d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @
Hmor s d)): transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C) = morphism D
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor'
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) = @compose D
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d Hcomp: forall (sdd' : D) (m : morphism D d d')
(m' : morphism D s d),
transport idmap (Hmor s d')
(transport idmap (Hmor d d')^ m
o transport idmap (Hmor s d)^ m') =
m o m' Hmor':= path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C)) (morphism D)
(funs : D =>
path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C) s) (morphism D s)
(fund : D =>
((ap10
(transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s))
d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @
Hmor s d)): transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C) = morphism D x, x0, x1: D x2: morphism D x0 x1 x3: morphism D x x0
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor'
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) x x0 x1 x2 x3 =
x2 o x3
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d Hmor':= path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C)) (morphism D)
(funs : D =>
path_forall
(transport
(funx : Type =>
idmap x ->
(funx0 : Type => x0 -> Type) x) Hobj
(morphism C) s) (morphism D s)
(fund : D =>
((ap10
(transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s))
d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @
Hmor s d)): transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C) = morphism D x, x0, x1: D x2: morphism D x0 x1 x3: morphism D x x0
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
Hmor'
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) x x0 x1 x2 x3 =
transport idmap (Hmor x x1)
(transport idmap (Hmor x0 x1)^ x2
o transport idmap (Hmor x x0)^ x3)
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d x, x0, x1: D x2: morphism D x0 x1 x3: morphism D x x0
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
(path_forall
(transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C)) (morphism D)
(funs : D =>
path_forall
(transport
(funx : Type =>
idmap x -> (funx0 : Type => x0 -> Type) x)
Hobj (morphism C) s) (morphism D s)
(fund : D =>
((ap10 (transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s)) d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @ Hmor s d)))
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) x x0 x1 x2 x3 =
transport idmap (Hmor x x1)
(transport idmap (Hmor x0 x1)^ x2
o transport idmap (Hmor x x0)^ x3)
fs: Funext C, D: PreCategory Hobj: C = D Hmor: forallsd : D,
morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d) =
morphism D s d x, x0, x1: D x2: morphism D x0 x1 x3: morphism D x x0
transport
(funmor : D -> D -> Type =>
forallsdd' : D, mor d d' -> mor s d -> mor s d')
(path_forall
(transport (funx : Type => x -> x -> Type) Hobj
(morphism C)) (morphism D)
(funs : D =>
path_forall
(transport (funx : Type => x -> x -> Type)
Hobj (morphism C) s) (morphism D s)
(fund : D =>
((ap10 (transport_arrow Hobj (morphism C) s)
d @
transport_arrow Hobj
(morphism C (transport idmap Hobj^ s)) d) @
transport_const Hobj
(morphism C (transport idmap Hobj^ s)
(transport idmap Hobj^ d))) @ Hmor s d)))
(transportD (funobj : Type => obj -> obj -> Type)
(fun (obj : Type) (mor : obj -> obj -> Type) =>
forallsdd' : obj,
mor d d' -> mor s d -> mor s d') Hobj
(morphism C) (@compose C)) x x0 x1 x2 x3 =
transport idmap (Hmor x x1)
(transport idmap (Hmor x0 x1)^ x2
o transport idmap (Hmor x x0)^ x3)
abstract (
destruct C, D;
cbnin *;
destruct Hobj;
cbnin *;
repeatmatch goal with
| _ => reflexivity
| _ => rewrite !concat_1p
| _ => rewrite !transport_forall_constant, !transport_arrow
| _ => progress transport_path_forall_hammer
| [ |- transport ?P?p^ ?u = ?v ]
=> (apply (@moveR_transport_V _ P _ _ p u v); progress transport_path_forall_hammer)
| [ |- ?u = transport ?P?p^ ?v ]
=> (apply (@moveL_transport_V _ P _ _ p u v); progress transport_path_forall_hammer)
| [ |- context[?H?x?y] ]
=> (destruct (H x y); clear H)
| _ => progress f_ap
end
).Defined.Endpath_category.(** ** Tactic for proving equality of precategories *)(** We move the funext inference outside the loop. *)Ltacpath_category :=
idtac;
letlem := constr:(@path_precategory _) inrepeatmatch goal with
| _ => intro
| _ => reflexivity
| _ => simple refine (lem _ _ _ _ _); cbnend.