(** * Functors involving functor categories involving the terminal category *)
Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core NaturalTransformation.Paths.
Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations.
Require Import HoTT.Basics HoTT.Types.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope functor_scope.

Section law1.
  Context `{Funext}.
  Context `{IsInitialCategory zero}.
  Context `{IsTerminalCategory one}.
  Local Notation "0" := zero : category_scope.
  Local Notation "1" := one : category_scope.

  Variable C : PreCategory.

  (** ** [C¹ → C] *)
  Definition functor : Functor (1 -> C) C
    := Build_Functor (1 -> C) C
                     (fun F => F (center _))
                     (fun s d m => m (center _))
                     (fun _ _ _ _ _ => idpath)
                     (fun _ => idpath).

  Definition inverse_morphism_of
             s d (m : morphism C s d)
  : morphism (1 -> C)
             (Functors.from_terminal _ s)
             (Functors.from_terminal _ d).
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s0 d0 : 1%category, Contr (morphism 1 s0 d0)
H2: IsTerminalCategory 1
C: PreCategory
s, d: C
m: morphism C s d
morphism (1 -> C) (from_terminal C s) (from_terminal C d)
  Proof.
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s0 d0 : 1%category, Contr (morphism 1 s0 d0)
H2: IsTerminalCategory 1
C: PreCategory
s, d: C
m: morphism C s d
morphism (1 -> C) (from_terminal C s) (from_terminal C d)
    refine (Build_NaturalTransformation
              (Functors.from_terminal _ s)
              (Functors.from_terminal _ d)
              (fun _ => m)
              _).
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s0 d0 : 1%category, Contr (morphism 1 s0 d0)
H2: IsTerminalCategory 1
C: PreCategory
s, d: C
m: morphism C s d
forall (s0 d0 : 1%category) (m0 : morphism 1 s0 d0),
(m o (from_terminal C s) _1 m0)%morphism =
((from_terminal C d) _1 m0 o m)%morphism
    simpl; intros.
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s1 d1 : 1%category, Contr (morphism 1 s1 d1)
H2: IsTerminalCategory 1
C: PreCategory
s, d: C
m: morphism C s d
s0, d0: 1%category
m0: morphism 1 s0 d0
(m o 1)%morphism = (1 o m)%morphism
    etransitivity;
      [ apply right_identity
      | symmetry; apply left_identity ].
  Defined.

  Global Arguments inverse_morphism_of / _ _ _.

  (** ** [C → C¹] *)
  Definition inverse : Functor C (1 -> C).
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s d : 1%category, Contr (morphism 1 s d)
H2: IsTerminalCategory 1
C: PreCategory
Functor C (1 -> C)
  Proof.
H: Funext
zero: PreCategory
H0: IsInitialCategory 0
one: PreCategory
Contr0: Contr 1%category
H1: forall s d : 1%category, Contr (morphism 1 s d)
H2: IsTerminalCategory 1
C: PreCategory
Functor C (1 -> C)
    refine (Build_Functor
              C (1 -> C)
              (@Functors.from_terminal _ _ _ _ _)
              inverse_morphism_of
              _
              _
           );
    abstract (path_natural_transformation; trivial).
  Defined.
End law1.

Section law1'.
  Context `{Funext}.
  Context `{IsInitialCategory zero}.
  Context `{IsTerminalCategory one}.
  Local Notation "0" := zero : category_scope.
  Local Notation "1" := one : category_scope.

  Variable C : PreCategory.

  #[export] Instance: IsTerminalCategory (C -> 1) := {}.

  (** ** [1ˣ → 1] *)
  Definition functor' : Functor (C -> 1) 1
    := Functors.to_terminal _.

  (** ** [1 → 1ˣ] *)
  Definition inverse' : Functor 1 (C -> 1)
    := Functors.to_terminal _.

  (** ** [1ˣ ≅ 1] *)
  Definition law'
  : functor' o inverse' = 1
    /\ inverse' o functor' = 1
    := center _.
End law1'.