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.
  Proof.
    apply path_sigma_uncurried; simpl.
    (∃ (path_prod'
               (Functor.Composition.Laws.left_identity _)
               (Functor.Composition.Laws.right_identity _))).
    Adjoint.Composition.LawsTactic.law_t.
  Qed.

  Lemma right_identity
  : ((_, _); A o 1) = ((_, _); A) :> AdjunctionWithFunctors C D.
  Proof.
    apply path_sigma_uncurried; simpl.
    (∃ (path_prod'
               (Functor.Composition.Laws.right_identity _)
               (Functor.Composition.Laws.left_identity _))).
    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.