(** * Opposite adjunction [F ⊣ G → Gᵒᵖ ⊣ Fᵒᵖ] *)
Require Import Category.Core Functor.Core.
Require Import Functor.Dual NaturalTransformation.Dual.
Require Import Adjoint.UnitCounit Adjoint.Core.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.

(** ** Definition of [Aᵒᵖ] *)
Definition opposite
           C D
           (F : Functor C D)
           (G : Functor D C)
           (A : F -| G)
: G^op -| F^op
  := @Build_AdjunctionUnitCounit
       _ _ (G^op) (F^op)
       ((counit A)^op)
       ((unit A)^op)
       (unit_counit_equation_2 A)
       (unit_counit_equation_1 A).

Local Notation "A ^op" := (opposite A) : adjunction_scope.

Local Open Scope adjunction_scope.

(** ** [ᵒᵖ] is judgmentally involutive *)
Definition opposite_involutive C D (F : Functor C D) (G : Functor D C) (A : F -| G)
: (A^op)^op = A
  := idpath.

Module Export AdjointDualNotations.
  Notation "A ^op" := (opposite A) : adjunction_scope.
End AdjointDualNotations.