(** * Induced functors between comma categories *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Dual.
Require Import Category.Prod.
Require Import NaturalTransformation.Identity.
Require Import FunctorCategory.Core Cat.Core.
Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors.
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 HoTT.Tactics.
Require Import Basics.Tactics.

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

Local Open Scope functor_scope.
Local Open Scope category_scope.

(** ** Morphisms in [(A → C)ᵒᵖ × (B → C)] from [(s₀, s₁)] to [(d₀, d₁)] induce functors [(s₀ / s₁) → (d₀ / d₁)] *)
Section comma_category_induced_functor.
  Context `{Funext}.
  Variables A B C : PreCategory.

  Definition comma_category_induced_functor_object_of s d
             (m : morphism ((A -> C)^op * (B -> C)) s d)
             (x : fst s / snd s)
  : (fst d / snd d)
    := CommaCategory.Build_object
         (fst d) (snd d)
         (CommaCategory.a x)
         (CommaCategory.b x)
         ((snd m) (CommaCategory.b x) o CommaCategory.f x o (fst m) (CommaCategory.a x)).

  Lemma comma_category_induced_functor_object_of_identity s x
  : comma_category_induced_functor_object_of (Category.Core.identity s) x
    = x.
H: Funext
A, B, C: PreCategory
s: (A -> C)^op * (B -> C)
x: fst s / snd s
comma_category_induced_functor_object_of 1 x = x
  Proof.
H: Funext
A, B, C: PreCategory
s: (A -> C)^op * (B -> C)
x: fst s / snd s
comma_category_induced_functor_object_of 1 x = x
    let x1 := match goal with |- ?x1 = ?x2 => constr:(x1) end in
    let x2 := match goal with |- ?x1 = ?x2 => constr:(x2) end in
    apply (CommaCategory.path_object' x1 x2 idpath idpath).
H: Funext
A, B, C: PreCategory
s: (A -> C)^op * (B -> C)
x: fst s / snd s
transport
  (fun X : A =>
   morphism C ((fst s) _0 X)%object
     ((snd s) _0 (CommaCategory.b x))%object) 1
  (transport
     (fun Y : B =>
      morphism C
        ((fst s)
         _0 (CommaCategory.a
               (comma_category_induced_functor_object_of
                  1 x)))%object ((snd s) _0 Y)%object)
     1
     (CommaCategory.f
        (comma_category_induced_functor_object_of 1 x))) =
CommaCategory.f x
    simpl.
H: Funext
A, B, C: PreCategory
s: (A -> C)^op * (B -> C)
x: fst s / snd s
(1 o CommaCategory.f x o 1)%morphism =
CommaCategory.f x
    abstract (rewrite ?left_identity, ?right_identity; reflexivity).
  Defined.

  Definition comma_category_induced_functor_object_of_compose s d d'
             (m : morphism ((A -> C)^op * (B -> C)) d d')
             (m' : morphism ((A -> C)^op * (B -> C)) s d)
             x
  : comma_category_induced_functor_object_of (m o m') x
    = comma_category_induced_functor_object_of
        m
        (comma_category_induced_functor_object_of m' x).
H: Funext
A, B, C: PreCategory
s, d, d': (A -> C)^op * (B -> C)
m: morphism ((A -> C)^op * (B -> C)) d d'
m': morphism ((A -> C)^op * (B -> C)) s d
x: fst s / snd s
comma_category_induced_functor_object_of (m o m') x =
comma_category_induced_functor_object_of m
  (comma_category_induced_functor_object_of m' x)
  Proof.
H: Funext
A, B, C: PreCategory
s, d, d': (A -> C)^op * (B -> C)
m: morphism ((A -> C)^op * (B -> C)) d d'
m': morphism ((A -> C)^op * (B -> C)) s d
x: fst s / snd s
comma_category_induced_functor_object_of (m o m') x =
comma_category_induced_functor_object_of m
  (comma_category_induced_functor_object_of m' x)
    let x1 := match goal with |- ?x1 = ?x2 => constr:(x1) end in
    let x2 := match goal with |- ?x1 = ?x2 => constr:(x2) end in
    apply (CommaCategory.path_object' x1 x2 idpath idpath).
H: Funext
A, B, C: PreCategory
s, d, d': (A -> C)^op * (B -> C)
m: morphism ((A -> C)^op * (B -> C)) d d'
m': morphism ((A -> C)^op * (B -> C)) s d
x: fst s / snd s
transport
  (fun X : A =>
   morphism C ((fst d') _0 X)%object
     ((snd d')
      _0 (CommaCategory.b
            (comma_category_induced_functor_object_of
               m
               (comma_category_induced_functor_object_of
                  m' x))))%object) 1
  (transport
     (fun Y : B =>
      morphism C
        ((fst d')
         _0 (CommaCategory.a
               (comma_category_induced_functor_object_of
                  (m o m') x)))%object
        ((snd d') _0 Y)%object) 1
     (CommaCategory.f
        (comma_category_induced_functor_object_of
           (m o m') x))) =
CommaCategory.f
  (comma_category_induced_functor_object_of m
     (comma_category_induced_functor_object_of m' x))
    abstract (
        destruct m', m, x;
        simpl in *;
          rewrite !associativity;
        reflexivity
      ).
  Defined.

  Definition comma_category_induced_functor_morphism_of s d m s0 d0
             (m0 : morphism (fst s / snd s) s0 d0)
  : morphism (fst d / snd d)
             (@comma_category_induced_functor_object_of s d m s0)
             (@comma_category_induced_functor_object_of s d m d0).
H: Funext
A, B, C: PreCategory
s, d: (CC_Functor' A C * CC_Functor' B C)%type
m: morphism ((A -> C)^op * (B -> C)) s d
s0, d0: fst s / snd s
m0: morphism (fst s / snd s) s0 d0
morphism (fst d / snd d)
  (comma_category_induced_functor_object_of m s0)
  (comma_category_induced_functor_object_of m d0)
  Proof.
H: Funext
A, B, C: PreCategory
s, d: (CC_Functor' A C * CC_Functor' B C)%type
m: morphism ((A -> C)^op * (B -> C)) s d
s0, d0: fst s / snd s
m0: morphism (fst s / snd s) s0 d0
morphism (fst d / snd d)
  (comma_category_induced_functor_object_of m s0)
  (comma_category_induced_functor_object_of m d0)
    simpl.
H: Funext
A, B, C: PreCategory
s, d: (CC_Functor' A C * CC_Functor' B C)%type
m: morphism ((A -> C)^op * (B -> C)) s d
s0, d0: fst s / snd s
m0: morphism (fst s / snd s) s0 d0
CommaCategory.morphism
  (comma_category_induced_functor_object_of m s0)
  (comma_category_induced_functor_object_of m d0)
    let s := match goal with |- CommaCategory.morphism ?s ?d => constr:(s) end in
    let d := match goal with |- CommaCategory.morphism ?s ?d => constr:(d) end in
    refine (CommaCategory.Build_morphism s d (CommaCategory.g m0) (CommaCategory.h m0) _);
      simpl in *; clear.
A, B, C: PreCategory
s, d: (Functor A C * Functor B C)%type
m: (NaturalTransformation (fst d) (fst s) *
 NaturalTransformation (snd s) (snd d))%type
s0, d0: CommaCategory.object (fst s) (snd s)
m0: CommaCategory.morphism s0 d0
((snd d) _1 (CommaCategory.h m0)
 o (snd m (CommaCategory.b s0) o CommaCategory.f s0
    o fst m (CommaCategory.a s0)))%morphism =
(snd m (CommaCategory.b d0) o CommaCategory.f d0
 o fst m (CommaCategory.a d0)
 o (fst d) _1 (CommaCategory.g m0))%morphism
    abstract (
        destruct_head prod;
        destruct_head CommaCategory.morphism;
        destruct_head CommaCategory.object;
        simpl in *;
          repeat (try_associativity_quick (rewrite <- !commutes || (progress f_ap)));
        repeat (try_associativity_quick (rewrite !commutes || (progress f_ap)));
        assumption
      ). (* 3.495 s *)
  Defined.

  Definition comma_category_induced_functor s d
             (m : morphism ((A -> C)^op * (B -> C)) s d)
  : Functor (fst s / snd s) (fst d / snd d).
H: Funext
A, B, C: PreCategory
s, d: (A -> C)^op * (B -> C)
m: morphism ((A -> C)^op * (B -> C)) s d
Functor (fst s / snd s) (fst d / snd d)
  Proof.
H: Funext
A, B, C: PreCategory
s, d: (A -> C)^op * (B -> C)
m: morphism ((A -> C)^op * (B -> C)) s d
Functor (fst s / snd s) (fst d / snd d)
    refine (Build_Functor (fst s / snd s) (fst d / snd d)
                          (@comma_category_induced_functor_object_of s d m)
                          (@comma_category_induced_functor_morphism_of s d m)
                          _
                          _
           );
    abstract (
        intros; apply CommaCategory.path_morphism; reflexivity
      ).
  Defined.
End comma_category_induced_functor.

(** ** Morphisms in [C] from [a] to [a'] induce functors [(C / a) → (C / a')] *)
Section slice_category_induced_functor.
  Context `{Funext}.
  Variable C : PreCategory.

  Section slice_coslice.
    Variable D : PreCategory.

    (** TODO(JasonGross): See if this can be recast as an exponential law functor about how [1 → Cat] is isomorphic to [Cat], or something *)
    Definition slice_category_induced_functor_nt s d (m : morphism D s d)
    : NaturalTransformation !s !d.
H: Funext
C, D: PreCategory
s, d: D
m: morphism D s d
NaturalTransformation !s !d
    Proof.
H: Funext
C, D: PreCategory
s, d: D
m: morphism D s d
NaturalTransformation !s !d
      exists (fun _ : Unit => m);
      simpl; intros; clear;
      abstract (autorewrite with category; reflexivity).
    Defined.

    Variable F : Functor C D.
    Variable a : D.

    Section slice.
      Definition slice_category_induced_functor F' a'
                 (m : morphism D a a')
                 (T : NaturalTransformation F' F)
      : Functor (F / a) (F' / a')
        := comma_category_induced_functor
             (s := (F, !a))
             (d := (F', !a'))
             (T, @slice_category_induced_functor_nt a a' m).

      Definition slice_category_nt_induced_functor F' T
        := @slice_category_induced_functor F' a 1 T.
      Definition slice_category_morphism_induced_functor a' m
        := @slice_category_induced_functor F a' m 1.
    End slice.

    Section coslice.
      Definition coslice_category_induced_functor F' a'
                 (m : morphism D a' a)
                 (T : NaturalTransformation F F')
      : Functor (a / F) (a' / F')
        := comma_category_induced_functor
             (s := (!a, F))
             (d := (!a', F'))
             (@slice_category_induced_functor_nt a' a m, T).

      Definition coslice_category_nt_induced_functor F' T
        := @coslice_category_induced_functor F' a 1 T.
      Definition coslice_category_morphism_induced_functor a' m
        := @coslice_category_induced_functor F a' m 1.
    End coslice.
  End slice_coslice.

  Definition slice_category_over_induced_functor a a' (m : morphism C a a')
  : Functor (C / a) (C / a')
    := Eval hnf in slice_category_morphism_induced_functor _ _ _ m.
  Definition coslice_category_over_induced_functor a a' (m : morphism C a' a)
  : Functor (a \ C) (a' \ C)
    := Eval hnf in coslice_category_morphism_induced_functor _ _ _ m.
End slice_category_induced_functor.

(** ** Functors [A → A'] functors [(cat / A) → (cat / A')] *)
Section cat_over_induced_functor.
  Local Open Scope type_scope.

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

  Local Notation cat := (@sub_pre_cat _ P H0).

  Definition cat_over_induced_functor a a' (m : morphism cat a a')
  : Functor (cat / a) (cat / a')
    := slice_category_over_induced_functor cat a a' m.

  Definition over_cat_induced_functor a a' (m : morphism cat a' a)
  : Functor (a \ cat) (a' \ cat)
    := coslice_category_over_induced_functor cat a a' m.
End cat_over_induced_functor.