(** * Left and right identity laws of adjunction composition *)
Require Import Category.Core Functor.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Adjoint.Composition.Core Adjoint.Core Adjoint.Identity.
Require Adjoint.Composition.LawsTactic.
Require Import Types.Sigma Types.Prod.

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

Local Open Scope adjunction_scope.
Local Open Scope morphism_scope.

Section identity_lemmas.
  Local Notation AdjunctionWithFunctors C D :=
    { fg : Functor C D * Functor D C
    | fst fg -| snd fg }.

  Context `{Funext}.

  Variables C D : PreCategory.

  Variable F : Functor C D.
  Variable G : Functor D C.

  Variable A : F -| G.

  Local Open Scope adjunction_scope.

  Lemma left_identity
  : ((_, _); 1 o A) = ((_, _); A) :> AdjunctionWithFunctors C D.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
((Functor.Composition.Core.compose
    (Functor.Identity.identity D) F,
 Functor.Composition.Core.compose G
   (Functor.Identity.identity D)); 1 o A) =
((F, G); A)
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
((Functor.Composition.Core.compose
    (Functor.Identity.identity D) F,
 Functor.Composition.Core.compose G
   (Functor.Identity.identity D)); 1 o A) =
((F, G); A)
    apply path_sigma_uncurried; simpl.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
{p
: (Functor.Composition.Core.compose
     (Functor.Identity.identity D) F,
  Functor.Composition.Core.compose G
    (Functor.Identity.identity D)) = (F, G) &
transport
  (fun fg : Functor C D * Functor D C =>
   fst fg -| snd fg) p (1 o A) = A}
    (exists (path_prod'
               (Functor.Composition.Laws.left_identity _)
               (Functor.Composition.Laws.right_identity _))).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
transport
  (fun fg : Functor C D * Functor D C =>
   fst fg -| snd fg)
  (path_prod' (Laws.left_identity F)
     (Laws.right_identity G)) (1 o A) = A
    Adjoint.Composition.LawsTactic.law_t.
  Qed.

  Lemma right_identity
  : ((_, _); A o 1) = ((_, _); A) :> AdjunctionWithFunctors C D.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
((Functor.Composition.Core.compose F
    (Functor.Identity.identity C),
 Functor.Composition.Core.compose
   (Functor.Identity.identity C) G); A o 1) =
((F, G); A)
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
((Functor.Composition.Core.compose F
    (Functor.Identity.identity C),
 Functor.Composition.Core.compose
   (Functor.Identity.identity C) G); A o 1) =
((F, G); A)
    apply path_sigma_uncurried; simpl.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
{p
: (Functor.Composition.Core.compose F
     (Functor.Identity.identity C),
  Functor.Composition.Core.compose
    (Functor.Identity.identity C) G) = (F, G) &
transport
  (fun fg : Functor C D * Functor D C =>
   fst fg -| snd fg) p (A o 1) = A}
    (exists (path_prod'
               (Functor.Composition.Laws.right_identity _)
               (Functor.Composition.Laws.left_identity _))).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: F -| G
transport
  (fun fg : Functor C D * Functor D C =>
   fst fg -| snd fg)
  (path_prod' (Laws.right_identity F)
     (Laws.left_identity G)) (A o 1) = A
    Adjoint.Composition.LawsTactic.law_t.
  Qed.
End identity_lemmas.

#[export]
Hint Rewrite @left_identity @right_identity : category.
#[export]
Hint Immediate left_identity right_identity : category.