(** * Functoriality of the comma category construction with projection functors *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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.
Local Set Warnings "-notation-overridden". (* work around bug #5567, https://coq.inria.fr/bugs/show_bug.cgi?id=5567, notation-overridden,parsing should not trigger for only printing notations *)
Import Comma.Core.
Local Set Warnings "notation-overridden".
Require Import Comma.InducedFunctors Comma.Projection.
Require ProductLaws ExponentialLaws.Law1.Functors ExponentialLaws.Law4.Functors.
Require Import Types.Forall PathGroupoids HoTT.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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 Notation 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
Cat / !((A * B; PAB) : Cat)
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
Cat / !((A * B; PAB) : Cat)
    exists (Basics.Overture.fst ST / Basics.Overture.snd ST; P_comma _ _) (center _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
comma_category_projection_functor_morphism_of 1 = 1
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
comma_category_projection_functor_morphism_of 1 = 1
    apply CommaCategory.path_morphism; simpl; [ | reflexivity ].
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
{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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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
    d : CommaCategory.object (Overture.fst s)
          (Overture.snd s),
   CommaCategory.morphism s0 d ->
   CommaCategory.morphism (GO s0) (GO d)) 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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
    d : CommaCategory.object (Overture.fst s)
          (Overture.snd s),
   CommaCategory.morphism s0 d ->
   CommaCategory.morphism (GO s0) (GO d)) 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C 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)
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
    d : CommaCategory.object (Overture.fst s)
          (Overture.snd s),
   CommaCategory.morphism s0 d ->
   CommaCategory.morphism (GO s0) (GO d))
  (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 Notation 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 Notation 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op -> D -> Cat / ((C; PC) : Cat)
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op -> D -> Cat / ((C; PC) : Cat)
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op * D -> Cat / (C; PC)
    refine (_ o (Functor.Identity.identity (C -> D)^op,
                 inv D)).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor (Cat / !(C * 1; PC1)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
morphism Cat (C * 1; PC1) (C; PC)
    hnf.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op -> D -> Cat / ((C; PC) : Cat)
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op -> D -> Cat / ((C; PC) : Cat)
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D)^op * D -> Cat / (C; PC)
    refine (_ o (Functor.Identity.identity (C -> D)^op,
                 inv D)).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor (Cat / !(C * 1; PC1)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
morphism Cat (C * 1; PC1) (C; PC)
    hnf.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) -> D^op -> Cat / ((C; PC) : Cat)
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) -> D^op -> Cat / ((C; PC) : Cat)
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) * D^op -> Cat / (C; PC)
    refine (_ o (Functor.Identity.identity (C -> D),
                 (inv D)^op)).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor ((C -> D) * (1 -> D)^op) (Cat / (C; PC))
    refine (_ o ProductLaws.Swap.functor _ _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor (Cat / !(1 * C; P1C)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
morphism Cat (1 * C; P1C) (C; PC)
    hnf.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) -> D^op -> Cat / ((C; PC) : Cat)
  Proof.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) -> D^op -> Cat / ((C; PC) : Cat)
    refine ((ExponentialLaws.Law4.Functors.inverse _ _ _) _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
(C -> D) * D^op -> Cat / (C; PC)
    refine (_ o (Functor.Identity.identity (C -> D),
                 (inv D)^op)).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor ((C -> D) * (1 -> D)^op) (Cat / (C; PC))
    refine (_ o ProductLaws.Swap.functor _ _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / 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)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor (Cat / !(1 * C; P1C)) (Cat / (C; PC))
    refine (cat_over_induced_functor _).
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
morphism Cat (1 * C; P1C) (C; PC)
    hnf.
H: Funext
P: (PreCategory -> Type)%type
HF: forall C D : PreCategory,
P C -> P D -> IsHSet (Functor C D)
C, D: PreCategory
P1C: P (1 * C)
PC1: P (C * 1)
PC: P C
P_comma: forall (S0 : Functor C D) 
(T : Functor 1 D), P (S0 / T)
P_comma': forall (S0 : Functor 1 D)
(T : Functor C D), P (S0 / T)
Functor (1 * C; P1C).1 (C; PC).1
    exact (ProductLaws.Law1.functor' _).
  Defined.
End slice_category_projection_functor.