Require Import Category.Core Functor.Core NaturalTransformation.Core.Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import Functor.Composition.Core.
Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core.
Require Import Category.Morphisms FunctorCategory.Core.
Require Import Pseudofunctor.Core.
Require Import NaturalTransformation.Composition.Laws.
Require Import Trunc Types.Sigma.
Require Import Basics.Tactics.

Import Functor.Identity.FunctorIdentityNotations.

Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope morphism_scope.
Local Open Scope category_scope.
Local Open Scope type_scope.

(** Quoting David Spivak:

    David: ok
       so an object of [FC ⇓ D] is a pair [(X, G)], where [X] is a
       finite category (or a small category or whatever you wanted)
       and [G : X --> D] is a functor.
       a morphism in [FC ⇓ D] is a ``natural transformation diagram''
       (as opposed to a commutative diagram, in which the natural
       transformation would be ``identity'')
       so a map in [FC ⇓ D] from [(X, G)] to [(X', G')] is a pair
       [(F, α)] where [F : X --> X'] is a functor and
       [α : G --> G' ∘ F] is a natural transformation
       and the punchline is that there is a functor
       [colim : FC ⇓ D --> D]

     David: consider for yourself the case where [F : X --> X'] is
       identity ([X = X']) and (separately) the case where
       [α : G --> G ∘ F] is identity.
       the point is, you've already done the work to get this colim
       functor.
       because every map in [FC ⇓ D] can be written as a composition
       of two maps, one where the [F]-part is identity and one where
       the [α]-part is identity.
       and you've worked both of those cases out already.
       *)

Module Import LaxCommaCategoryParts.
  Section lax_comma_category_parts.
    Context `{Funext}.
    Variables A B : PreCategory.

    Variable S : Pseudofunctor A.
    Variable T : Pseudofunctor B.

    Context `{forall a b, IsHSet (Functor (S a) (T b))}.

    Record object :=
      {
        a : A;
        b : B;
        f : Functor (S a) (T b)
      }.

    Local Abbreviation object_sig_T :=
      ({ a : A
       | { b : B
         | Functor (S a) (T b) }}).

    Lemma issig_object
    : object_sig_T <~> object.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
{a0 : A & {b0 : B & Functor (S a0) (T b0)}} <~> object
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
{a0 : A & {b0 : B & Functor (S a0) (T b0)}} <~> object
      issig.
    Defined.

    #[export] Instance trunc_object `{IsTrunc n A, IsTrunc n B}
           `{forall s d, IsTrunc n (Functor (S s) (T d))}
    : IsTrunc n object.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
n: trunc_index
IsTrunc0: IsTrunc n A
IsTrunc1: IsTrunc n B
H1: forall (s : A) (d : B), IsTrunc n (Functor (S s) (T d))
IsTrunc n object
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
n: trunc_index
IsTrunc0: IsTrunc n A
IsTrunc1: IsTrunc n B
H1: forall (s : A) (d : B), IsTrunc n (Functor (S s) (T d))
IsTrunc n object
      eapply istrunc_equiv_istrunc;
      [ exact issig_object | ].
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
n: trunc_index
IsTrunc0: IsTrunc n A
IsTrunc1: IsTrunc n B
H1: forall (s : A) (d : B), IsTrunc n (Functor (S s) (T d))
IsTrunc n {a0 : A & {b0 : B & Functor (S a0) (T b0)}}
      typeclasses eauto.
    Qed.

    Lemma path_object (x y : object)
    : forall (Ha : x.(a) = y.(a))
             (Hb : x.(b) = y.(b)),
        match Ha in _ = X, Hb in _ = Y return Functor (S X) (T Y) with
          | idpath, idpath => x.(f)
        end = y.(f)
        -> x = y.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
forall (Ha : a x = a y) (Hb : b x = b y),
match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y -> x = y
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
forall (Ha : a x = a y) (Hb : b x = b y),
match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y -> x = y
      destruct x, y; simpl.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a2 : A) (b2 : B), IsHSet (Functor (S a2) (T b2))
a0: A
b0: B
f0: Functor (S a0) (T b0)
a1: A
b1: B
f1: Functor (S a1) (T b1)
forall (Ha : a0 = a1) (Hb : b0 = b1),
match Ha in _ = X return Functor (S X) (T b1) with
| 1%path =>
    match Hb in _ = Y return Functor (S a0) (T Y) with
    | 1%path => f0
    end
end = f1 -> {| a := a0; b := b0; f := f0 |} = {| a := a1; b := b1; f := f1 |}
      intros; path_induction; reflexivity.
    Defined.

    Definition path_object_uncurried x y
               (H : { HaHb : (x.(a) = y.(a)) * (x.(b) = y.(b))
                    | match fst HaHb in _ = X, snd HaHb in _ = Y return Functor (S X) (T Y) with
                        | idpath, idpath => x.(f)
                      end = y.(f) })
    : x = y
      := @path_object x y (fst H.1) (snd H.1) H.2.

    Lemma ap_a_path_object x y Ha Hb Hf
    : ap (@a) (@path_object x y Ha Hb Hf) = Ha.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
Ha: a x = a y
Hb: b x = b y
Hf: match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y
ap a (path_object x y Ha Hb Hf) = Ha
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
Ha: a x = a y
Hb: b x = b y
Hf: match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y
ap a (path_object x y Ha Hb Hf) = Ha
      destruct x, y; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a2 : A) (b2 : B), IsHSet (Functor (S a2) (T b2))
a0: A
b0: B
f0: Functor (S a0) (T b0)
a1: A
b1: B
f1: Functor (S a1) (T b1)
Ha: a0 = a1
Hb: b0 = b1
Hf: match Ha in _ = X return Functor (S X) (T b1) with
| 1%path =>
    match Hb in _ = Y return Functor (S a0) (T Y) with
    | 1%path => f0
    end
end = f1
ap a
  (path_object {| a := a0; b := b0; f := f0 |}
     {| a := a1; b := b1; f := f1 |} Ha Hb Hf) =
Ha
      destruct Ha, Hb, Hf; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a1 : A) (b1 : B), IsHSet (Functor (S a1) (T b1))
a0: A
b0: B
f0: Functor (S a0) (T b0)
1%path = 1%path
      reflexivity.
    Qed.

    Lemma ap_b_path_object x y Ha Hb Hf
    : ap (@b) (@path_object x y Ha Hb Hf) = Hb.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
Ha: a x = a y
Hb: b x = b y
Hf: match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y
ap b (path_object x y Ha Hb Hf) = Hb
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x, y: object
Ha: a x = a y
Hb: b x = b y
Hf: match Ha in _ = X return Functor (S X) (T (b y)) with
| 1%path =>
    match Hb in _ = Y return Functor (S (a x)) (T Y) with
    | 1%path => f x
    end
end = f y
ap b (path_object x y Ha Hb Hf) = Hb
      destruct x, y; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a2 : A) (b2 : B), IsHSet (Functor (S a2) (T b2))
a0: A
b0: B
f0: Functor (S a0) (T b0)
a1: A
b1: B
f1: Functor (S a1) (T b1)
Ha: a0 = a1
Hb: b0 = b1
Hf: match Ha in _ = X return Functor (S X) (T b1) with
| 1%path =>
    match Hb in _ = Y return Functor (S a0) (T Y) with
    | 1%path => f0
    end
end = f1
ap b
  (path_object {| a := a0; b := b0; f := f0 |}
     {| a := a1; b := b1; f := f1 |} Ha Hb Hf) =
Hb
      destruct Ha, Hb, Hf; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a1 : A) (b1 : B), IsHSet (Functor (S a1) (T b1))
a0: A
b0: B
f0: Functor (S a0) (T b0)
1%path = 1%path
      reflexivity.
    Qed.

    Global Opaque path_object.

    Record morphism (abf a'b'f' : object) :=
      {
        g : Category.Core.morphism A (abf.(a)) (a'b'f'.(a));
        h : Category.Core.morphism B (abf.(b)) (a'b'f'.(b));
        p : NaturalTransformation (p_morphism_of T h o abf.(f))
                                  (a'b'f'.(f) o p_morphism_of S g)
      }.

    Local Abbreviation morphism_sig_T abf a'b'f' :=
      ({ g : Category.Core.morphism A (abf.(a)) (a'b'f'.(a))
       | { h : Category.Core.morphism B (abf.(b)) (a'b'f'.(b))
         | NaturalTransformation (p_morphism_of T h o abf.(f))
                                 (a'b'f'.(f) o p_morphism_of S g) }}).

    Lemma issig_morphism abf a'b'f'
    : (morphism_sig_T abf a'b'f')
        <~> morphism abf a'b'f'.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
morphism_sig_T abf a'b'f' <~> morphism abf a'b'f'
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
morphism_sig_T abf a'b'f' <~> morphism abf a'b'f'
      issig.
    Defined.

    #[export] Instance trunc_morphism abf a'b'f'
           `{IsTrunc n (Category.Core.morphism A (abf.(a)) (a'b'f'.(a)))}
           `{IsTrunc n (Category.Core.morphism B (abf.(b)) (a'b'f'.(b)))}
           `{forall m1 m2,
               IsTrunc n (NaturalTransformation
                            (p_morphism_of T m2 o abf.(f))
                            (a'b'f'.(f) o p_morphism_of S m1))}
    : IsTrunc n (morphism abf a'b'f').
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
n: trunc_index
IsTrunc0: IsTrunc n (Core.morphism A (a abf) (a a'b'f'))
IsTrunc1: IsTrunc n (Core.morphism B (b abf) (b a'b'f'))
H1: forall (m1 : Core.morphism A (a abf) (a a'b'f'))
(m2 : Core.morphism B (b abf) (b a'b'f')),
IsTrunc n
  (NaturalTransformation (p_morphism_of T m2 o f abf)
     (f a'b'f' o p_morphism_of S m1))
IsTrunc n (morphism abf a'b'f')
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
n: trunc_index
IsTrunc0: IsTrunc n (Core.morphism A (a abf) (a a'b'f'))
IsTrunc1: IsTrunc n (Core.morphism B (b abf) (b a'b'f'))
H1: forall (m1 : Core.morphism A (a abf) (a a'b'f'))
(m2 : Core.morphism B (b abf) (b a'b'f')),
IsTrunc n
  (NaturalTransformation (p_morphism_of T m2 o f abf)
     (f a'b'f' o p_morphism_of S m1))
IsTrunc n (morphism abf a'b'f')
      eapply istrunc_equiv_istrunc;
      [ exact (issig_morphism _ _) | ].
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
n: trunc_index
IsTrunc0: IsTrunc n (Core.morphism A (a abf) (a a'b'f'))
IsTrunc1: IsTrunc n (Core.morphism B (b abf) (b a'b'f'))
H1: forall (m1 : Core.morphism A (a abf) (a a'b'f'))
(m2 : Core.morphism B (b abf) (b a'b'f')),
IsTrunc n
  (NaturalTransformation (p_morphism_of T m2 o f abf)
     (f a'b'f' o p_morphism_of S m1))
IsTrunc n (morphism_sig_T abf a'b'f')
      typeclasses eauto.
    Qed.

    Lemma path_morphism abf a'b'f'
          (gh g'h' : morphism abf a'b'f')
    : forall
        (Hg : gh.(g) = g'h'.(g))
        (Hh : gh.(h) = g'h'.(h)),
        match Hg in _ = g, Hh in _ = h
              return NaturalTransformation
                       (p_morphism_of T h o abf.(f))
                       (a'b'f'.(f) o p_morphism_of S g)
        with
          | idpath, idpath => gh.(p)
        end = g'h'.(p)
         -> gh = g'h'.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
forall (Hg : g gh = g g'h') (Hh : h gh = h g'h'),
match
  Hg in _ = g
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g)
with
| 1%path =>
    match
      Hh in _ = h
      return
        NaturalTransformation (p_morphism_of T h o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h' -> gh = g'h'
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
forall (Hg : g gh = g g'h') (Hh : h gh = h g'h'),
match
  Hg in _ = g
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g)
with
| 1%path =>
    match
      Hh in _ = h
      return
        NaturalTransformation (p_morphism_of T h o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h' -> gh = g'h'
      intros Hg Hh Hp.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
Hg: g gh = g g'h'
Hh: h gh = h g'h'
Hp: match
  Hg in _ = g0
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g0)
with
| 1%path =>
    match
      Hh in _ = h0
      return
        NaturalTransformation (p_morphism_of T h0 o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h'
gh = g'h'
      destruct gh, g'h'; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
g0: Core.morphism A (a abf) (a a'b'f')
h0: Core.morphism B (b abf) (b a'b'f')
p0: NaturalTransformation (p_morphism_of T h0 o f abf)
  (f a'b'f' o p_morphism_of S g0)
g1: Core.morphism A (a abf) (a a'b'f')
h1: Core.morphism B (b abf) (b a'b'f')
p1: NaturalTransformation (p_morphism_of T h1 o f abf)
  (f a'b'f' o p_morphism_of S g1)
Hg: g0 = g1
Hh: h0 = h1
Hp: match
  Hg in _ = g2
  return
    NaturalTransformation (p_morphism_of T h1 o f abf)
      (f a'b'f' o p_morphism_of S g2)
with
| 1%path =>
    match
      Hh in _ = h2
      return
        NaturalTransformation (p_morphism_of T h2 o f abf)
          (f a'b'f' o p_morphism_of S g0)
    with
    | 1%path => p0
    end
end = p1
{| g := g0; h := h0; p := p0 |} = {| g := g1; h := h1; p := p1 |}
      destruct Hg, Hh, Hp.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
g0: Core.morphism A (a abf) (a a'b'f')
h0: Core.morphism B (b abf) (b a'b'f')
p0: NaturalTransformation (p_morphism_of T h0 o f abf)
  (f a'b'f' o p_morphism_of S g0)
{| g := g0; h := h0; p := p0 |} = {| g := g0; h := h0; p := p0 |}
      reflexivity.
    Qed.

    Definition path_morphism_uncurried abf a'b'f' gh g'h'
               (H : { HgHh : (gh.(g) = g'h'.(g)) * (gh.(h) = g'h'.(h))
                    | match fst HgHh in _ = g, snd HgHh in _ = h
                            return NaturalTransformation
                                     (p_morphism_of T h o abf.(f))
                                     (a'b'f'.(f) o p_morphism_of S g)
                      with
                        | idpath, idpath => gh.(p)
                      end = g'h'.(p) })
    : gh = g'h'
      := @path_morphism abf a'b'f' gh g'h' (fst H.1) (snd H.1) H.2.

    Lemma path_morphism'_helper abf a'b'f'
          (gh g'h' : morphism abf a'b'f')
    : forall
        (Hg : gh.(g) = g'h'.(g))
        (Hh : gh.(h) = g'h'.(h)),
        ((_ oL (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ S _ _) Hg) : Category.Core.morphism _ _ _))
           o (gh.(p))
           o ((Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ T _ _) Hh) : Category.Core.morphism _ _ _)^-1 oR _)
         = g'h'.(p))%natural_transformation
        -> match Hg in _ = g, Hh in _ = h
                 return NaturalTransformation
                          (p_morphism_of T h o abf.(f))
                          (a'b'f'.(f) o p_morphism_of S g)
           with
             | idpath, idpath => gh.(p)
           end = g'h'.(p).
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
forall (Hg : g gh = g g'h') (Hh : h gh = h g'h'),
(f a'b'f'
 oL (idtoiso (S (a abf) -> S (a a'b'f')) (ap (p_morphism_of S) Hg)
     :
     Core.morphism (S (a abf) -> S (a a'b'f')) (p_morphism_of S (g gh))
       (p_morphism_of S (g g'h')))
 o p gh
 o ((idtoiso (T (b abf) -> T (b a'b'f')) (ap (p_morphism_of T) Hh))^-1
    oR f abf))%natural_transformation =
p g'h' ->
match
  Hg in _ = g0
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g0)
with
| 1%path =>
    match
      Hh in _ = h0
      return
        NaturalTransformation (p_morphism_of T h0 o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h'
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
forall (Hg : g gh = g g'h') (Hh : h gh = h g'h'),
(f a'b'f'
 oL (idtoiso (S (a abf) -> S (a a'b'f')) (ap (p_morphism_of S) Hg)
     :
     Core.morphism (S (a abf) -> S (a a'b'f')) (p_morphism_of S (g gh))
       (p_morphism_of S (g g'h')))
 o p gh
 o ((idtoiso (T (b abf) -> T (b a'b'f')) (ap (p_morphism_of T) Hh))^-1
    oR f abf))%natural_transformation =
p g'h' ->
match
  Hg in _ = g0
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g0)
with
| 1%path =>
    match
      Hh in _ = h0
      return
        NaturalTransformation (p_morphism_of T h0 o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h'
      simpl; intros Hg Hh Hp.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh, g'h': morphism abf a'b'f'
Hg: g gh = g g'h'
Hh: h gh = h g'h'
Hp: (f a'b'f' oL idtoiso (S (a abf) -> S (a a'b'f')) (ap (p_morphism_of S) Hg)
 o p gh
 o ((idtoiso (T (b abf) -> T (b a'b'f')) (ap (p_morphism_of T) Hh))^-1
    oR f abf))%natural_transformation =
p g'h'
match
  Hg in _ = g0
  return
    NaturalTransformation (p_morphism_of T (h g'h') o f abf)
      (f a'b'f' o p_morphism_of S g0)
with
| 1%path =>
    match
      Hh in _ = h0
      return
        NaturalTransformation (p_morphism_of T h0 o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p g'h'
      destruct g'h'; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh: morphism abf a'b'f'
g0: Core.morphism A (a abf) (a a'b'f')
h0: Core.morphism B (b abf) (b a'b'f')
p0: NaturalTransformation (p_morphism_of T h0 o f abf)
  (f a'b'f' o p_morphism_of S g0)
Hg: g gh = g0
Hh: h gh = h0
Hp: (f a'b'f' oL idtoiso (S (a abf) -> S (a a'b'f')) (ap (p_morphism_of S) Hg)
 o p gh
 o ((idtoiso (T (b abf) -> T (b a'b'f')) (ap (p_morphism_of T) Hh))^-1
    oR f abf))%natural_transformation =
p0
match
  Hg in _ = g1
  return
    NaturalTransformation (p_morphism_of T h0 o f abf)
      (f a'b'f' o p_morphism_of S g1)
with
| 1%path =>
    match
      Hh in _ = h1
      return
        NaturalTransformation (p_morphism_of T h1 o f abf)
          (f a'b'f' o p_morphism_of S (g gh))
    with
    | 1%path => p gh
    end
end = p0
      destruct Hg, Hh, Hp; simpl in *.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh: morphism abf a'b'f'
p gh =
(f a'b'f' oL NaturalTransformation.Identity.identity (p_morphism_of S (g gh))
 o p gh
 o (NaturalTransformation.Identity.identity (p_morphism_of T (h gh)) oR f abf))%natural_transformation
      path_natural_transformation.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh: morphism abf a'b'f'
x: S (a abf)
p gh x = (f a'b'f') _1 1 o p gh x o 1
      autorewrite with functor morphism.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
abf, a'b'f': object
gh: morphism abf a'b'f'
x: S (a abf)
p gh x = p gh x
      reflexivity.
    Qed.

    Definition path_morphism' abf a'b'f'
               (gh g'h' : morphism abf a'b'f')
               (Hg : gh.(g) = g'h'.(g))
               (Hh : gh.(h) = g'h'.(h))
               (Hp : ((_ oL (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ S _ _) Hg) : Category.Core.morphism _ _ _))
                        o (gh.(p))
                        o ((Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ T _ _) Hh) : Category.Core.morphism _ _ _)^-1 oR _)
                      = g'h'.(p))%natural_transformation)
    : gh = g'h'
      := @path_morphism abf a'b'f' gh g'h' Hg Hh
                        (@path_morphism'_helper abf a'b'f' gh g'h' Hg Hh Hp).

    Definition path_morphism'_uncurried abf a'b'f' gh g'h'
               (H : { HgHh : (gh.(g) = g'h'.(g)) * (gh.(h) = g'h'.(h))
                    | ((_ oL (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ S _ _) (fst HgHh)) : Category.Core.morphism _ _ _))
                         o (gh.(p))
                         o ((Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ T _ _) (snd HgHh)) : Category.Core.morphism _ _ _)^-1 oR _)
                       = g'h'.(p))%natural_transformation })
    : gh = g'h'
      := @path_morphism' abf a'b'f' gh g'h' (fst H.1) (snd H.1) H.2.

    Definition compose s d d'
               (gh : morphism d d') (g'h' : morphism s d)
    : morphism s d'.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
s, d, d': object
gh: morphism d d'
g'h': morphism s d
morphism s d'
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
s, d, d': object
gh: morphism d d'
g'h': morphism s d
morphism s d'
      exists (gh.(g) o g'h'.(g)) (gh.(h) o g'h'.(h)).
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
s, d, d': object
gh: morphism d d'
g'h': morphism s d
NaturalTransformation (p_morphism_of T (h gh o h g'h') o f s)
  (f d' o p_morphism_of S (g gh o g g'h'))
      exact ((_ oL (p_composition_of S _ _ _ _ _)^-1)
               o (associator_1 _ _ _)
               o (gh.(p) oR _)
               o (associator_2 _ _ _)
               o (_ oL g'h'.(p))
               o (associator_1 _ _ _)
               o ((p_composition_of T _ _ _ _ _ : Category.Core.morphism _ _ _)
                    oR _))%natural_transformation.
    Defined.

    Global Arguments compose _ _ _ _ _ / .

    Definition identity x : morphism x x.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x: object
morphism x x
    Proof.
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x: object
morphism x x
      exists (identity (x.(a))) (identity (x.(b))).
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a0 : A) (b0 : B), IsHSet (Functor (S a0) (T b0))
x: object
NaturalTransformation (p_morphism_of T 1 o f x) (f x o p_morphism_of S 1)
      exact ((_ oL (p_identity_of S _ : Category.Core.morphism _ _ _)^-1)
               o (right_identity_natural_transformation_2 _)
               o (left_identity_natural_transformation_1 _)
               o ((p_identity_of T _ : Category.Core.morphism _ _ _)
                    oR _))%natural_transformation.
    Defined.

    Global Arguments identity _ / .
  End lax_comma_category_parts.
End LaxCommaCategoryParts.