(** * Exponential laws about the terminal category *)
Require Import Category.Core Functor.Core Functor.Identity Functor.Paths ExponentialLaws.Law1.Functors Functor.Composition.Core.
Require Import InitialTerminalCategory.Core.
Require Import Basics.Trunc ExponentialLaws.Tactics.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope functor_scope.

(** ** [C¹ ≅ C] *)
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.

  Definition helper (c : Functor 1 C)
  : Functors.from_terminal C (c (center _)) = 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
c: Functor 1 C
Functors.from_terminal C (c _0 (center 1%category)) = 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
c: Functor 1 C
Functors.from_terminal C (c _0 (center 1%category)) = c
    path_functor.
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
c: Functor 1 C
{HO : (fun _ : 1%category => (c _0 (center 1%category))%object) = c &
transport
  (fun GO : 1%category -> C =>
   forall s d : 1%category, morphism 1 s d -> morphism C (GO s) (GO d))
  HO (fun (s d : 1%category) (_ : morphism 1 s d) => 1%morphism) =
morphism_of c}
    exists (path_forall _ _ (fun x => ap (object_of c) (contr _))).
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
c: Functor 1 C
transport
  (fun GO : 1%category -> C =>
   forall s d : 1%category, morphism 1 s d -> morphism C (GO s) (GO d))
  (path_forall (fun _ : 1%category => (c _0 (center 1%category))%object)
     (fun x : 1%category => (c _0 x)%object)
     (fun x : 1%category => ap c (contr x)))
  (fun (s d : 1%category) (_ : morphism 1 s d) => 1%morphism) =
morphism_of c
    abstract (
        exp_laws_t;
        simpl;
        rewrite <- identity_of;
        f_ap;
        symmetry;
        apply contr
      ).
  Defined.

  Lemma law
  : @functor _ one _ C o inverse C = 1
    /\ inverse C o @functor _ one _ C = 1.
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 o inverse C = 1) * (inverse C o functor C = 1)
  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 o inverse C = 1) * (inverse C o functor C = 1)
    split;
    path_functor.
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
{HO
: (fun c : Functor 1 C => Functors.from_terminal C (c _0 (center 1%category))) =
  idmap
&
transport
  (fun GO : Functor 1 C -> Functor 1 C =>
   forall s d : Functor 1 C,
   Core.NaturalTransformation s d -> Core.NaturalTransformation (GO s) (GO d))
  HO
  (fun (s d : Functor 1 C) (m : Core.NaturalTransformation s d) =>
   Core.Build_NaturalTransformation
     (Functors.from_terminal C (s _0 (center 1%category)))
     (Functors.from_terminal C (d _0 (center 1%category)))
     (fun _ : 1%category => Core.components_of m (center 1%category))
     (fun (s0 d0 : 1%category) (_ : morphism 1 s0 d0) =>
      right_identity C (s _0 (center 1%category)) 
        (d _0 (center 1%category)) (Core.components_of m (center 1%category)) @
      (left_identity C (s _0 (center 1%category)) 
         (d _0 (center 1%category))
         (Core.components_of m (center 1%category)))^)) =
(fun s d : Functor 1 C => idmap)}
    exists (path_forall _ _ helper).
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
transport
  (fun GO : Functor 1 C -> Functor 1 C =>
   forall s d : Functor 1 C,
   Core.NaturalTransformation s d -> Core.NaturalTransformation (GO s) (GO d))
  (path_forall
     (fun c : Functor 1 C =>
      Functors.from_terminal C (c _0 (center 1%category)))
     idmap helper)
  (fun (s d : Functor 1 C) (m : Core.NaturalTransformation s d) =>
   Core.Build_NaturalTransformation
     (Functors.from_terminal C (s _0 (center 1%category)))
     (Functors.from_terminal C (d _0 (center 1%category)))
     (fun _ : 1%category => Core.components_of m (center 1%category))
     (fun (s0 d0 : 1%category) (_ : morphism 1 s0 d0) =>
      right_identity C (s _0 (center 1%category)) 
        (d _0 (center 1%category)) (Core.components_of m (center 1%category)) @
      (left_identity C (s _0 (center 1%category)) 
         (d _0 (center 1%category))
         (Core.components_of m (center 1%category)))^)) =
(fun s d : Functor 1 C => idmap)
    unfold helper.
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
transport
  (fun GO : Functor 1 C -> Functor 1 C =>
   forall s d : Functor 1 C,
   Core.NaturalTransformation s d -> Core.NaturalTransformation (GO s) (GO d))
  (path_forall
     (fun c : Functor 1 C =>
      Functors.from_terminal C (c _0 (center 1%category)))
     idmap
     (fun c : Functor 1 C =>
      path_functor_uncurried
        (Functors.from_terminal C (c _0 (center 1%category))) c
        (path_forall
           (fun _ : 1%category => (c _0 (center 1%category))%object)
           (fun x : 1%category => (c _0 x)%object)
           (fun x : 1%category => ap c (contr x));
        helper_subproof c)))
  (fun (s d : Functor 1 C) (m : Core.NaturalTransformation s d) =>
   Core.Build_NaturalTransformation
     (Functors.from_terminal C (s _0 (center 1%category)))
     (Functors.from_terminal C (d _0 (center 1%category)))
     (fun _ : 1%category => Core.components_of m (center 1%category))
     (fun (s0 d0 : 1%category) (_ : morphism 1 s0 d0) =>
      right_identity C (s _0 (center 1%category)) 
        (d _0 (center 1%category)) (Core.components_of m (center 1%category)) @
      (left_identity C (s _0 (center 1%category)) 
         (d _0 (center 1%category))
         (Core.components_of m (center 1%category)))^)) =
(fun s d : Functor 1 C => idmap)
    exp_laws_t.
  Qed.
End law1.