(** * Functors to and from initial and terminal categories *)
Require Import Category.Core Functor.Core Functor.Paths.
Require Import InitialTerminalCategory.Core.
Require Import NatCategory.
Require Import HoTT.Basics.

Set Implicit Arguments.
Generalizable All Variables.

Section functors.
  Variable C : PreCategory.

  (** *** Functor to any terminal category *)
  Definition to_terminal `{@IsTerminalCategory one Hone Hone'}
  : Functor C one
    := Build_Functor
         C one
         (fun _ => center _)
         (fun _ _ _ => center _)
         (fun _ _ _ _ _ => contr _)
         (fun _ => contr _).

  (** *** Constant functor from any terminal category *)
  Definition from_terminal `{@IsTerminalCategory one Hone Hone'} (c : C)
  : Functor one C
    := Build_Functor
         one C
         (fun _ => c)
         (fun _ _ _ => identity c)
         (fun _ _ _ _ _ => symmetry _ _ (@identity_identity _ _))
         (fun _ => idpath).

  (** *** Functor from any initial category *)
  Definition from_initial `{@IsInitialCategory zero}
  : Functor zero C
    := Build_Functor
         zero C
         (fun x => initial_category_ind _ x)
         (fun x _ _ => initial_category_ind _ x)
         (fun x _ _ _ _ => initial_category_ind _ x)
         (fun x => initial_category_ind _ x).
End functors.

Local Arguments to_terminal / .
Local Arguments from_terminal / .
Local Arguments from_initial / .

Definition to_1 C : Functor C 1
  := Eval simpl in to_terminal C.
Definition from_1 C c : Functor 1 C
  := Eval simpl in from_terminal C c.
Definition from_0 C : Functor 0 C
  := Eval simpl in from_initial C.

Local Notation "! x" := (@from_terminal _ terminal_category _ _ _ x) : functor_scope.

(** *** Uniqueness principles about initial and terminal categories and functors *)
Section unique.
  Context `{Funext}.

  #[export] Instance trunc_initial_category_function
         `{@IsInitialCategory zero} T
  : Contr (zero -> T).
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
T: Type
Contr (zero -> T)
  Proof.
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
T: Type
Contr (zero -> T)
    refine (Build_Contr _ (initial_category_ind _) _).
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
T: Type
forall y : zero -> T, initial_category_ind T = y
    intro y.
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
T: Type
y: zero -> T
initial_category_ind T = y
    apply path_forall; intro x.
H: Funext
zero: PreCategory
H0: IsInitialCategory zero
T: Type
y: zero -> T
x: zero
initial_category_ind T x = y x
    exact (initial_category_ind _ x).
  Defined.

  Variable C : PreCategory.

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

  #[export] Instance trunc_to_initial_category
         `{@IsInitialCategory zero}
  : IsHProp (Functor C zero).
H: Funext
C, zero: PreCategory
H0: IsInitialCategory zero
IsHProp (Functor C zero)
  Proof.
H: Funext
C, zero: PreCategory
H0: IsInitialCategory zero
IsHProp (Functor C zero)
    typeclasses eauto.
  Qed.

  Definition to_initial_category_empty
             `{@IsInitialCategory zero}
             (F : Functor C zero)
  : IsInitialCategory C
    := fun P x => initial_category_ind P (F x).

  #[export] Instance trunc_terminal_category
         `{@IsTerminalCategory one H1 H2}
  : Contr (Functor C one).
H: Funext
C, one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
Contr (Functor C one)
  Proof.
H: Funext
C, one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
Contr (Functor C one)
    refine (Build_Contr _ (to_terminal C) _).
H: Funext
C, one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
forall y : Functor C one, to_terminal C = y
    intros.
H: Funext
C, one: PreCategory
H1: Contr one
H2: forall s d : one, Contr (morphism one s d)
H0: IsTerminalCategory one
y: Functor C one
to_terminal C = y
    exact (center _).
  Defined.
End unique.

Module Export InitialTerminalCategoryFunctorsNotations.
  Notation "! x" := (@from_terminal _ terminal_category _ _ _ x) : functor_scope.
End InitialTerminalCategoryFunctorsNotations.