ProjectionFunctors.v

(** * 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 Append "-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 Append "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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type) 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))%type
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))%type)
  (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))%type
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))%type
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))%type
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))%type
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))%type) 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))%type
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))%type) 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))%type
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))%type)
  (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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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))%type
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.