proposition: Corollary Opposite_Adjunction_Transform_invol `(F : D ⟶ C) `(U : C ⟶ D) (A : F ∹ U) : Opposite_Adjunction_Transform (U^op) (F^op) (Opposite_Adjunction_Transform F U A) = A.
proof: Proof. reflexivity. Qed.
imports: Category.Lib Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Opposite Category.Adjunction.Natural.Transformation