HoTT.Categories.Category.Paths.v.alectryon.json

(** * Classification of path spaces of precategories *)
Require Import Category.Core.
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 Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.
Local Open Scope category_scope.

Section path_category.
  Local Open 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 Notation path_precategory''_T C D
    := { Hobj : object C = object D
       | { Hmor : transport (fun obj => obj -> obj -> Type)
                            Hobj
                            (morphism C)
                  = morphism D
         | transport _
                     Hmor
                     (transportD (fun obj => obj -> obj -> Type)
                                 (fun obj mor => forall s d d', mor d d' -> mor s d -> mor s d')
                                 Hobj
                                 (morphism C)
                                 (@compose C))
           = @compose D
           /\ transport _
                        Hmor
                        (transportD (fun obj => obj -> obj -> Type)
                                    (fun obj mor => forall x, mor x x)
                                    Hobj
                                    (morphism C)
                                    (@identity C))
              = @identity D }}.

  Local Notation path_precategory'_T C D
    := { Hobj : object C = object D
       | { Hmor : transport (fun obj => obj -> obj -> Type)
                            Hobj
                            (morphism C)
                  = morphism D
         | transport _
                     Hmor
                     (transportD (fun obj => obj -> obj -> Type)
                                 (fun obj mor => forall s d d', mor d d' -> mor s d -> mor s d')
                                 Hobj
                                 (morphism C)
                                 (@compose C))
           = @compose D }}.

  (** ** Classify sufficient conditions to prove precategories equal *)
  Lemma path_precategory_uncurried__identity_helper `{Funext} (C D : PreCategory)
        (Heq : path_precategory'_T C D)
  : transport _
              Heq.2.1
              (transportD (fun obj => obj -> obj -> Type)
                          (fun obj mor => forall x, mor x x)
                          Heq.1
                          (morphism C)
                          (@identity C))
    = @identity D.H: Funext
C, D: PreCategory
Heq: path_precategory'_T C D
transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall x : D, mor x x)
  (Heq.2).1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall x : obj, mor x x)
     Heq.1 (morphism C) identity) =
identity
  Proof.H: Funext
C, D: PreCategory
Heq: path_precategory'_T C D
transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall x : D, mor x x)
  (Heq.2).1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall x : obj, mor x x)
     Heq.1 (morphism C) identity) =
identity
    destruct Heq as [? [? ?]]; cbn in *.H: Funext
C, D: PreCategory
proj1: C = D
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 (morphism C) =
morphism D
proj2: transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 (morphism C) (@compose C)) =
@compose D
transport (fun mor : D -> D -> Type => forall x : D, mor x x) proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     proj1 (morphism C) identity) =
identity
    repeat (intro || apply path_forall).H: Funext
C, D: PreCategory
proj1: C = D
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 (morphism C) =
morphism D
proj2: transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 (morphism C) (@compose C)) =
@compose D
x: D
transport (fun mor : D -> D -> Type => forall x0 : D, mor x0 x0) proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall x0 : obj, mor x0 x0)
     proj1 (morphism C) identity)
  x =
1%morphism
    apply identity_unique; cbn in *; auto with morphism.H: Funext
C, D: PreCategory
proj1: C = D
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 (morphism C) =
morphism D
proj2: transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 (morphism C) (@compose C)) =
@compose D
x: D
forall (s d : D) (m : morphism D s d),
m
o transport (fun mor : D -> D -> Type => forall x0 : D, mor x0 x0) proj0
    (transportD (fun obj : Type => obj -> obj -> Type)
       (fun (obj : Type) (mor : obj -> obj -> Type) =>
        forall x0 : obj, mor x0 x0)
       proj1 (morphism C) identity)
    s =
m
    destruct C, D; cbn in *.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x0 : object, morphism x0 x0
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x0 : object,
compose x0 x0 x0 (identity x0) (identity x0) = identity x0
trunc_morphism: forall s d : object, IsHSet (morphism s d)
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x0 : object0, morphism0 x0 x0
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x0 : object0,
compose0 x0 x0 x0 (identity0 x0) (identity0 x0) = identity0 x0
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
proj1: object = object0
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 morphism = morphism0
proj2: transport
  (fun mor : object0 -> object0 -> Type =>
   forall s d d' : object0, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 morphism compose) =
compose0
x: object0
forall (s d : object0) (m : morphism0 s d),
compose0 s s d m
  (transport
     (fun mor : object0 -> object0 -> Type => forall x0 : object0, mor x0 x0)
     proj0
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x0 : obj, mor x0 x0)
        proj1 morphism identity)
     s) =
m
    path_induction; cbn in *.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x0 : object, morphism x0 x0
compose: forall s0 d0 d' : object, morphism d0 d' -> morphism s0 d0 -> morphism s0 d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x0 : object,
compose x0 x0 x0 (identity x0) (identity x0) = identity x0
trunc_morphism: forall s0 d0 : object, IsHSet (morphism s0 d0)
identity0: forall x0 : object, morphism x0 x0
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity0 b) f = f
right_identity0: forall (a b : object) (f : morphism a b), compose a a b f (identity0 a) = f
identity_identity0: forall x0 : object,
compose x0 x0 x0 (identity0 x0) (identity0 x0) = identity0 x0
trunc_morphism0: forall s0 d0 : object, IsHSet (morphism s0 d0)
x, s, d: object
m: morphism s d
compose s s d m (identity s) = m
    auto.
  Qed.

  Definition path_precategory''_T__of__path_precategory'_T `{Funext} C D
  : path_precategory'_T C D -> path_precategory''_T C D
    := fun H => (H.1; (H.2.1; (H.2.2, path_precategory_uncurried__identity_helper C D H))).

  Lemma eta2_sigma_helper A B P Q `{forall a b, IsHProp (Q a b)}
        (x : { a : A & { b : B a & P a b /\ Q a b }})
        q'
  : (x.1; (x.2.1; (fst x.2.2, q'))) = x.A: Type
B: A -> Type
P, Q: forall x0 : A, B x0 -> 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
  Proof.A: Type
B: A -> Type
P, Q: forall x0 : A, B x0 -> 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
    destruct x as [? [? [? ?]]]; cbn in *.A: Type
B: A -> Type
P, Q: forall x : 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
(proj1; proj0; (fst, q')) = (proj1; proj0; (fst, snd))
    repeat f_ap; apply path_ishprop.
  Defined.

  #[export] Instance isequiv__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)
         (fun H => (H.1; (H.2.1; fst H.2.2)))
         (fun x => eta2_sigma_helper _ _ _ x _)
         eta2_sigma.

  Definition path_precategory_uncurried' `{fs : Funext} (C D : PreCategory)
  : path_precategory''_T C D -> C = D.fs: Funext
C, D: PreCategory
path_precategory''_T C D -> C = D
  Proof.fs: Funext
C, D: PreCategory
path_precategory''_T C D -> C = D
    intros [? [? [? ?]]].fs: Funext
C, D: PreCategory
proj1: C = D
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 (morphism C) =
morphism D
fst: transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 (morphism C) (@compose C)) =
@compose D
snd: transport (fun mor : D -> D -> Type => forall x : D, mor x x) proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     proj1 (morphism C) identity) =
identity
C = D
    destruct C, D; cbn in *.fs: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x : object0, morphism0 x x
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x : object0, compose0 x x x (identity0 x) (identity0 x) = identity0 x
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
proj1: object = object0
proj0: transport (fun obj : Type => obj -> obj -> Type) proj1 morphism = morphism0
fst: transport
  (fun mor : object0 -> object0 -> Type =>
   forall s d d' : object0, mor d d' -> mor s d -> mor s d')
  proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     proj1 morphism compose) =
compose0
snd: transport
  (fun mor : object0 -> object0 -> Type => forall x : object0, mor x x) proj0
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     proj1 morphism identity) =
identity0
{|
  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
|}
    path_induction; cbn in *.fs: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
left_identity0: forall (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity0: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity0: forall x : object, compose x x x (identity x) (identity x) = identity x
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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
trunc_morphism0: forall s d : object, IsHSet (morphism s d)
{|
  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 := morphism;
  identity := identity;
  compose := compose;
  associativity := associativity0;
  associativity_sym := associativity_sym0;
  left_identity := left_identity0;
  right_identity := right_identity0;
  identity_identity := identity_identity0;
  trunc_morphism := trunc_morphism0
|}
    f_ap;
      eapply @center; abstract exact _.
  Defined.

  (** *** Said proof respects [object] *)
  Lemma path_precategory_uncurried'_fst `{Funext} C D HO HM HC HI
  : ap object (@path_precategory_uncurried' _ C D (HO; (HM; (HC, HI)))) = HO.H: Funext
C, D: PreCategory
HO: C = D
HM: transport (fun obj : Type => obj -> obj -> Type) HO (morphism C) = morphism D
HC: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     HO (morphism C) (@compose C)) =
@compose D
HI: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall x : D, mor x x)
  HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall x : obj, mor x x)
     HO (morphism C) identity) =
identity
ap object (path_precategory_uncurried' C D (HO; HM; (HC, HI))) = HO
  Proof.H: Funext
C, D: PreCategory
HO: C = D
HM: transport (fun obj : Type => obj -> obj -> Type) HO (morphism C) = morphism D
HC: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     HO (morphism C) (@compose C)) =
@compose D
HI: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall x : D, mor x x)
  HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall x : obj, mor x x)
     HO (morphism C) identity) =
identity
ap object (path_precategory_uncurried' C D (HO; HM; (HC, HI))) = HO
    destruct C, D; cbn in *.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x : object0, morphism0 x x
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x : object0, compose0 x x x (identity0 x) (identity0 x) = identity0 x
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
HO: object = object0
HM: transport (fun obj : Type => obj -> obj -> Type) HO morphism = morphism0
HC: transport
  (fun mor : object0 -> object0 -> Type =>
   forall s d d' : object0, mor d d' -> mor s d -> mor s d')
  HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     HO morphism compose) =
compose0
HI: transport
  (fun mor : object0 -> object0 -> Type => forall x : object0, mor x x) HM
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     HO morphism identity) =
identity0
ap Core.object
  (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
     |} (HO; HM; (HC, HI))) =
HO
    path_induction_hammer.
  Qed.

  (** *** Said proof respects [idpath] *)
  Lemma path_precategory_uncurried'_idpath `{Funext} C
  : @path_precategory_uncurried' _ C C (idpath; (idpath; (idpath, idpath))) = idpath.H: Funext
C: PreCategory
path_precategory_uncurried' C C (1; 1; (1, 1)) = 1
  Proof.H: Funext
C: PreCategory
path_precategory_uncurried' C C (1; 1; (1, 1)) = 1
    destruct C; cbn in *.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : 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 => 1
              end (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
    rewrite !(contr idpath).H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
ap11 (ap11 (ap11 (ap11 (ap11 1 1) 1) 1) 1) 1 = 1
    reflexivity.
  Qed.

  (** ** Equality of precategories gives rise to an inhabitant of the path-classifying-type *)
  Definition path_precategory_uncurried'_inv (C D : PreCategory)
  : C = D -> path_precategory''_T C D.C, D: PreCategory
C = D -> path_precategory''_T C D
  Proof.C, D: PreCategory
C = D -> path_precategory''_T C D
    intro H'.C, D: PreCategory
H': C = D
path_precategory''_T C D
    exists (ap object H').C, D: PreCategory
H': C = D
{Hmor
: transport (fun obj : Type => obj -> obj -> Type) 
    (ap object H') (morphism C) =
  morphism D
&
(transport
   (fun mor : D -> D -> Type =>
    forall s d d' : D, mor d d' -> mor s d -> mor s d')
   Hmor
   (transportD (fun obj : Type => obj -> obj -> Type)
      (fun (obj : Type) (mor : obj -> obj -> Type) =>
       forall s d d' : obj, mor d d' -> mor s d -> mor s d')
      (ap object H') (morphism C) (@compose C)) =
 @compose D) *
(transport (fun mor : D -> D -> Type => forall x : D, mor x x) Hmor
   (transportD (fun obj : Type => obj -> obj -> Type)
      (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
      (ap object H') (morphism C) identity) =
 identity)}
    exists ((transport_compose _ object _ _) ^ @ apD (@morphism) H').C, D: PreCategory
H': C = D
(transport
   (fun mor : D -> D -> Type =>
    forall s d d' : D, mor d d' -> mor s d -> mor s d')
   ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
       (morphism C))^ @
    apD morphism H')
   (transportD (fun obj : Type => obj -> obj -> Type)
      (fun (obj : Type) (mor : obj -> obj -> Type) =>
       forall s d d' : obj, mor d d' -> mor s d -> mor s d')
      (ap object H') (morphism C) (@compose C)) =
 @compose D) *
(transport (fun mor : D -> D -> Type => forall x : D, mor x x)
   ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
       (morphism C))^ @
    apD morphism H')
   (transportD (fun obj : Type => obj -> obj -> Type)
      (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
      (ap object H') (morphism C) identity) =
 identity)
    split.C, D: PreCategory
H': C = D
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : 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 (fun mor : D -> D -> Type => forall x : D, mor x x)
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     (ap object H') (morphism C) identity) =
identity
    -C, D: PreCategory
H': C = D
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     (ap object H') (morphism C) (@compose C)) =
@compose D refine (_ @ apD (@compose) H'); cbn.C, D: PreCategory
H': C = D
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     (ap object H') (morphism C) (@compose C)) =
transport
  (fun C0 : PreCategory =>
   forall s d d' : C0,
   morphism C0 d d' -> morphism C0 s d -> morphism C0 s d')
  H' (@compose C)
      refine (transport_pp _ _ _ _ @ _).C, D: PreCategory
H': C = D
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  (apD morphism H')
  (transport
     (fun mor : D -> D -> Type =>
      forall s d d' : D, mor d d' -> mor s d -> mor s d')
     (transport_compose (fun obj : Type => obj -> obj -> Type) object H'
        (morphism C))^
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        (ap object H') (morphism C) (@compose C))) =
transport
  (fun C0 : PreCategory =>
   forall s d d' : C0,
   morphism C0 d d' -> morphism C0 s d -> morphism C0 s d')
  H' (@compose C)
      exact ((ap _ (transportD_compose
                       (fun obj => obj -> obj -> Type)
                       (fun obj mor =>
                          forall s d d' : obj, mor d d' -> mor s d -> mor s d') object H'
                       (morphism C) (@compose C))^)
                @ (transport_apD_transportD
                     _
                     morphism
                     (fun x mor => forall s d d' : x, mor d d' -> mor s d -> mor s d') H'
                     (@compose C))).
    -C, D: PreCategory
H': C = D
transport (fun mor : D -> D -> Type => forall x : D, mor x x)
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     (ap object H') (morphism C) identity) =
identity refine (_ @ apD (@identity) H'); cbn.C, D: PreCategory
H': C = D
transport (fun mor : D -> D -> Type => forall x : D, mor x x)
  ((transport_compose (fun obj : Type => obj -> obj -> Type) object H'
      (morphism C))^ @
   apD morphism H')
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     (ap object H') (morphism C) identity) =
transport (fun C0 : PreCategory => forall x : C0, morphism C0 x x) H'
  identity
      refine (transport_pp _ _ _ _ @ _).C, D: PreCategory
H': C = D
transport (fun mor : D -> D -> Type => forall x : D, mor x x)
  (apD morphism H')
  (transport (fun mor : D -> D -> Type => forall x : D, mor x x)
     (transport_compose (fun obj : Type => obj -> obj -> Type) object H'
        (morphism C))^
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x : obj, mor x x)
        (ap object H') (morphism C) identity)) =
transport (fun C0 : PreCategory => forall x : C0, morphism C0 x x) H'
  identity
      exact ((ap _ (transportD_compose
                       (fun obj => obj -> obj -> Type)
                       (fun obj mor =>
                          forall x : obj, mor x x) object H'
                       (morphism C) (@identity C))^)
                @ (transport_apD_transportD
                     _
                     morphism
                     (fun x mor => forall s : x, mor s s) H'
                     (@identity C))).
  Defined.

  (** ** Classify equality of precategories up to equivalence *)
  Lemma equiv_path_precategory_uncurried'__eissect `{Funext} (C D : PreCategory)
  : forall x : path_precategory''_T C D,
      path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x.H: Funext
C, D: PreCategory
forall x : path_precategory''_T C D,
path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x
  Proof.H: Funext
C, D: PreCategory
forall x : path_precategory''_T C D,
path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x
    destruct C, D; cbn in *.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x : object0, morphism0 x x
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x : object0, compose0 x x x (identity0 x) (identity0 x) = identity0 x
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
forall
x : {Hobj : object = object0 &
    {Hmor
    : transport (fun obj : Type => obj -> obj -> Type) Hobj morphism =
      morphism0
    &
    (transport
       (fun mor : object0 -> object0 -> Type =>
        forall s d d' : object0, mor d d' -> mor s d -> mor s d')
       Hmor
       (transportD (fun obj : Type => obj -> obj -> Type)
          (fun (obj : Type) (mor : obj -> obj -> Type) =>
           forall s d d' : obj, mor d d' -> mor s d -> mor s d')
          Hobj morphism compose) =
     compose0) *
    (transport
       (fun mor : object0 -> object0 -> Type => forall x : object0, mor x x)
       Hmor
       (transportD (fun obj : Type => obj -> obj -> Type)
          (fun (obj : Type) (mor : obj -> obj -> Type) =>
           forall x : 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
    intros [H0' [H1' [H2' H3']]].H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
object0: Type
morphism0: object0 -> object0 -> Type
identity0: forall x : object0, morphism0 x x
compose0: forall s d d' : object0, morphism0 d d' -> morphism0 s d -> morphism0 s d'
associativity0: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object0) (f : morphism0 a b),
compose0 a b b (identity0 b) f = f
right_identity0: forall (a b : object0) (f : morphism0 a b),
compose0 a a b f (identity0 a) = f
identity_identity0: forall x : object0, compose0 x x x (identity0 x) (identity0 x) = identity0 x
trunc_morphism0: forall s d : object0, IsHSet (morphism0 s d)
H0': object = object0
H1': transport (fun obj : Type => obj -> obj -> Type) H0' morphism = morphism0
H2': transport
  (fun mor : object0 -> object0 -> Type =>
   forall s d d' : object0, mor d d' -> mor s d -> mor s d')
  H1'
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     H0' morphism compose) =
compose0
H3': transport
  (fun mor : object0 -> object0 -> Type => forall x : object0, mor x x) H1'
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) => forall x : obj, mor x x)
     H0' 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
     |} (H0'; H1'; (H2', H3'))) =
(H0'; H1'; (H2', H3'))
    path_induction.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
left_identity0: forall (a b : object)
(f : transport (fun obj : Type => obj -> obj -> Type) 1 morphism a b),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  a b b
  (transport
     (fun mor : object -> object -> Type => forall x : object, mor x x) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x : obj, mor x x)
        1 morphism identity)
     b)
  f =
f
right_identity0: forall (a b : object)
(f : transport (fun obj : Type => obj -> obj -> Type) 1 morphism a b),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  a a b f
  (transport
     (fun mor : object -> object -> Type => forall x : object, mor x x) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x : obj, mor x x)
        1 morphism identity)
     a) =
f
identity_identity0: forall x : object,
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x x x
  (transport
     (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x0 : obj, mor x0 x0)
        1 morphism identity)
     x)
  (transport
     (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x0 : obj, mor x0 x0)
        1 morphism identity)
     x) =
transport
  (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall x0 : obj, mor x0 x0)
     1 morphism identity)
  x
associativity0: forall (x1 x2 x3 x4 : object)
(m1 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x1 x2)
(m2 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x2 x3)
(m3 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x3 x4),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x2 x4
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x2 x3 x4 m3 m2)
  m1 =
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x3 x4 m3
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x1 x2 x3 m2 m1)
associativity_sym0: forall (x1 x2 x3 x4 : object)
(m1 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x1 x2)
(m2 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x2 x3)
(m3 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x3 x4),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x3 x4 m3
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x1 x2 x3 m2 m1) =
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x2 x4
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x2 x3 x4 m3 m2)
  m1
trunc_morphism0: forall s d : object,
IsHSet (transport (fun obj : 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 (fun obj : Type => obj -> obj -> Type) 1 morphism;
       identity :=
         transport
           (fun mor : object -> object -> Type => forall x : object, mor x x)
           1
           (transportD (fun obj : Type => obj -> obj -> Type)
              (fun (obj : Type) (mor : obj -> obj -> Type) =>
               forall x : obj, mor x x)
              1 morphism identity);
       compose :=
         transport
           (fun mor : object -> object -> Type =>
            forall s d d' : object, mor d d' -> mor s d -> mor s d')
           1
           (transportD (fun obj : Type => obj -> obj -> Type)
              (fun (obj : Type) (mor : obj -> obj -> Type) =>
               forall s d d' : 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))
    cbn.H: Funext
object: Type
morphism: object -> object -> Type
identity: forall x : object, morphism x x
compose: forall s d d' : object, morphism d d' -> morphism s d -> morphism s d'
associativity: forall (x1 x2 x3 x4 : 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 (x1 x2 x3 x4 : 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 (a b : object) (f : morphism a b), compose a b b (identity b) f = f
right_identity: forall (a b : object) (f : morphism a b), compose a a b f (identity a) = f
identity_identity: forall x : object, compose x x x (identity x) (identity x) = identity x
trunc_morphism: forall s d : object, IsHSet (morphism s d)
left_identity0: forall (a b : object)
(f : transport (fun obj : Type => obj -> obj -> Type) 1 morphism a b),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  a b b
  (transport
     (fun mor : object -> object -> Type => forall x : object, mor x x) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x : obj, mor x x)
        1 morphism identity)
     b)
  f =
f
right_identity0: forall (a b : object)
(f : transport (fun obj : Type => obj -> obj -> Type) 1 morphism a b),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  a a b f
  (transport
     (fun mor : object -> object -> Type => forall x : object, mor x x) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x : obj, mor x x)
        1 morphism identity)
     a) =
f
identity_identity0: forall x : object,
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x x x
  (transport
     (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x0 : obj, mor x0 x0)
        1 morphism identity)
     x)
  (transport
     (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall x0 : obj, mor x0 x0)
        1 morphism identity)
     x) =
transport
  (fun mor : object -> object -> Type => forall x0 : object, mor x0 x0) 1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall x0 : obj, mor x0 x0)
     1 morphism identity)
  x
associativity0: forall (x1 x2 x3 x4 : object)
(m1 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x1 x2)
(m2 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x2 x3)
(m3 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x3 x4),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x2 x4
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x2 x3 x4 m3 m2)
  m1 =
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x3 x4 m3
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x1 x2 x3 m2 m1)
associativity_sym0: forall (x1 x2 x3 x4 : object)
(m1 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x1 x2)
(m2 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x2 x3)
(m3 : transport (fun obj : Type => obj -> obj -> Type) 1 morphism x3 x4),
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x3 x4 m3
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x1 x2 x3 m2 m1) =
transport
  (fun mor : object -> object -> Type =>
   forall s d d' : object, mor d d' -> mor s d -> mor s d')
  1
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     1 morphism compose)
  x1 x2 x4
  (transport
     (fun mor : object -> object -> Type =>
      forall s d d' : object, mor d d' -> mor s d -> mor s d')
     1
     (transportD (fun obj : Type => obj -> obj -> Type)
        (fun (obj : Type) (mor : obj -> obj -> Type) =>
         forall s d d' : obj, mor d d' -> mor s d -> mor s d')
        1 morphism compose)
     x2 x3 x4 m3 m2)
  m1
trunc_morphism0: forall s d : object,
IsHSet (transport (fun obj : 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 => 1
                 end (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))
    repeat (edestruct (center (_ = _)); try reflexivity).
  Qed.

  Lemma equiv_path_precategory_uncurried' `{Funext} (C D : PreCategory)
  : path_precategory''_T C D <~> C = D.H: Funext
C, D: PreCategory
path_precategory''_T C D <~> C = D
  Proof.H: Funext
C, D: PreCategory
path_precategory''_T C D <~> C = D
    apply (equiv_adjointify (@path_precategory_uncurried' _ C D)
                            (@path_precategory_uncurried'_inv C D)).H: Funext
C, D: PreCategory
(fun x : C = D =>
 path_precategory_uncurried' C D (path_precategory_uncurried'_inv x)) ==
idmap
H: Funext
C, D: PreCategory
(fun x : path_precategory''_T C D =>
 path_precategory_uncurried'_inv (path_precategory_uncurried' C D x)) ==
idmap
    -H: Funext
C, D: PreCategory
(fun x : C = D =>
 path_precategory_uncurried' C D (path_precategory_uncurried'_inv x)) ==
idmap hnf.H: Funext
C, D: PreCategory
forall x : C = D,
path_precategory_uncurried' C D (path_precategory_uncurried'_inv x) = x
      intros [].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
(fun x : path_precategory''_T C D =>
 path_precategory_uncurried'_inv (path_precategory_uncurried' C D x)) ==
idmap hnf.H: Funext
C, D: PreCategory
forall x : path_precategory''_T C D,
path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x
      apply equiv_path_precategory_uncurried'__eissect.
  Defined.

  Definition equiv_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))).

  Definition path_precategory_uncurried `{Funext} C D : _ -> _
    := equiv_path_precategory_uncurried C D.

  (** ** Curried version of path classifying lemma *)
  Lemma path_precategory' `{fs : Funext} (C D : PreCategory)
  : forall (Hobj : object C = object D)
           (Hmor : transport (fun obj => obj -> obj -> Type)
                             Hobj
                             (morphism C)
                   = morphism D),
      transport _
                Hmor
                (transportD (fun obj => obj -> obj -> Type)
                            (fun obj mor => forall s d d', 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 (fun obj : Type => obj -> obj -> Type) Hobj (morphism C) =
        morphism D),
transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C)) =
@compose D -> C = D
  Proof.fs: Funext
C, D: PreCategory
forall (Hobj : C = D)
(Hmor : transport (fun obj : Type => obj -> obj -> Type) Hobj (morphism C) =
        morphism D),
transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C)) =
@compose D -> C = D
    intros.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: transport (fun obj : Type => obj -> obj -> Type) Hobj (morphism C) =
morphism D
X: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C)) =
@compose D
C = D
    apply path_precategory_uncurried.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: transport (fun obj : Type => obj -> obj -> Type) Hobj (morphism C) =
morphism D
X: transport
  (fun mor : (fun obj : Type => obj -> obj -> Type) D =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : (fun obj0 : Type => obj0 -> obj0 -> Type) obj) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C)) =
@compose D
path_precategory'_T C D
    repeat esplit; eassumption.
  Defined.

  (** ** Curried version of path classifying lemma, using [forall] in place of equality of functions *)
  Lemma path_precategory `{fs : Funext} (C D : PreCategory)
  : forall (Hobj : object C = object D)
           (Hmor : forall s d,
                     morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d)
                     = morphism D s d),
      (forall s d d' m m',
         transport idmap (Hmor _ _)
                   (@compose C _ _ _
                             (transport idmap (Hmor _ _)^ m)
                             (transport idmap (Hmor _ _)^ m'))
         = @compose D s d d' m m')
      -> C = D.fs: Funext
C, D: PreCategory
forall (Hobj : C = D)
(Hmor : forall s d : D,
        morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
        morphism D s d),
(forall (s d d' : 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
  Proof.fs: Funext
C, D: PreCategory
forall (Hobj : C = D)
(Hmor : forall s d : D,
        morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
        morphism D s d),
(forall (s d d' : 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
    intros Hobj Hmor Hcomp.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : D,
morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
morphism D s d
Hcomp: forall (s d d' : 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
    pose (path_forall
            _ _
            (fun s =>
               path_forall
                 _ _
                 (fun d =>
                    (ap10 (@transport_arrow Type idmap (fun x => x -> Type) _ _ Hobj (@morphism C) _) _)
                      @ (@transport_arrow Type idmap _ _ _ Hobj (@morphism C _) _)
                      @ (transport_const _ _)
                      @ Hmor s d)))
      as Hmor'.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : D,
morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
morphism D s d
Hcomp: forall (s d d' : 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 (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x)
     Hobj (morphism C))
  (morphism D)
  (fun s : D =>
   path_forall
     (transport (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x)
        Hobj (morphism C) s)
     (morphism D s)
     (fun d : 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 (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x) Hobj
  (morphism C) =
morphism D
C = D
    eapply (path_precategory' C D Hobj Hmor').fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : D,
morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
morphism D s d
Hcomp: forall (s d d' : 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 (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x)
     Hobj (morphism C))
  (morphism D)
  (fun s : D =>
   path_forall
     (transport (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x)
        Hobj (morphism C) s)
     (morphism D s)
     (fun d : 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 (fun x : Type => idmap x -> (fun x0 : Type => x0 -> Type) x) Hobj
  (morphism C) =
morphism D
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor'
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C)) =
@compose D
    repeat (apply path_forall; intro).fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : D,
morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
morphism D s d
Hcomp: forall (s d d' : 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 (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4)
     Hobj (morphism C))
  (morphism D)
  (fun s : D =>
   path_forall
     (transport
        (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4) Hobj
        (morphism C) s)
     (morphism D s)
     (fun d : 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 (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4)
  Hobj (morphism C) =
morphism D
x, x0, x1: D
x2: morphism D x0 x1
x3: morphism D x x0
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor'
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : obj, mor d d' -> mor s d -> mor s d')
     Hobj (morphism C) (@compose C))
  x x0 x1 x2 x3 =
x2 o x3
    refine (_ @ Hcomp _ _ _ _ _); clear Hcomp.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : D,
morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) =
morphism D s d
Hmor':= path_forall
  (transport (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4)
     Hobj (morphism C))
  (morphism D)
  (fun s : D =>
   path_forall
     (transport
        (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4) Hobj
        (morphism C) s)
     (morphism D s)
     (fun d : 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 (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4)
  Hobj (morphism C) =
morphism D
x, x0, x1: D
x2: morphism D x0 x1
x3: morphism D x x0
transport
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  Hmor'
  (transportD (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : 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)
    subst Hmor'.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : 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
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  (path_forall
     (transport
        (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4) Hobj
        (morphism C))
     (morphism D)
     (fun s : D =>
      path_forall
        (transport
           (fun x4 : Type => idmap x4 -> (fun x5 : Type => x5 -> Type) x4)
           Hobj (morphism C) s)
        (morphism D s)
        (fun d : 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 (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : 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)
    cbn.fs: Funext
C, D: PreCategory
Hobj: C = D
Hmor: forall s d : 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
  (fun mor : D -> D -> Type =>
   forall s d d' : D, mor d d' -> mor s d -> mor s d')
  (path_forall
     (transport (fun x4 : Type => x4 -> x4 -> Type) Hobj (morphism C))
     (morphism D)
     (fun s : D =>
      path_forall
        (transport (fun x4 : Type => x4 -> x4 -> Type) Hobj (morphism C) s)
        (morphism D s)
        (fun d : 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 (fun obj : Type => obj -> obj -> Type)
     (fun (obj : Type) (mor : obj -> obj -> Type) =>
      forall s d d' : 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;
        cbn in *;
          destruct Hobj;
        cbn in *;
          repeat match 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.
End path_category.

(** ** Tactic for proving equality of precategories *)
(** We move the funext inference outside the loop. *)
Ltac path_category :=
  idtac;
  let lem := constr:(@path_precategory _) in
  repeat match goal with
           | _ => intro
           | _ => reflexivity
           | _ => simple refine (lem _ _ _ _ _); cbn
         end.