(** * Left and right identity laws of adjunction composition *)
Require Import Category.Core Functor.Core.
Require Import Adjoint.Composition.Core Adjoint.Core Adjoint.Identity.
Require Adjoint.Composition.LawsTactic.
Require Import Types.Sigma Types.Prod.

Set Implicit Arguments.
Generalizable All Variables.

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.