Paths.v

(** * Classification of path spaces of precategories *)
Require Import Category.Core.[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.

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 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) 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 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) s = m
    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)
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 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) s) = m
    path_induction; 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)
identity0: forall x : object, morphism x 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
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 x : object,
compose x x x (identity0 x)
  (identity0 x) = identity0 x
trunc_morphism0: forall s d : object,
IsHSet (morphism s d)
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 x : 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
  Proof.A: Type
B: A -> Type
P, Q: forall x : 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
    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.

  Global 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 precategorys 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 C : PreCategory =>
   forall s d d' : C,
   morphism C d d' ->
   morphism C s d -> morphism C 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 C : PreCategory =>
   forall s d d' : C,
   morphism C d d' ->
   morphism C s d -> morphism C s d') H' (@compose C)
      refine ((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 C : PreCategory => forall x : C, morphism C 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 C : PreCategory => forall x : C, morphism C x x)
  H' identity
      refine ((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 precategorys 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 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
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 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
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 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)))
  (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 x : Type => x -> x -> Type) Hobj
        (morphism C)) (morphism D)
     (fun s : D =>
      path_forall
        (transport (fun x : Type => x -> x -> 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.