(** * Natural transformations between functors from initial categories and to terminal categories *)
Require Import Category.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths.
Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors.
Require Import Contractible.

Set Implicit Arguments.
Generalizable All Variables.

Section NaturalTransformations.
  Variable C : PreCategory.

  Definition from_initial
             `{@IsInitialCategory zero} (F G : Functor zero C)
  : NaturalTransformation F G
    := Build_NaturalTransformation
         F G
         (fun x => initial_category_ind _ x)
         (fun x _ _ => initial_category_ind _ x).

  #[export] Instance trunc_from_initial
         `{Funext}
         `{@IsInitialCategory zero} (F G : Functor zero C)
  : Contr (NaturalTransformation F G).
C: PreCategory
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
F, G: Functor zero C
Contr (NaturalTransformation F G)
  Proof.
C: PreCategory
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
F, G: Functor zero C
Contr (NaturalTransformation F G)
    refine (Build_Contr _ (from_initial F G) _).
C: PreCategory
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
F, G: Functor zero C
forall y : NaturalTransformation F G, from_initial F G = y
    abstract (
        intros;
        apply path_natural_transformation;
        intro x;
        exact (initial_category_ind _ x)
      ).
  Defined.

  Local Existing Instance Functors.to_initial_category_empty.

  #[export] Instance trunc_to_initial
         `{Funext}
         `{@IsInitialCategory zero}
         (F G : Functor zero C)
  : Contr (NaturalTransformation F G)
    := trunc_from_initial F G.

  Definition to_terminal
             `{@IsTerminalCategory one H1 H2} (F G : Functor C one)
  : NaturalTransformation F G
    := Build_NaturalTransformation
         F G
         (fun x => center _)
         (fun _ _ _ => path_contr _ _).

  #[export] Instance trunc_to_terminal
         `{Funext}
         `{@IsTerminalCategory one H1 H2} (F G : Functor C one)
  : Contr (NaturalTransformation F G).
C: PreCategory
H: Funext
one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
F, G: Functor C one
Contr (NaturalTransformation F G)
  Proof.
C: PreCategory
H: Funext
one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
F, G: Functor C one
Contr (NaturalTransformation F G)
    refine (Build_Contr _ (to_terminal F G) _).
C: PreCategory
H: Funext
one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
F, G: Functor C one
forall y : NaturalTransformation F G, to_terminal F G = y
    abstract (path_natural_transformation; exact (contr _)).
  Defined.
End NaturalTransformations.