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 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.
  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.