(** * Functoriality of the comma category construction with projection functors *)
Require Import Category.Core Functor.Core.
Require Import Category.Prod Functor.Prod.Core.
Require Import Category.Dual Functor.Dual.
Require Import Functor.Composition.Core.
Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors NatCategory.
Require Import FunctorCategory.Core.
Require Import Cat.Core.
Require Import Functor.Paths.
Require Comma.Core.
Import Comma.Core.
Require Import Comma.InducedFunctors Comma.Projection.
Require ProductLaws ExponentialLaws.Law1.Functors ExponentialLaws.Law4.Functors.
Require Import Types.Forall PathGroupoids HoTT.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.

(** ** Functor from [(A → C)ᵒᵖ × (B → C)] to [cat / (A × B)] *)
(** It sends [S : A → C ← B : T] to the category [(S / T)] and its projection functor to [A × B]. *)
Section comma.
  Local Open Scope type_scope.
  Context `{Funext}.

  Variable P : PreCategory -> Type.
  Context `{HF : forall C D, P C -> P D -> IsHSet (Functor C D)}.

  Local Abbreviation Cat := (@sub_pre_cat _ P HF).

  Variables A B C : PreCategory.

  Hypothesis PAB : P (A * B).
  Hypothesis P_comma : forall (S : Functor A C) (T : Functor B C),
                         P (S / T).

  Local Open Scope category_scope.
  Local Open Scope morphism_scope.

  Definition comma_category_projection_functor_object_of
             (ST : object ((A -> C)^op * (B -> C)))
  : Cat / !((A * B; PAB) : Cat).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
ST: ((A -> C)^op * (B -> C))%category
Cat / !((A * B; PAB) : Cat)
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
ST: ((A -> C)^op * (B -> C))%category
Cat / !((A * B; PAB) : Cat)
    exists (Basics.Overture.fst ST / Basics.Overture.snd ST; P_comma _ _) (center _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
ST: ((A -> C)^op * (B -> C))%category
morphism Cat
  (Cat
   _0 (Overture.fst ST / Overture.snd ST;
      P_comma (Overture.fst ST) (Overture.snd ST)))%object
  (!(A * B; PAB) _0 (center 1%category))%object
    exact (comma_category_projection (Basics.Overture.fst ST) (Basics.Overture.snd ST)).
  Defined.

  Definition comma_category_projection_functor_morphism_of
             s d (m : morphism ((A -> C)^op * (B -> C)) s d)
  : morphism (Cat / !((A * B; PAB) : Cat))
             (comma_category_projection_functor_object_of s)
             (comma_category_projection_functor_object_of d).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d: ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
morphism (Cat / !((A * B; PAB) : Cat))
  (comma_category_projection_functor_object_of s)
  (comma_category_projection_functor_object_of d)
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d: ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
morphism (Cat / !((A * B; PAB) : Cat))
  (comma_category_projection_functor_object_of s)
  (comma_category_projection_functor_object_of d)
    hnf.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d: ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
CommaCategory.morphism (comma_category_projection_functor_object_of s)
  (comma_category_projection_functor_object_of d)
    refine (CommaCategory.Build_morphism
              (comma_category_projection_functor_object_of s)
              (comma_category_projection_functor_object_of d)
              (comma_category_induced_functor m)
              (center _)
              _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d: ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
!(A * B; PAB)
_1 (center
      (morphism 1
         (CommaCategory.b (comma_category_projection_functor_object_of s))
         (CommaCategory.b (comma_category_projection_functor_object_of d))))
o CommaCategory.f (comma_category_projection_functor_object_of s) =
CommaCategory.f (comma_category_projection_functor_object_of d)
o Cat _1 (comma_category_induced_functor m)
    simpl.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d: ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
(Identity.identity (A * B)
 o comma_category_projection (Overture.fst s) (Overture.snd s))%functor =
(comma_category_projection (Overture.fst d) (Overture.snd d)
 o comma_category_induced_functor m)%functor
    destruct_head_hnf Basics.Overture.prod.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
fst1: Functor A C
snd1: Functor B C
fst0: Functor A C
snd0: Functor B C
fst: Core.NaturalTransformation fst0 fst1
snd: Core.NaturalTransformation snd1 snd0
(Identity.identity (A * B) o comma_category_projection fst1 snd1)%functor =
(comma_category_projection fst0 snd0
 o comma_category_induced_functor (fst, snd)%core)%functor
    path_functor.
  Defined.

  Local Ltac comma_laws_t :=
    repeat (apply path_forall || intro);
    simpl;
    rewrite !transport_forall_constant;
    transport_path_forall_hammer;
    simpl;
    destruct_head Basics.Overture.prod;
    simpl in *;
    apply CommaCategory.path_morphism;
    simpl;
    repeat match goal with
             | [ |- context[?f _ _ _ _ _ _ _ (transport ?P ?p ?z)] ]
               => simpl rewrite (@ap_transport
                                   _ P _ _ _ p
                                   (fun _ => f _ _ _ _ _ _ _)
                                   z)
             | [ |- context[transport (fun y => ?f (?fa _ _ _ _ _ y) ?x)] ]
               => rewrite (fun a b => @transport_compose _ _ a b (fun y => f y x) (fa _ _ _ _ _))
             | [ |- context[transport (fun y => ?f ?x (?fa _ _ _ _ _ y))] ]
               => rewrite (fun a b => @transport_compose _ _ a b (fun y => f x y) (fa _ _ _ _ _))
           end;
    unfold comma_category_induced_functor_object_of_identity;
    unfold comma_category_induced_functor_object_of_compose;
    simpl;
    rewrite ?CommaCategory.ap_a_path_object', ?CommaCategory.ap_b_path_object';
    try reflexivity.

  Lemma comma_category_projection_functor_identity_of x
  : comma_category_projection_functor_morphism_of (Category.Core.identity x)
    = 1.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
x: ((A -> C)^op * (B -> C))%category
comma_category_projection_functor_morphism_of 1 = 1
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
x: ((A -> C)^op * (B -> C))%category
comma_category_projection_functor_morphism_of 1 = 1
    apply CommaCategory.path_morphism; simpl; [ | reflexivity ].
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
x: ((A -> C)^op * (B -> C))%category
comma_category_induced_functor
  (NaturalTransformation.Identity.identity (Overture.fst x),
  NaturalTransformation.Identity.identity (Overture.snd x)) =
Identity.identity (Overture.fst x / Overture.snd x)
    path_functor.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
x: ((A -> C)^op * (B -> C))%category
{HO
: comma_category_induced_functor_object_of
    (NaturalTransformation.Identity.identity (Overture.fst x),
    NaturalTransformation.Identity.identity (Overture.snd x)) =
  idmap
&
transport
  (fun
     GO : CommaCategory.object (Overture.fst x) (Overture.snd x) ->
          CommaCategory.object (Overture.fst x) (Overture.snd x) =>
   forall s d : CommaCategory.object (Overture.fst x) (Overture.snd x),
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  HO
  (comma_category_induced_functor_morphism_of
     (NaturalTransformation.Identity.identity (Overture.fst x),
     NaturalTransformation.Identity.identity (Overture.snd x))) =
(fun s d : CommaCategory.object (Overture.fst x) (Overture.snd x) => idmap)}
    exists (path_forall _ _ (comma_category_induced_functor_object_of_identity _)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
x: ((A -> C)^op * (B -> C))%category
transport
  (fun
     GO : CommaCategory.object (Overture.fst x) (Overture.snd x) ->
          CommaCategory.object (Overture.fst x) (Overture.snd x) =>
   forall s d : CommaCategory.object (Overture.fst x) (Overture.snd x),
   CommaCategory.morphism s d -> CommaCategory.morphism (GO s) (GO d))
  (path_forall (comma_category_induced_functor_object_of 1) idmap
     (comma_category_induced_functor_object_of_identity x))
  (comma_category_induced_functor_morphism_of
     (NaturalTransformation.Identity.identity (Overture.fst x),
     NaturalTransformation.Identity.identity (Overture.snd x))) =
(fun s d : CommaCategory.object (Overture.fst x) (Overture.snd x) => idmap)
    comma_laws_t.
  Qed.

  Lemma comma_category_projection_functor_composition_of s d d' m m'
  : comma_category_projection_functor_morphism_of
      (@Category.Core.compose _ s d d' m' m)
    = (comma_category_projection_functor_morphism_of m')
        o (comma_category_projection_functor_morphism_of m).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_projection_functor_morphism_of (m' o m) =
comma_category_projection_functor_morphism_of m'
o comma_category_projection_functor_morphism_of m
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_projection_functor_morphism_of (m' o m) =
comma_category_projection_functor_morphism_of m'
o comma_category_projection_functor_morphism_of m
    apply CommaCategory.path_morphism; simpl; [ | reflexivity ].
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
comma_category_induced_functor
  (Core.compose (Overture.fst m) (Overture.fst m'),
  Core.compose (Overture.snd m') (Overture.snd m)) =
(comma_category_induced_functor m' o comma_category_induced_functor m)%functor
    path_functor.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
{HO
: comma_category_induced_functor_object_of
    (Core.compose (Overture.fst m) (Overture.fst m'),
    Core.compose (Overture.snd m') (Overture.snd m)) =
  (fun c : CommaCategory.object (Overture.fst s) (Overture.snd s) =>
   comma_category_induced_functor_object_of m'
     (comma_category_induced_functor_object_of m c))
&
transport
  (fun
     GO : CommaCategory.object (Overture.fst s) (Overture.snd s) ->
          CommaCategory.object (Overture.fst d') (Overture.snd d') =>
   forall s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s),
   CommaCategory.morphism s0 d0 -> CommaCategory.morphism (GO s0) (GO d0))
  HO
  (comma_category_induced_functor_morphism_of
     (Core.compose (Overture.fst m) (Overture.fst m'),
     Core.compose (Overture.snd m') (Overture.snd m))) =
(fun (s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s))
   (m0 : CommaCategory.morphism s0 d0) =>
 comma_category_induced_functor_morphism_of m'
   (comma_category_induced_functor_morphism_of m m0))}
    simpl.
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
{HO
: comma_category_induced_functor_object_of
    (Core.compose (Overture.fst m) (Overture.fst m'),
    Core.compose (Overture.snd m') (Overture.snd m)) =
  (fun c : CommaCategory.object (Overture.fst s) (Overture.snd s) =>
   comma_category_induced_functor_object_of m'
     (comma_category_induced_functor_object_of m c))
&
transport
  (fun
     GO : CommaCategory.object (Overture.fst s) (Overture.snd s) ->
          CommaCategory.object (Overture.fst d') (Overture.snd d') =>
   forall s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s),
   CommaCategory.morphism s0 d0 -> CommaCategory.morphism (GO s0) (GO d0))
  HO
  (comma_category_induced_functor_morphism_of
     (Core.compose (Overture.fst m) (Overture.fst m'),
     Core.compose (Overture.snd m') (Overture.snd m))) =
(fun (s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s))
   (m0 : CommaCategory.morphism s0 d0) =>
 comma_category_induced_functor_morphism_of m'
   (comma_category_induced_functor_morphism_of m m0))}
    exists (path_forall _ _ (comma_category_induced_functor_object_of_compose m' m)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D : PreCategory, P C0 -> P D -> IsHSet (Functor C0 D)
A, B, C: PreCategory
PAB: P (A * B)
P_comma: forall (S : Functor A C) (T : Functor B C), P (S / T)
s, d, d': ((A -> C)^op * (B -> C))%category
m: morphism ((A -> C)^op * (B -> C)) s d
m': morphism ((A -> C)^op * (B -> C)) d d'
transport
  (fun
     GO : CommaCategory.object (Overture.fst s) (Overture.snd s) ->
          CommaCategory.object (Overture.fst d') (Overture.snd d') =>
   forall s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s),
   CommaCategory.morphism s0 d0 -> CommaCategory.morphism (GO s0) (GO d0))
  (path_forall (comma_category_induced_functor_object_of (m' o m))
     (fun x : Overture.fst s / Overture.snd s =>
      comma_category_induced_functor_object_of m'
        (comma_category_induced_functor_object_of m x))
     (comma_category_induced_functor_object_of_compose m' m))
  (comma_category_induced_functor_morphism_of
     (Core.compose (Overture.fst m) (Overture.fst m'),
     Core.compose (Overture.snd m') (Overture.snd m))) =
(fun (s0 d0 : CommaCategory.object (Overture.fst s) (Overture.snd s))
   (m0 : CommaCategory.morphism s0 d0) =>
 comma_category_induced_functor_morphism_of m'
   (comma_category_induced_functor_morphism_of m m0))
    comma_laws_t.
  Qed.

  Definition comma_category_projection_functor
  : Functor ((A -> C)^op * (B -> C))
            (Cat / !((A * B; PAB) : Cat))
    := Build_Functor ((A -> C)^op * (B -> C))
                     (Cat / !((A * B; PAB) : Cat))
                     comma_category_projection_functor_object_of
                     comma_category_projection_functor_morphism_of
                     comma_category_projection_functor_composition_of
                     comma_category_projection_functor_identity_of.
End comma.

Section slice_category_projection_functor.
  Local Open Scope type_scope.
  Context `{Funext}.

  Variable P : PreCategory -> Type.
  Context `{HF : forall C D, P C -> P D -> IsHSet (Functor C D)}.

  Local Abbreviation Cat := (@sub_pre_cat _ P HF).

  Variables C D : PreCategory.

  Hypothesis P1C : P (1 * C).
  Hypothesis PC1 : P (C * 1).
  Hypothesis PC : P C.
  Hypothesis P_comma : forall (S : Functor C D) (T : Functor 1 D), P (S / T).
  Hypothesis P_comma' : forall (S : Functor 1 D) (T : Functor C D), P (S / T).

  Local Open Scope functor_scope.
  Local Open Scope category_scope.

  Local Abbreviation inv D := (@ExponentialLaws.Law1.Functors.inverse _ terminal_category _ _ _ D).

  (** ** Functor [(C → D)ᵒᵖ → D → (cat / C)] *)
  Definition slice_category_projection_functor
  : object (((C -> D)^op) -> (D -> (Cat / ((C; PC) : Cat)))).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op -> D -> Cat / ((C; PC) : Cat))%category
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op -> D -> Cat / ((C; PC) : Cat))%category
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op * D -> Cat / (C; PC))%category
    refine (_ o (Functor.Identity.identity (C -> D)^op,
                 inv D)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((C -> D)^op * (1 -> D)) (Cat / (C; PC))
    refine (_ o @comma_category_projection_functor _ P HF C 1 D PC1 P_comma).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (Cat / !(C * 1; PC1)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
morphism Cat (C * 1; PC1) (C; PC)
    hnf.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (C * 1; PC1).1 (C; PC).1
    exact (ProductLaws.Law1.functor _).
  Defined.

  Definition coslice_category_projection_functor
  : object ((C -> D)^op -> (D -> (Cat / ((C; PC) : Cat)))).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op -> D -> Cat / ((C; PC) : Cat))%category
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op -> D -> Cat / ((C; PC) : Cat))%category
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D)^op * D -> Cat / (C; PC))%category
    refine (_ o (Functor.Identity.identity (C -> D)^op,
                 inv D)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((C -> D)^op * (1 -> D)) (Cat / (C; PC))
    refine (_ o @comma_category_projection_functor _ P HF C 1 D PC1 P_comma).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (Cat / !(C * 1; PC1)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
morphism Cat (C * 1; PC1) (C; PC)
    hnf.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (C * 1; PC1).1 (C; PC).1
    exact (ProductLaws.Law1.functor _).
  Defined.

  (** ** Functor [(C → D) → Dᵒᵖ → (cat / C)] *)
  Definition slice_category_projection_functor'
  : object ((C -> D) -> (D^op -> (Cat / ((C; PC) : Cat)))).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) -> D^op -> Cat / ((C; PC) : Cat))%category
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) -> D^op -> Cat / ((C; PC) : Cat))%category
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) * D^op -> Cat / (C; PC))%category
    refine (_ o (Functor.Identity.identity (C -> D),
                 (inv D)^op)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((C -> D) * (1 -> D)^op) (Cat / (C; PC))
    refine (_ o ProductLaws.Swap.functor _ _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((1 -> D)^op * (C -> D)) (Cat / (C; PC))
    refine (_ o @comma_category_projection_functor _ P HF 1 C D P1C P_comma').
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (Cat / !(1 * C; P1C)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
morphism Cat (1 * C; P1C) (C; PC)
    hnf.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (1 * C; P1C).1 (C; PC).1
    exact (ProductLaws.Law1.functor' _).
  Defined.

  Definition coslice_category_projection_functor'
  : object ((C -> D) -> (D^op -> (Cat / ((C; PC) : Cat)))).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) -> D^op -> Cat / ((C; PC) : Cat))%category
  Proof.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) -> D^op -> Cat / ((C; PC) : Cat))%category
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
((C -> D) * D^op -> Cat / (C; PC))%category
    refine (_ o (Functor.Identity.identity (C -> D),
                 (inv D)^op)).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((C -> D) * (1 -> D)^op) (Cat / (C; PC))
    refine (_ o ProductLaws.Swap.functor _ _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor ((1 -> D)^op * (C -> D)) (Cat / (C; PC))
    refine (_ o @comma_category_projection_functor _ P HF 1 C D P1C P_comma').
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (Cat / !(1 * C; P1C)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
morphism Cat (1 * C; P1C) (C; PC)
    hnf.
H: Funext
P: PreCategory -> Type
HF: forall C0 D0 : PreCategory, P C0 -> P D0 -> IsHSet (Functor C0 D0)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S : Functor C D) (T : Functor 1 D), P (S / T)
P_comma': forall (S : Functor 1 D) (T : Functor C D), P (S / T)
Functor (1 * C; P1C).1 (C; PC).1
    exact (ProductLaws.Law1.functor' _).
  Defined.
End slice_category_projection_functor.