We prove the equivalence of the two definitions of adjunction.

Require Import
  abstract_algebra theory.setoids interfaces.functors theory.categories
  workaround_tactics theory.jections.
Require dual.

Local Hint Unfold id compose: typeclass_instances. LocalLocal
Lemma equal_because_sole `{Setoid T} (P: T Prop) x: is_sole P x forall y z, P y P z y = z.

Section for_φAdjunction.

  Context `(Adjunction).

  Implicit Arguments φ [[d] [c]].

  Let hint''''' := _adjunction_bijective F G.
  Let hint'''' x y: Injective (@ x y) := _.
  Let hint := _adjunction_left_functor F G.
  Let hint' := _adjunction_right_functor F G.
  Let hint'' := functor_from G.
  Let hint''' := functor_to G.

  Lemma _adjunction_natural_right_inv `(g: c G d) `(h: c' c): ⁻¹ (g h) = ⁻¹ g fmap F h.

  Lemma _adjunction_natural_left_inv `(g: c G d) `(k: d d'): ⁻¹ (fmap G k g) = k ⁻¹ g.

  Let η: id G F := λ c, (cat_id: F c F c).
  Let ε: F G id := λ d, ⁻¹ (cat_id: G d G d).

  Global Instance η_natural: NaturalTransformation η.

  Global Instance: NaturalTransformation ε.

  Lemma _in_terms_of_η `(f: F x a): f = fmap G f η x.

  Lemma _in_terms_of_ε `(g: x G a): ⁻¹ g = ε a fmap F g.

  Definition univwit (c : C) (d : D): (c G d) (F c d) := ⁻¹.

  Instance: c, UniversalArrow (η c: c G (F c)) (univwit c).

  Instance Adjunction_ηAdjunction: ηAdjunction F G η univwit := {}.

  Instance Adjunction_ηεAdjunction: ηεAdjunction F G η ε.

  Goal @Adjunction D _ _ _ _ C _ _ _ _ G (dual.fmap_op G) F (dual.fmap_op F) (λ d c, (@ c d)⁻¹)
    (λ d c, @ c d).

End for_φAdjunction.

Section for_ηAdjunction.

  Context `(ηAdjunction).

  Let hint := η_adjunction_left_functor F G.
  Let hint' := η_adjunction_right_functor F G.
  Let hint'' := functor_from G.
  Let hint''' := functor_to G.

  Let x a (g: F x a): (x G a) := fmap G g η x.

  Instance: (c: C) (d: D), Inverse (@ c d) := uniwit.

  Instance: x a, Surjective (@ x a).

  Instance: x a, Injective (@ x a).

  Instance: x a, Bijective (@ x a) := {}.

  Instance ηAdjunction_φAdjunction: Adjunction F G .

End for_ηAdjunction.

Section for_ηεAdjunction.

  Context `(ηεAdjunction).

  Let hint := ηε_adjunction_left_functor F G.
  Let hint' := ηε_adjunction_right_functor F G.
  Let hint'' := functor_from G.
  Let hint''' := functor_to G.
  Let hint'''' := ηε_adjunction_η_natural F G.
  Let hint''''' := ηε_adjunction_ε_natural F G.

  Let `(f: F c d): (c G d) := fmap G f η c.
  Instance uniwit c d: Inverse ( c d) := λ f, ε d fmap F f.

  Instance ηεAdjunction_ηAdjunction: ηAdjunction F G η uniwit.

  Instance ηεAdjunction_φAdjunction: Adjunction F G .

End for_ηεAdjunction.