(** * Coercions between hom-set adjunctions and unit+counit adjunctions *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Hom.
Require Import Category.Morphisms.
Require Import Functor.Composition.Core.
Require Import FunctorCategory.Morphisms.
Require Import Functor.Identity.
Require Import SetCategory.Morphisms.
Require Import Basics.Trunc Types.Sigma HoTT.Tactics Equivalences.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope path_scope.
Local Open Scope morphism_scope.
Local Open Scope category_scope.
Local Open Scope functor_scope.
Local Open Scope natural_transformation_scope.

(** ** unit+UMP from hom-set adjunction *)
Section AdjunctionEquivalences.
  Context `{Funext}.
  Variables C D : PreCategory.
  Variable F : Functor C D.
  Variable G : Functor D C.

  Local Open Scope morphism_scope.

  (** We need to jump through some hoops with [simpl] for speed *)
  Section adjunction_naturality.
    Variable A : AdjunctionHom F G.

    Section nat1.
      Context c d d'
              (f : morphism D (F c) d)
              (g : morphism D d d').

      Let adjunction_naturalityT
        := Eval simpl in
            G _1 g o A (c, d) f = A (c, d') (g o f).

      Lemma adjunction_naturality : adjunction_naturalityT.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d, d': D
f: morphism D (F _0 c)%object d
g: morphism D d d'
adjunction_naturalityT:= G _1 g o A (c, d) f =
A (c, d') (g o f): Type
adjunction_naturalityT
      Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d, d': D
f: morphism D (F _0 c)%object d
g: morphism D d d'
adjunction_naturalityT:= G _1 g o A (c, d) f =
A (c, d') (g o f): Type
adjunction_naturalityT
        pose proof (ap10 (commutes A (c, d) (c, d') (1%morphism, g))^ f) as H'; simpl in *.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d, d': D
f: morphism D (F _0 c)%object d
g: morphism D d d'
adjunction_naturalityT:= G _1 g o A (c, d) f =
A (c, d') (g o f): Type
H': G _1 g o A (c, d) f o 1 =
A (c, d') (g o f o F _1 1)
adjunction_naturalityT
        rewrite ?identity_of, ?left_identity, ?right_identity in H'.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d, d': D
f: morphism D (F _0 c)%object d
g: morphism D d d'
adjunction_naturalityT:= G _1 g o A (c, d) f =
A (c, d') (g o f): Type
H': G _1 g o A (c, d) f = A (c, d') (g o f)
adjunction_naturalityT
        exact H'.
      Qed.
    End nat1.

    Section nat2.
      Context c c' d
              (f : morphism D (F c') d)
              (g : morphism C c c').

      Let adjunction_naturalityT'
        := Eval simpl in
            A (c', d) f o g = A (c, d) (f o F _1 g).

      Lemma adjunction_naturality' : adjunction_naturalityT'.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c, c': C
d: D
f: morphism D (F _0 c')%object d
g: morphism C c c'
adjunction_naturalityT':= A (c', d) f o g =
A (c, d) (f o F _1 g): Type
adjunction_naturalityT'
      Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c, c': C
d: D
f: morphism D (F _0 c')%object d
g: morphism C c c'
adjunction_naturalityT':= A (c', d) f o g =
A (c, d) (f o F _1 g): Type
adjunction_naturalityT'
        pose proof (ap10 (commutes A (c', d) (c, d) (g, 1%morphism))^ f) as H'; simpl in *.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c, c': C
d: D
f: morphism D (F _0 c')%object d
g: morphism C c c'
adjunction_naturalityT':= A (c', d) f o g =
A (c, d) (f o F _1 g): Type
H': G _1 1 o A (c', d) f o g =
A (c, d) (1 o f o F _1 g)
adjunction_naturalityT'
        rewrite ?identity_of, ?left_identity, ?right_identity in H'.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c, c': C
d: D
f: morphism D (F _0 c')%object d
g: morphism C c c'
adjunction_naturalityT':= A (c', d) f o g =
A (c, d) (f o F _1 g): Type
H': A (c', d) f o g = A (c, d) (f o F _1 g)
adjunction_naturalityT'
        exact H'.
      Qed.
    End nat2.
  End adjunction_naturality.

  (**
     Quoting from Awodey's "Category Theory":

     Proposition 9.4. Given categories and functors,

     [F : C ↔ D : G]

     the following conditions are equivalent:

     1. [F] is left adjoint to [G]; that is, there is a natural
        transformation

        [η : 1_C → G ∘ F]

        that has the UMP of the unit:

        For any [c : C], [d : D] and [f : c -> G d] there exists a
        unique [g : F c → d] such that [f = G g ∘ η c].

     2. For any [c : C] and [d : D] there is an isomorphism,

        [ϕ : Hom_D (F c, d) ≅ Hom_C (c, G d)]

        that is natural in both [c] and [d].

     Moreover, the two conditions are related by the formulas

     [ϕ g = G g ∘ η c]

     [η c = ϕ(1_{F c})]
     *)

  Lemma adjunction_unit__of__adjunction_hom_helper (A : AdjunctionHom F G)
        (c : C) (d : D) (f : morphism C c (G d))
  : IsHProp {g : morphism D (F c) d & G _1 g o A (c, F c) 1 = f}.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
IsHProp
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f}
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
IsHProp
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f}
    apply hprop_allpath.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
forall
x
 y : {g : morphism D (F _0 c)%object d &
     G _1 g o A (c, (F _0 c)%object) 1 = f}, x = y
    intros [g0 H0] [g1 H1]; apply path_sigma_hprop; simpl.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
g0: morphism D (F _0 c)%object d
H0: G _1 g0 o A (c, (F _0 c)%object) 1 = f
g1: morphism D (F _0 c)%object d
H1: G _1 g1 o A (c, (F _0 c)%object) 1 = f
g0 = g1
    destruct H1.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: G _1 g0 o A (c, (F _0 c)%object) 1 =
G _1 g1 o A (c, (F _0 c)%object) 1
g0 = g1
    rewrite !adjunction_naturality in H0.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) (g0 o 1) = A (c, d) (g1 o 1)
g0 = g1
    rewrite !right_identity in H0.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) g0 = A (c, d) g1
g0 = g1
    change (idmap g0 = idmap g1).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) g0 = A (c, d) g1
idmap g0 = idmap g1
    rewrite <- (ap10 (@left_inverse _ _ _ (A (c, d)) _)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) g0 = A (c, d) g1
((A (c, d))^-1 o A (c, d)) g0 = g1
    simpl rewrite H0.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) g0 = A (c, d) g1
A^-1 (c, d) (A (c, d) g1) = g1
    let k := constr:(ap10 (@left_inverse _ _ _ (A (c, d)) _)) in
    simpl rewrite k. (* https://coq.inria.fr/bugs/show_bug.cgi?id=3773 and https://coq.inria.fr/bugs/show_bug.cgi?id=3772 (probably) *)
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
g0, g1: morphism D (F _0 c)%object d
H0: A (c, d) g0 = A (c, d) g1
g1 = g1
    reflexivity.
  Qed.

  Lemma adjunction_unit__of__adjunction_hom__mate_of__commutes
        (A : AdjunctionHom F G) (s d : C) (m : morphism C s d)
  : A (d, F d) 1 o m = G _1 (F _1 m) o A (s, F s) 1.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
s, d: C
m: morphism C s d
A (d, (F _0 d)%object) 1 o m =
G _1 (F _1 m) o A (s, (F _0 s)%object) 1
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
s, d: C
m: morphism C s d
A (d, (F _0 d)%object) 1 o m =
G _1 (F _1 m) o A (s, (F _0 s)%object) 1
    simpl; rewrite adjunction_naturality', adjunction_naturality.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
s, d: C
m: morphism C s d
A (s, (F _0 d)%object) (1 o F _1 m) =
A (s, (F _0 d)%object) (F _1 m o 1)
    rewrite ?left_identity, ?right_identity.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
s, d: C
m: morphism C s d
A (s, (F _0 d)%object) (F _1 m) =
A (s, (F _0 d)%object) (F _1 m)
    reflexivity.
  Qed.

  Definition adjunction_unit__of__adjunction_hom (A : AdjunctionHom F G)
  : AdjunctionUnit F G.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
AdjunctionUnit F G
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
AdjunctionUnit F G
    exists (Build_NaturalTransformation
              1 (G o F)
              (fun c => A (c, F c) 1)
              (adjunction_unit__of__adjunction_hom__mate_of__commutes A)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
forall (c : C) (d : D)
(f : morphism C c (G _0 d)%object),
Contr
  {g : morphism D (F _0 c)%object d &
  G _1 g
  o Build_NaturalTransformation 1 (G o F)
      (fun c0 : C => A (c0, (F _0 c0)%object) 1)
      (adjunction_unit__of__adjunction_hom__mate_of__commutes
         A) c = f}
    simpl in *.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
forall (c : C) (d : D)
(f : morphism C c (G _0 d)%object),
Contr
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f}
    intros c d f.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
Contr
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f}
    apply contr_inhabited_hprop.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
IsHProp
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f}
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
{g : morphism D (F _0 c)%object d &
G _1 g o A (c, (F _0 c)%object) 1 = f}
    -
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
IsHProp
  {g : morphism D (F _0 c)%object d &
  G _1 g o A (c, (F _0 c)%object) 1 = f} apply adjunction_unit__of__adjunction_hom_helper.
    -
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A: AdjunctionHom F G
c: C
d: D
f: morphism C c (G _0 d)%object
{g : morphism D (F _0 c)%object d &
G _1 g o A (c, (F _0 c)%object) 1 = f} exact ((A (c, d))^-1%morphism f;
             ((adjunction_naturality A _ _ _ _ _)
                @ (ap (A (c, d)) (right_identity _ _ _ _))
                @ (ap10 (@right_inverse _ _ _ (A (c, d)) _) f))%path).
  Defined.
End AdjunctionEquivalences.

Section isequiv.
  (** We want to be able to use this without needing [Funext].  So, first, we prove that the types of hom-sets are equivalent. *)
  Variables C D : PreCategory.
  Variable F : Functor C D.
  Variable G : Functor D C.

  Local Open Scope morphism_scope.

  Variable T : AdjunctionUnit F G.

  Lemma equiv_hom_set_adjunction
        (c : C) (d : D)
  : morphism C c (G d) <~> morphism D (F c) d.
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
morphism C c (G _0 d)%object <~>
morphism D (F _0 c)%object d
  Proof.
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
morphism C c (G _0 d)%object <~>
morphism D (F _0 c)%object d
    refine (equiv_adjointify
              (fun f => (@center _ (T.2 _ _ f)).1)
              (fun g => G _1 g o T.1 c)
              _ _);
    intro.
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism D (F _0 c)%object d
(center
   {g : morphism D (F _0 c)%object d &
   G _1 g o T.1 c = G _1 x o T.1 c}).1 = x
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism C c (G _0 d)%object
G
_1 (center
      {g : morphism D (F _0 c)%object d &
      G _1 g o T.1 c = x}).1 o T.1 c = x
    -
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism D (F _0 c)%object d
(center
   {g : morphism D (F _0 c)%object d &
   G _1 g o T.1 c = G _1 x o T.1 c}).1 = x match goal with
        | [ |- @pr1 ?A ?P ?x = ?y ]
          => change (x.1 = (exist P y idpath).1)
      end.
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism D (F _0 c)%object d
(center
   {g : morphism D (F _0 c)%object d &
   G _1 g o T.1 c = G _1 x o T.1 c}).1 = (x; 1%path).1
      apply (ap pr1).
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism D (F _0 c)%object d
center
  {g : morphism D (F _0 c)%object d &
  G _1 g o T.1 c = G _1 x o T.1 c} = (x; 1%path)
      apply contr.
    -
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
c: C
d: D
x: morphism C c (G _0 d)%object
G
_1 (center
      {g : morphism D (F _0 c)%object d &
      G _1 g o T.1 c = x}).1 o T.1 c = x match goal with
        | [ |- context[?x.1] ]
          => apply x.2
      end.
  Defined.
End isequiv.

(** ** hom-set adjunction from unit+ump adjunction *)
Section AdjunctionEquivalences'.
  Context `{Funext}.
  Variables C D : PreCategory.
  Variable F : Functor C D.
  Variable G : Functor D C.

  Local Open Scope morphism_scope.

  Lemma adjunction_hom__of__adjunction_unit__commutes
        (T : AdjunctionUnit F G)
        sc sd dc dd
        (mc : morphism C dc sc) (md : morphism D sd dd)
  : (fun x : morphism D (F sc) sd => G _1 (md o x o F _1 mc) o T .1 dc) =
    (fun x : morphism D (F sc) sd => G _1 md o (G _1 x o T .1 sc) o mc).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
sc: C
sd: D
dc: C
dd: D
mc: morphism C dc sc
md: morphism D sd dd
(fun x : morphism D (F _0 sc)%object sd =>
 G _1 (md o x o F _1 mc) o T.1 dc) =
(fun x : morphism D (F _0 sc)%object sd =>
 G _1 md o (G _1 x o T.1 sc) o mc)
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
sc: C
sd: D
dc: C
dd: D
mc: morphism C dc sc
md: morphism D sd dd
(fun x : morphism D (F _0 sc)%object sd =>
 G _1 (md o x o F _1 mc) o T.1 dc) =
(fun x : morphism D (F _0 sc)%object sd =>
 G _1 md o (G _1 x o T.1 sc) o mc)
    apply path_forall; intro.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
sc: C
sd: D
dc: C
dd: D
mc: morphism C dc sc
md: morphism D sd dd
x: morphism D (F _0 sc)%object sd
G _1 (md o x o F _1 mc) o T.1 dc =
G _1 md o (G _1 x o T.1 sc) o mc
    rewrite !composition_of, !associativity.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
sc: C
sd: D
dc: C
dd: D
mc: morphism C dc sc
md: morphism D sd dd
x: morphism D (F _0 sc)%object sd
G _1 md o (G _1 x o (G _1 (F _1 mc) o T.1 dc)) =
G _1 md o (G _1 x o (T.1 sc o mc))
    simpl rewrite (commutes T.1).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
sc: C
sd: D
dc: C
dd: D
mc: morphism C dc sc
md: morphism D sd dd
x: morphism D (F _0 sc)%object sd
G _1 md o (G _1 x o (G _1 (F _1 mc) o T.1 dc)) =
G _1 md o (G _1 x o (G _1 (F _1 mc) o T.1 dc))
    reflexivity.
  Qed.

  Definition adjunction_hom__of__adjunction_unit
             (T : AdjunctionUnit F G)
  : AdjunctionHom F G.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
AdjunctionHom F G
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
AdjunctionHom F G
    constructor.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
(HomFunctor.hom_functor D
 o Core.pair (Functor.Dual.opposite F) 1)%functor <~=~>
(HomFunctor.hom_functor C o Core.pair 1 G)%functor
    (eexists (Build_NaturalTransformation _ _ _ _)).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
IsIsomorphism
  (Build_NaturalTransformation
     (HomFunctor.hom_functor D
      o Core.pair (Functor.Dual.opposite F) 1)
     (HomFunctor.hom_functor C o Core.pair 1 G) ?CO
     ?COM)
    apply (@isisomorphism_natural_transformation _); simpl.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
forall x : C * D, IsIsomorphism (?CO x)
    exact (fun cd =>
             @isiso_isequiv
               _ _ _ _
               (equiv_isequiv
                  (equiv_hom_set_adjunction T (fst cd) (snd cd))^-1)).
    Unshelve.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
forall (s d : Prod.prod (Category.Dual.opposite C) D)
(m : morphism (Prod.prod (Category.Dual.opposite C) D)
       s d),
(fun cd : C * D =>
 equiv_fun
   (equiv_hom_set_adjunction T (fst cd) (snd cd))^-1)
  d
o (HomFunctor.hom_functor D
   o Core.pair (Functor.Dual.opposite F) 1) _1 m =
(HomFunctor.hom_functor C o Core.pair 1 G) _1 m
o (fun cd : C * D =>
   equiv_fun
     (equiv_hom_set_adjunction T (fst cd) (snd cd))^-1)
    s
    simpl.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
forall (s d : C * D)
(m : morphism C (fst d) (fst s) *
     morphism D (snd s) (snd d)),
(fun x : morphism D (F _0 (fst s))%object (snd s) =>
 G _1 (snd m o x o F _1 (fst m)) o T.1 (fst d)) =
(fun x : morphism D (F _0 (fst s))%object (snd s) =>
 G _1 (snd m) o (G _1 x o T.1 (fst s)) o fst m)
    intros.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
T: AdjunctionUnit F G
s, d: C * D
m: morphism C (fst d) (fst s) *
morphism D (snd s) (snd d)
(fun x : morphism D (F _0 (fst s))%object (snd s) =>
 G _1 (snd m o x o F _1 (fst m)) o T.1 (fst d)) =
(fun x : morphism D (F _0 (fst s))%object (snd s) =>
 G _1 (snd m) o (G _1 x o T.1 (fst s)) o fst m)
    exact (adjunction_hom__of__adjunction_unit__commutes T _ _ _ _ _ _).
  Defined.
End AdjunctionEquivalences'.

Definition AdjunctionUnitWithFunext `{Funext} C D F G := @AdjunctionUnit C D F G.
Definition AdjunctionCounitWithFunext `{Funext} C D F G := @AdjunctionCounit C D F G.
Definition AdjunctionUnitCounitWithFunext `{Funext} C D F G := @AdjunctionUnitCounit C D F G.
Identity Coercion AdjunctionUnit_Funext : AdjunctionUnitWithFunext >-> AdjunctionUnit.
Identity Coercion AdjunctionCounit_Funext : AdjunctionCounitWithFunext >-> AdjunctionCounit.
Identity Coercion AdjunctionUnitCounit_Funext : AdjunctionUnitCounitWithFunext >-> AdjunctionUnitCounit.

Definition adjunction_hom__of__adjunction_unit_Funext `{Funext} C D F G
           (A : AdjunctionUnitWithFunext _ _)
: AdjunctionHom _ _
  := @adjunction_hom__of__adjunction_unit _ C D F G A.
Definition AdjunctionHomOfAdjunctionCounit_Funext `{Funext} C D F G
           (A : AdjunctionCounitWithFunext _ _)
: AdjunctionHom _ _
  := @adjunction_hom__of__adjunction_unit _ C D F G (adjunction_unit_counit__of__adjunction_counit A).
Definition adjunction_hom__of__adjunction_unitCounit_Funext `{Funext} C D F G
           (A : AdjunctionUnitCounitWithFunext _ _)
: AdjunctionHom _ _
  := @adjunction_hom__of__adjunction_unit _ C D F G A.