Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import WildCat.NatTrans.
Require Import WildCat.Equiv.
Require Import WildCat.Prod.
Require Import WildCat.Opposite.
Require Import WildCat.Yoneda.
Require Import WildCat.FunctorCat.
Require Import WildCat.Universe.
Require Import Types.Prod.

Generalizable Variables C D F G.

(** ** Notions of adjunctions in wild categories. *)

(** We try to capture a wild notion of (oo,1)-adjunctions since these are the ones that commonly appear in practice. Special cases include the standard 1-categorical adjunction.

There are notions of 2-adjunction/biadjunction/higher adjunction but it is not clear if this generality is useful.

We will define an adjunction to be an equivalence (in Type) between corresponding hom-types. This is a more immediately useful definition than others we can consider.

We should also be able to define "F having a left adjoint" as the initial object of a slice category C / F. However this seems like too much work for now, and it is not immediately obvious how it ties back to the adjunction isomorphism.

In the future, it ought to be possible to generalize this definition to live inside a given bicategory, however due to current structural issues in the WildCat library, writing down a usable definition of bicategory requires a lot of effort.
*)

(** * Definition of adjunction *)

(** ** Definition of adjunction *)

Record Adjunction {C D : Type} (F : C -> D) (G : D -> C)
  `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} :=
{
  equiv_adjunction (x : C) (y : D) : (F x $-> y) <~> (x $-> G y) ;
  (** Naturality condition in both variable separately *)
  (** The left variable is a bit trickier to state since we have opposite categories involved. *)
  is1natural_equiv_adjunction_l (y : D)
    :: Is1Natural (A := C^op) (yon y o F)
        (** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
        (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
        (yon (G y)) (fun x => equiv_adjunction _ y) ;
  (** Naturality in the right variable *)
  is1natural_equiv_adjunction_r (x : C)
    :: Is1Natural (opyon (F x)) (opyon x o G) (equiv_adjunction x) ;
}.

Arguments equiv_adjunction {C D F G
  isgraph_C is2graph_C is01cat_C is1cat_C
  isgraph_D is2graph_D is01cat_D is1cat_D
  is0functor_F is0functor_G} adj x y : rename.
Arguments is1natural_equiv_adjunction_l {C D F G
  isgraph_C is2graph_C is01cat_C is1cat_C
  isgraph_D is2graph_D is01cat_D is1cat_D
  is0functor_F is0functor_G} adj y : rename.
Arguments is1natural_equiv_adjunction_r {C D F G
  isgraph_C is2graph_C is01cat_C is1cat_C
  isgraph_D is2graph_D is01cat_D is1cat_D
  is0functor_F is0functor_G} adj x : rename.

Notation "F ⊣ G" := (Adjunction F G).


(** TODO: move but where? *)
Lemma fun01_profunctor {A B C D : Type} (F : A -> B) (G : C -> D)
  `{Is0Functor A B F, Is0Functor C D G}
  : Fun01 (A^op * C) (B^op * D).
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Fun01 (A^op * C) (B^op * D)
Proof.
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Fun01 (A^op * C) (B^op * D)
  snapply Build_Fun01.
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
A^op * C -> B^op * D
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Is0Functor ?F
  1: exact (functor_prod F G).
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Is0Functor (functor_prod F G)
  rapply is0functor_prod_functor.
Defined.

Definition fun01_hom {C : Type} `{Is01Cat C}
  : Fun01 (C^op * C) Type
  := @Build_Fun01 _ _ _ _ _ is0functor_hom.

(** ** Natural equivalences coming from adjunctions. *)

(** There are various bits of data we would like to extract from adjunctions. *)
Section AdjunctionData.
  Context {C D : Type} {F : C -> D} {G : D -> C}
    `{Is1Cat C, Is1Cat D, !HasMorExt C, !HasMorExt D,
      !Is0Functor F, !Is0Functor G, !Is1Functor F, !Is1Functor G}
    (adj : Adjunction F G).

  Definition natequiv_adjunction_l (y : D)
    : NatEquiv (A := C^op) (yon y o F)
        (** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
        (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
        (yon (G y)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y: D
NatEquiv (yon y o F) (yon (G y))
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y: D
NatEquiv (yon y o F) (yon (G y))
    napply Build_NatEquiv.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y: D
Is1Natural (fun x : C => yon y (F x)) (yon (G y))
  (fun a : C^op => ?Goal a)
    apply (is1natural_equiv_adjunction_l adj).
  Defined.

  Definition natequiv_adjunction_r (x : C)
    : NatEquiv (opyon (F x)) (opyon x o G).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
NatEquiv (opyon (F x)) (opyon x o G)
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
NatEquiv (opyon (F x)) (opyon x o G)
    napply Build_NatEquiv.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
Is1Natural (opyon (F x))
  (fun x0 : D => opyon x (G x0))
  (fun a : D => ?Goal a)
    apply (is1natural_equiv_adjunction_r adj).
  Defined.

  (** We also have the natural equivalence in both arguments at the same time. *)
  (** In order to manage the typeclass instances, we have to bundle them up into Fun01. *)
  Definition natequiv_adjunction
    : NatEquiv (A := C^op * D)
        (fun01_compose fun01_hom (fun01_profunctor F idmap))
        (fun01_compose fun01_hom (fun01_profunctor idmap G)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatEquiv
  (fun01_compose fun01_hom (fun01_profunctor F idmap))
  (fun01_compose fun01_hom (fun01_profunctor idmap G))
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatEquiv
  (fun01_compose fun01_hom (fun01_profunctor F idmap))
  (fun01_compose fun01_hom (fun01_profunctor idmap G))
    snapply Build_NatEquiv.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall a : C^op * D,
fun01_compose fun01_hom (fun01_profunctor F idmap) a $<~>
fun01_compose fun01_hom (fun01_profunctor idmap G) a
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural
  (fun01_compose fun01_hom (fun01_profunctor F idmap))
  (fun01_compose fun01_hom (fun01_profunctor idmap G))
  (fun a : C^op * D => ?e a)
    1: intros [x y]; exact (equiv_adjunction adj x y).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural
  (fun01_compose fun01_hom (fun01_profunctor F idmap))
  (fun01_compose fun01_hom (fun01_profunctor idmap G))
  (fun a : C^op * D =>
   (fun a0 : C^op * D =>
    (fun (x : C^op) (y : D) =>
     equiv_adjunction adj x y) (fst a0) (snd a0)) a)
    snapply Build_Is1Natural.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall (a a' : C^op * D) (f : a $-> a'),
(fun a0 : C^op * D =>
 cate_fun
   ((fun a1 : C^op * D =>
     (fun (x : C^op) (y : D) =>
      equiv_adjunction adj x y) (fst a1) (snd a1)) a0))
  a' $o
fmap
  (fun01_compose fun01_hom (fun01_profunctor F idmap))
  f $==
fmap
  (fun01_compose fun01_hom (fun01_profunctor idmap G))
  f $o
(fun a0 : C^op * D =>
 cate_fun
   ((fun a1 : C^op * D =>
     (fun (x : C^op) (y : D) =>
      equiv_adjunction adj x y) (fst a1) (snd a1)) a0))
  a
    intros [a b] [a' b'] [f g] K.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
a: C^op
b: D
a': C^op
b': D
f: fst (a, b) $-> fst (a', b')
g: snd (a, b) $-> snd (a', b')
K: fun01_compose fun01_hom 
  (fun01_profunctor F idmap) 
  (a, b)
(equiv_adjunction adj a' b' $o
 fmap
   (fun01_compose fun01_hom (fun01_profunctor F idmap))
   (f, g)) K =
(fmap
   (fun01_compose fun01_hom (fun01_profunctor idmap G))
   (f, g) $o equiv_adjunction adj a b) K
    refine (_ @ ap (fun x : a $-> G b' => x $o f)
      (is1natural_equiv_adjunction_r adj a b b' g K)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
a: C^op
b: D
a': C^op
b': D
f: fst (a, b) $-> fst (a', b')
g: snd (a, b) $-> snd (a', b')
K: fun01_compose fun01_hom 
  (fun01_profunctor F idmap) 
  (a, b)
(equiv_adjunction adj a' b' $o
 fmap
   (fun01_compose fun01_hom (fun01_profunctor F idmap))
   (f, g)) K =
(equiv_adjunction adj a b' $o fmap (opyon (F a)) g) K $o
f
    exact (is1natural_equiv_adjunction_l adj _ _ _ f (g $o K)).
  Defined.

  (** The counit of an adjunction *)
  Definition adjunction_counit : NatTrans idmap (G o F).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatTrans idmap (G o F)
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatTrans idmap (G o F)
    snapply Build_NatTrans.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
idmap $=> (fun x : C => G (F x))
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural idmap (fun x : C => G (F x)) ?alpha
    {
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
idmap $=> (fun x : C => G (F x)) hnf.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall a : C, a $-> G (F a) intros x.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
x $-> G (F x)
      exact (equiv_adjunction adj x (F x) (Id _)). }
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural idmap (fun x : C => G (F x))
  ((fun x : C =>
    equiv_adjunction adj x (F x) (Id (F x)))
   :
   idmap $=> (fun x : C => G (F x)))
    snapply Build_Is1Natural.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall (a a' : C) (f : a $-> a'),
(fun x : C => equiv_adjunction adj x (F x) (Id (F x)))
  a' $o fmap idmap f $==
fmap (G o F) f $o
(fun x : C => equiv_adjunction adj x (F x) (Id (F x)))
  a
    intros x x' f.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
(fun x : C => equiv_adjunction adj x (F x) (Id (F x)))
  x' $o fmap idmap f $==
fmap (G o F) f $o
(fun x : C => equiv_adjunction adj x (F x) (Id (F x)))
  x
    apply GpdHom_path.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
equiv_adjunction adj x' (F x') (Id (F x')) $o
fmap idmap f =
fmap (G o F) f $o
equiv_adjunction adj x (F x) (Id (F x))
    refine (_^ @ _ @ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
?Goal0 =
equiv_adjunction adj x' (F x') (Id (F x')) $o
fmap idmap f
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
?Goal0 = ?Goal
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
?Goal =
fmap (G o F) f $o
equiv_adjunction adj x (F x) (Id (F x))
    1: exact (is1natural_equiv_adjunction_l adj _ _ _ f (Id _)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
((fun x : C^op =>
  equiv_fun (equiv_adjunction adj x (F x'))) x $o
 fmap (yon (F x') o F) f) (Id (F x')) = ?Goal
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
?Goal =
fmap (G o F) f $o
equiv_adjunction adj x (F x) (Id (F x))
    2: exact (is1natural_equiv_adjunction_r adj _ _ _ (fmap F f) (Id _)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
((fun x : C^op =>
  equiv_fun (equiv_adjunction adj x (F x'))) x $o
 fmap (yon (F x') o F) f) (Id (F x')) =
((fun y : D => equiv_fun (equiv_adjunction adj x y))
   (F x') $o fmap (opyon (F x)) (fmap F f)) (Id (F x))
    simpl.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
equiv_adjunction adj x (F x') (Id (F x') $o fmap F f) =
equiv_adjunction adj x (F x') (fmap F f $o Id (F x))
    apply equiv_ap'.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
Id (F x') $o fmap F f = fmap F f $o Id (F x)
    apply path_hom.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x, x': C
f: x $-> x'
Id (F x') $o fmap F f $== fmap F f $o Id (F x)
    apply Square.vrefl.
  Defined.

  (** The unit of an adjunction *)
  Definition adjunction_unit : NatTrans (F o G) idmap.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatTrans (F o G) idmap
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
NatTrans (F o G) idmap
    snapply Build_NatTrans.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
(fun x : D => F (G x)) $=> idmap
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural (fun x : D => F (G x)) idmap ?alpha
    {
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
(fun x : D => F (G x)) $=> idmap hnf.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall a : D, F (G a) $-> a intros y.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y: D
F (G y) $-> y
      exact ((equiv_adjunction adj (G y) y)^-1 (Id _)). }
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
Is1Natural (fun x : D => F (G x)) idmap
  ((fun y : D =>
    (equiv_adjunction adj (G y) y)^-1 (Id (G y)))
   :
   (fun x : D => F (G x)) $=> idmap)
    snapply Build_Is1Natural.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
forall (a a' : D) (f : a $-> a'),
(fun y : D =>
 (equiv_adjunction adj (G y) y)^-1 (Id (G y))) a' $o
fmap (F o G) f $==
fmap idmap f $o
(fun y : D =>
 (equiv_adjunction adj (G y) y)^-1 (Id (G y))) a
    intros y y' f.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
(fun y : D =>
 (equiv_adjunction adj (G y) y)^-1 (Id (G y))) y' $o
fmap (F o G) f $==
fmap idmap f $o
(fun y : D =>
 (equiv_adjunction adj (G y) y)^-1 (Id (G y))) y
    apply GpdHom_path.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
(equiv_adjunction adj (G y') y')^-1 (Id (G y')) $o
fmap (F o G) f =
fmap idmap f $o
(equiv_adjunction adj (G y) y)^-1 (Id (G y))
    refine (_^ @ _ @ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
?Goal0 =
(equiv_adjunction adj (G y') y')^-1 (Id (G y')) $o
fmap (F o G) f
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
?Goal0 = ?Goal
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
?Goal =
fmap idmap f $o
(equiv_adjunction adj (G y) y)^-1 (Id (G y))
    1: exact (is1natural_natequiv (natequiv_inverse
        (natequiv_adjunction_l _)) (G y') _ (fmap G f) _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
((fun a : C^op =>
  cate_fun
    (natequiv_inverse (natequiv_adjunction_l y') a))
   (G y) $o fmap (yon (G y')) (fmap G f)) (Id (G y')) =
?Goal
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
?Goal =
fmap idmap f $o
(equiv_adjunction adj (G y) y)^-1 (Id (G y))
    2: exact (is1natural_natequiv (natequiv_inverse
        (natequiv_adjunction_r _)) _ _ _ (Id _)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
((fun a : C^op =>
  cate_fun
    (natequiv_inverse (natequiv_adjunction_l y') a))
   (G y) $o fmap (yon (G y')) (fmap G f)) (Id (G y')) =
((fun a : D =>
  cate_fun
    (natequiv_inverse (natequiv_adjunction_r (G y)) a))
   y' $o fmap (opyon (G y) o G) (fmap idmap f))
  (Id (G y))
    simpl.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
(equiv_adjunction adj (G y) y')^-1
  (Id (G y') $o fmap G f) =
(equiv_adjunction adj (G y) y')^-1
  (fmap G f $o Id (G y))
    apply equiv_ap_inv'.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
Id (G y') $o fmap G f = fmap G f $o Id (G y)
    apply path_hom.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
y, y': D
f: y $-> y'
Id (G y') $o fmap G f $== fmap G f $o Id (G y)
    apply Square.vrefl.
  Defined.

  Lemma triangle_helper1 x y f
    : equiv_adjunction adj x y f = fmap G f $o adjunction_counit x.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
f: F x $-> y
equiv_adjunction adj x y f =
fmap G f $o adjunction_counit x
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
f: F x $-> y
equiv_adjunction adj x y f =
fmap G f $o adjunction_counit x
    refine (_ @ is1natural_equiv_adjunction_r adj _ _ _ _ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
f: F x $-> y
equiv_adjunction adj x y f =
(equiv_adjunction adj x y $o fmap (opyon (F x)) f)
  (Id (F x))
    by cbv; rewrite (cat_idr_strong f).
  Qed.

  Lemma triangle_helper2 x y g
    : (equiv_adjunction adj x y)^-1 g = adjunction_unit y $o fmap F g.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
g: x $-> G y
(equiv_adjunction adj x y)^-1 g =
adjunction_unit y $o fmap F g
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
g: x $-> G y
(equiv_adjunction adj x y)^-1 g =
adjunction_unit y $o fmap F g
    epose (n1 := is1natural_natequiv
      (natequiv_inverse (natequiv_adjunction_l _)) _ _ _ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
g: x $-> G y
n1:= is1natural_natequiv
  (natequiv_inverse (natequiv_adjunction_l ?y)) 
  ?a ?a' ?f ?x: ((fun a : C^op =>
  cate_fun
    (natequiv_inverse (natequiv_adjunction_l ?y)
       a)) ?a' $o fmap (yon (G ?y)) ?f) 
  ?x =
(fmap (yon ?y o F) ?f $o
 (fun a : C^op =>
  cate_fun
    (natequiv_inverse (natequiv_adjunction_l ?y)
       a)) ?a) ?x
(equiv_adjunction adj x y)^-1 g =
adjunction_unit y $o fmap F g
    clearbody n1; cbv in n1.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
g: x $-> G y
n1: (equiv_adjunction adj ?a' ?y)^-1 (?x $o ?f) =
(equiv_adjunction adj ?a ?y)^-1 ?x $o fmap F ?f
(equiv_adjunction adj x y)^-1 g =
adjunction_unit y $o fmap F g
    refine (_ @ n1).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
x: C
y: D
g: x $-> G y
n1: (equiv_adjunction adj x y)^-1 (Id (G y) $o g) =
(equiv_adjunction adj (G y) y)^-1 (Id (G y)) $o
fmap F g
(equiv_adjunction adj x y)^-1 g =
(equiv_adjunction adj x y)^-1 (Id (G y) $o g)
    by rewrite cat_idl_strong.
  Qed.

  Definition adjunction_triangle1
    : Transformation 
        (nattrans_comp
          (nattrans_prewhisker adjunction_unit F)
          (nattrans_postwhisker F adjunction_counit))
        (nattrans_id _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
nattrans_comp (nattrans_prewhisker adjunction_unit F)
  (nattrans_postwhisker F adjunction_counit) $=>
nattrans_id (fun x : C => F (idmap x))
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
nattrans_comp (nattrans_prewhisker adjunction_unit F)
  (nattrans_postwhisker F adjunction_counit) $=>
nattrans_id (fun x : C => F (idmap x))
    intros c.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
c: C
nattrans_comp (nattrans_prewhisker adjunction_unit F)
  (nattrans_postwhisker F adjunction_counit) c $->
nattrans_id (fun x : C => F x) c
    change (?x $-> _) with (x $-> Id (F c)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
c: C
nattrans_comp (nattrans_prewhisker adjunction_unit F)
  (nattrans_postwhisker F adjunction_counit) c $->
Id (F c)
    rewrite <- (eissect (equiv_adjunction adj _ _) (Id (F c))).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
c: C
nattrans_comp (nattrans_prewhisker adjunction_unit F)
  (nattrans_postwhisker F adjunction_counit) c $->
(equiv_adjunction adj c (F c))^-1
  (equiv_adjunction adj c (F c) (Id (F c)))
    cbv;rewrite <- (triangle_helper2 _ (F c) (adjunction_counit _)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
c: C
(equiv_adjunction adj c (F c))^-1
  (adjunction_counit c) $->
(equiv_adjunction adj c (F c))^-1
  (equiv_adjunction adj c (F c) (Id (F c)))
    exact (Id _).
  Qed.

  Definition adjunction_triangle2
    : Transformation
        (nattrans_comp
          (nattrans_postwhisker G adjunction_unit)
          (nattrans_prewhisker adjunction_counit G))
        (nattrans_id _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
nattrans_comp (nattrans_postwhisker G adjunction_unit)
  (nattrans_prewhisker adjunction_counit G) $=>
nattrans_id (fun x : D => idmap (G x))
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
nattrans_comp (nattrans_postwhisker G adjunction_unit)
  (nattrans_prewhisker adjunction_counit G) $=>
nattrans_id (fun x : D => idmap (G x))
    intros d.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
d: D
nattrans_comp (nattrans_postwhisker G adjunction_unit)
  (nattrans_prewhisker adjunction_counit G) d $->
nattrans_id (fun x : D => G x) d
    change (?x $-> _) with (x $-> Id (G d)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
d: D
nattrans_comp (nattrans_postwhisker G adjunction_unit)
  (nattrans_prewhisker adjunction_counit G) d $->
Id (G d)
    rewrite <- (eisretr (equiv_adjunction adj _ _) (Id (G d))).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
d: D
nattrans_comp (nattrans_postwhisker G adjunction_unit)
  (nattrans_prewhisker adjunction_counit G) d $->
equiv_adjunction adj (G d) d
  ((equiv_adjunction adj (G d) d)^-1 (Id (G d)))
    cbv;rewrite <- (triangle_helper1 (G d) _ (adjunction_unit _)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
adj: F ⊣ G
d: D
equiv_adjunction adj (G d) d (adjunction_unit d) $->
equiv_adjunction adj (G d) d
  ((equiv_adjunction adj (G d) d)^-1 (Id (G d)))
    exact (Id _).
  Qed.

End AdjunctionData.

(** ** Building adjunctions *)

(** There are various ways to build an adjunction. *)

(** A natural equivalence between functors [D -> Type] which is also natural in the left. *)
Definition Build_Adjunction_natequiv_nat_left
  {C D : Type} (F : C -> D) (G : D -> C)
  `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} 
  (e : forall x, NatEquiv (opyon (F x)) (opyon x o G))
  (is1nat_e : forall y, Is1Natural (A := C^op) (yon y o F)
      (** We have to explicitly give a witness to the functoriality of [yon y o F]. *)
      (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
      (yon (G y)) (fun x => e _ y))
  : Adjunction F G.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
F ⊣ G
Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
F ⊣ G
  snapply Build_Adjunction.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall (x : C) (y : D), (F x $-> y) <~> (x $-> G y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => ?equiv_adjunction x y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => ?equiv_adjunction x y)
  1: exact (fun x => e x).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall y : D,
Is1Natural (yon y o F) (yon (G y))
  (fun x : C^op =>
   (fun x0 : C => cat_equiv_natequiv (e x0)) x y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G)
  (fun y : D =>
   (fun x0 : C => cat_equiv_natequiv (e x0)) x y)
  1: exact is1nat_e.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall x : C, NatEquiv (opyon (F x)) (opyon x o G)
is1nat_e: forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => e x y)
forall x : C,
Is1Natural (opyon (F x)) (opyon x o G)
  (fun y : D =>
   (fun x0 : C => cat_equiv_natequiv (e x0)) x y)
  intros x; exact (is1natural_natequiv (e x)).
Defined.

(** A natural equivalence between functors [C^op -> Type] which is also natural in the left. *)
Definition Build_Adjunction_natequiv_nat_right
  {C D : Type} (F : C -> D) (G : D -> C)
  `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G} 
  (e : forall y, NatEquiv (A := C^op) (yon y o F) (yon (G y))
    (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _))
  (is1nat_e : forall x, Is1Natural (opyon (F x)) (opyon x o G) (fun y => e y x))
  : Adjunction F G.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
F ⊣ G
Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
F ⊣ G
  snapply Build_Adjunction.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall (x : C) (y : D), (F x $-> y) <~> (x $-> G y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => ?equiv_adjunction x y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => ?equiv_adjunction x y)
  1: exact (fun x y => e y x).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall y : D,
Is1Natural (yon y o F) (yon (G y))
  (fun x : C^op =>
   (fun (x0 : C) (y0 : D) => e y0 x0) x y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G)
  (fun y : D => (fun (x0 : C) (y0 : D) => e y0 x0) x y)
  1: intros y; exact (is1natural_natequiv (e y)).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
e: forall y : D, NatEquiv (yon y o F) (yon (G y))
is1nat_e: forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => e y x)
forall x : C,
Is1Natural (opyon (F x)) (opyon x o G)
  (fun y : D => (fun (x0 : C) (y0 : D) => e y0 x0) x y)
  exact is1nat_e.
Defined.

(** TODO: A natural equivalence between functors [C^op * D -> Type] *)

Section UnitCounitAdjunction.

  (** From the data of an adjunction: unit, counit, left triangle, right triangle *)
  Context {C D : Type} (F : C -> D) (G : D -> C)
  `{Is1Cat C, Is1Cat D, !Is0Functor F, !Is0Functor G,
    !Is1Functor F, !Is1Functor G}
  `{!HasMorExt C, !HasMorExt D}
  (ε : NatTrans (F o G) idmap)
  (η : NatTrans idmap (G o F))
  (t1 : Transformation 
    (nattrans_comp (nattrans_prewhisker ε F) (nattrans_postwhisker F η))
    (nattrans_id _))
  (t2 : Transformation
    (nattrans_comp (nattrans_postwhisker G ε) (nattrans_prewhisker η G))
    (nattrans_id _)).

  (** We can construct an equivalence between homs *)
  Local Definition γ a b : (F a $-> b) $<~> (a $-> G b).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(F a $-> b) $<~> (a $-> G b)
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(F a $-> b) $<~> (a $-> G b)
    srapply equiv_adjointify.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(F a $-> b) -> a $-> G b
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(a $-> G b) -> F a $-> b
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
?f o ?g == idmap
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
?g o ?f == idmap
    1: exact (fun x => fmap G x $o (η : _ $=> _) a).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(a $-> G b) -> F a $-> b
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(fun x : F a $-> b =>
 fmap G x $o
 (η : idmap $=> (fun x0 : C => G (F x0))) a) o 
?g == idmap
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
?g
o (fun x : F a $-> b =>
   fmap G x $o
   (η : idmap $=> (fun x0 : C => G (F x0))) a) ==
idmap
    1: exact (fun x => (ε : _ $=> _) b $o fmap F x).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(fun x : F a $-> b =>
 fmap G x $o
 (η : idmap $=> (fun x0 : C => G (F x0))) a)
o (fun x : a $-> G b =>
   (ε : (fun x0 : D => F (G x0)) $=> idmap) b $o
   fmap F x) == idmap
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(fun x : a $-> G b =>
 (ε : (fun x0 : D => F (G x0)) $=> idmap) b $o
 fmap F x)
o (fun x : F a $-> b =>
   fmap G x $o
   (η : idmap $=> (fun x0 : C => G (F x0))) a) ==
idmap
    +
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(fun x : F a $-> b =>
 fmap G x $o
 (η : idmap $=> (fun x0 : C => G (F x0))) a)
o (fun x : a $-> G b =>
   (ε : (fun x0 : D => F (G x0)) $=> idmap) b $o
   fmap F x) == idmap intros f.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b $o fmap F f) $o η a = f
      apply path_hom; simpl.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b $o fmap F f) $o η a $== f
      refine ((fmap_comp G _ _ $@R _) $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b) $o fmap G (fmap F f) $o η a $== f
      refine (cat_assoc _ _ _ $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b) $o (fmap G (fmap F f) $o η a) $== f
      refine ((_ $@L (isnat η f)^$) $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b) $o (η (G b) $o fmap idmap f) $== f
      refine (cat_assoc_opp _ _ _ $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b) $o η (G b) $o fmap idmap f $== f
      refine (_ $@R _ $@ cat_idl _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
f: a $-> G b
fmap G (ε b) $o η (G b) $== Id (G b)
      exact (t2 b).
    +
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
(fun x : a $-> G b =>
 (ε : (fun x0 : D => F (G x0)) $=> idmap) b $o
 fmap F x)
o (fun x : F a $-> b =>
   fmap G x $o
   (η : idmap $=> (fun x0 : C => G (F x0))) a) ==
idmap intros g.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
ε b $o fmap F (fmap G g $o η a) = g
      apply path_hom; simpl.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
ε b $o fmap F (fmap G g $o η a) $== g
      refine ((_ $@L fmap_comp F _ _) $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
ε b $o (fmap F (fmap G g) $o fmap F (η a)) $== g
      refine (cat_assoc_opp _ _ _ $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
ε b $o fmap F (fmap G g) $o fmap F (η a) $== g
      refine (((isnat ε g) $@R _) $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
fmap idmap g $o ε (F a) $o fmap F (η a) $== g
      refine (cat_assoc _ _ _ $@ _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
fmap idmap g $o (ε (F a) $o fmap F (η a)) $== g
      refine (_ $@L _ $@ cat_idr _).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
a: C
b: D
g: F a $-> b
ε (F a) $o fmap F (η a) $== Id (F a)
      exact (t1 a).
  Defined.

  (** Which is natural in the left *)
  Lemma is1natural_γ_l (y : D)
    : Is1Natural (yon y o F) (yon (G y))
      (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _)
      (is0functor_G := is0functor_yon (G y))
      (fun x : C^op => γ x y).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Natural (yon y o F) (yon (G y))
  (fun x : C^op => γ x y)
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Natural (yon y o F) (yon (G y))
  (fun x : C^op => γ x y)
    napply (is1natural_natequiv (natequiv_inverse
      (Build_NatEquiv (yon (G y)) (yon y o F) (fun x => (γ x y)^-1$) _))).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Natural (yon (G y)) (fun x : C => yon y (F x))
  (fun a : C^op => (γ a y)^-1$)
    napply is1natural_yoneda.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Functor (fun x : C => yon y (F x))
    napply is1functor_compose.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Functor F
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Functor (yon y)
    1: napply is1functor_op; exact _.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
Is1Functor (yon y)
    napply is1functor_opyon.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
y: D
HasMorExt D
    exact hasmorext_op.
  Defined.

  (** And natural in the right. *)
  Lemma is1natural_γ_r x
    : Is1Natural (opyon (F x)) (fun x0 : D => opyon x (G x0)) (γ x).
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
x: C
Is1Natural (opyon (F x))
  (fun x0 : D => opyon x (G x0)) (fun b : D => γ x b)
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
x: C
Is1Natural (opyon (F x))
  (fun x0 : D => opyon x (G x0)) (fun b : D => γ x b)
    napply is1natural_opyoneda.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
x: C
Is1Functor (fun x0 : D => opyon x (G x0))
    exact _.
  Defined.

  (** Together this constructs an adjunction. *)
  Definition Build_Adjunction_unit_counit : Adjunction F G.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
F ⊣ G
  Proof.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
F ⊣ G
    snapply Build_Adjunction.
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall (x : C) (y : D), (F x $-> y) <~> (x $-> G y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall y : D,
Is1Natural (yon y o F) 
  (yon (G y)) (fun x : C^op => ?equiv_adjunction x y)
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall x : C,
Is1Natural (opyon (F x)) 
  (opyon x o G) (fun y : D => ?equiv_adjunction x y)
    -
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall (x : C) (y : D), (F x $-> y) <~> (x $-> G y) exact γ.
    -
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall y : D,
Is1Natural (yon y o F) (yon (G y))
  (fun x : C^op => γ x y) exact is1natural_γ_l.
    -
C, D: Type
F: C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is1Functor0: Is1Functor F
Is1Functor1: Is1Functor G
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
ε: NatTrans (F o G) idmap
η: NatTrans idmap (G o F)
t1: nattrans_comp (nattrans_prewhisker ε F)
  (nattrans_postwhisker F η) $=>
nattrans_id (fun x : C => F (idmap x))
t2: nattrans_comp (nattrans_postwhisker G ε)
  (nattrans_prewhisker η G) $=>
nattrans_id (fun x : D => idmap (G x))
forall x : C,
Is1Natural (opyon (F x)) (opyon x o G)
  (fun y : D => γ x y) exact is1natural_γ_r.
  Defined.

End UnitCounitAdjunction.

(** * Properties of adjunctions *)

(** ** Postcomposition adjunction *)
(** There are at least two easy proofs of the following on paper:
 1. Using ends: Hom(F*x,y) ≃ ∫_c Hom(Fxc,yc) ≃ ∫_c Hom(xc,Gyc) ≃ Hom(x,G*y)
 2. 2-cat theory: postcomp (-)* is a 2-functor so preserves adjunctions.
*)

Lemma adjunction_postcomp (C D J : Type)
  `{HasEquivs C, HasEquivs D, Is01Cat J} (F : Fun11 C D) (G : Fun11 D C)
  `{!HasMorExt C, !HasMorExt D, !HasMorExt (Fun01 J C), !HasMorExt (Fun01 J D)}
  : F ⊣ G -> fun11_fun01_postcomp (A:=J) F ⊣ fun11_fun01_postcomp (A:=J) G.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
F ⊣ G ->
fun11_fun01_postcomp F ⊣ fun11_fun01_postcomp G
Proof.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
F ⊣ G ->
fun11_fun01_postcomp F ⊣ fun11_fun01_postcomp G
  intros adj.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
fun11_fun01_postcomp F ⊣ fun11_fun01_postcomp G
  srapply Build_Adjunction_unit_counit.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
NatTrans
  (fun11_fun01_postcomp F o fun11_fun01_postcomp G)
  idmap
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
NatTrans idmap
  (fun11_fun01_postcomp G o fun11_fun01_postcomp F)
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
nattrans_comp
  (nattrans_prewhisker ?ε (fun11_fun01_postcomp F))
  (nattrans_postwhisker (fun11_fun01_postcomp F) ?η) $=>
nattrans_id
  (fun x : Fun01 J C =>
   fun11_fun01_postcomp F (idmap x))
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
nattrans_comp
  (nattrans_postwhisker (fun11_fun01_postcomp G) ?ε)
  (nattrans_prewhisker ?η (fun11_fun01_postcomp G)) $=>
nattrans_id
  (fun x : Fun01 J D =>
   idmap (fun11_fun01_postcomp G x))
  -
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
NatTrans
  (fun11_fun01_postcomp F o fun11_fun01_postcomp G)
  idmap snapply Build_NatTrans.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
(fun x : Fun01 J D =>
 fun11_fun01_postcomp F (fun11_fun01_postcomp G x)) $=>
idmap
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
Is1Natural
  (fun x : Fun01 J D =>
   fun11_fun01_postcomp F (fun11_fun01_postcomp G x))
  idmap ?alpha
    +
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
(fun x : Fun01 J D =>
 fun11_fun01_postcomp F (fun11_fun01_postcomp G x)) $=>
idmap intros K.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K: Fun01 J D
fun11_fun01_postcomp F (fun11_fun01_postcomp G K) $->
K
      exact (nattrans_prewhisker (adjunction_unit adj) K).
    +
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
Is1Natural
  (fun x : Fun01 J D =>
   fun11_fun01_postcomp F (fun11_fun01_postcomp G x))
  idmap
  ((fun K : Fun01 J D =>
    nattrans_prewhisker (adjunction_unit adj) K)
   :
   (fun x : Fun01 J D =>
    fun11_fun01_postcomp F (fun11_fun01_postcomp G x)) $=>
   idmap) snapply Build_Is1Natural.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
forall (a a' : Fun01 J D) 
(f : a $-> a'),
(fun K : Fun01 J D =>
 nattrans_prewhisker (adjunction_unit adj) K) a' $o
fmap (fun11_fun01_postcomp F o fun11_fun01_postcomp G)
  f $==
fmap idmap f $o
(fun K : Fun01 J D =>
 nattrans_prewhisker (adjunction_unit adj) K) a
      intros K K' θ j.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
(nattrans_prewhisker (adjunction_unit adj) K' $o
 fmap
   (fun11_fun01_postcomp F o fun11_fun01_postcomp G) θ)
  j $==
(fmap idmap θ $o
 nattrans_prewhisker (adjunction_unit adj) K) j
      apply GpdHom_path.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
(nattrans_prewhisker (adjunction_unit adj) K' $o
 fmap
   (fun11_fun01_postcomp F o fun11_fun01_postcomp G) θ)
  j =
(fmap idmap θ $o
 nattrans_prewhisker (adjunction_unit adj) K) j
      refine (_ @ is1natural_natequiv (natequiv_inverse
        (natequiv_adjunction_r adj _)) _ _ _ _).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
trans_comp
  (nattrans_prewhisker (adjunction_unit adj) K')
  (fmap
     (fun11_fun01_postcomp F o fun11_fun01_postcomp G)
     θ) j =
(natequiv_inverse
   (natequiv_adjunction_r adj
      (fun11_fun01_postcomp G K j)) 
   (K' j) $o
 fmap (opyon (fun11_fun01_postcomp G K j) o G)
   (fmap idmap θ j)) (Id (G (K j)))
      refine ((is1natural_natequiv (natequiv_inverse
        (natequiv_adjunction_l adj _)) _ _ _ _)^ @ _).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
(natequiv_inverse (natequiv_adjunction_l adj (K' j))
   (fun11_fun01_postcomp G K j) $o
 fmap (yon (G (K' j))) (fmap (fun01_postcomp G) θ j))
  (Id (G (K' j))) =
(natequiv_inverse
   (natequiv_adjunction_r adj
      (fun11_fun01_postcomp G K j)) 
   (K' j) $o
 fmap (opyon (fun11_fun01_postcomp G K j) o G)
   (fmap idmap θ j)) (Id (G (K j)))
      cbn; rapply ap.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
Id (G (K' j)) $o trans_postwhisker G θ j =
fmap G (θ j) $o Id (G (K j))
      refine(cat_idl_strong _ @ _^).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J D
θ: K $-> K'
j: J
fmap G (θ j) $o Id (G (K j)) = trans_postwhisker G θ j
      apply cat_idr_strong.
  -
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
NatTrans idmap
  (fun11_fun01_postcomp G o fun11_fun01_postcomp F) snapply Build_NatTrans.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
idmap $=>
(fun x : Fun01 J C =>
 fun11_fun01_postcomp G (fun11_fun01_postcomp F x))
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
Is1Natural idmap
  (fun x : Fun01 J C =>
   fun11_fun01_postcomp G (fun11_fun01_postcomp F x))
  ?alpha
    +
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
idmap $=>
(fun x : Fun01 J C =>
 fun11_fun01_postcomp G (fun11_fun01_postcomp F x)) intros K.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K: Fun01 J C
K $->
fun11_fun01_postcomp G (fun11_fun01_postcomp F K)
      exact (nattrans_prewhisker (adjunction_counit adj) K).
    +
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
Is1Natural idmap
  (fun x : Fun01 J C =>
   fun11_fun01_postcomp G (fun11_fun01_postcomp F x))
  ((fun K : Fun01 J C =>
    nattrans_prewhisker (adjunction_counit adj) K)
   :
   idmap $=>
   (fun x : Fun01 J C =>
    fun11_fun01_postcomp G (fun11_fun01_postcomp F x))) snapply Build_Is1Natural.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
forall (a a' : Fun01 J C) 
(f : a $-> a'),
(fun K : Fun01 J C =>
 nattrans_prewhisker (adjunction_counit adj) K) a' $o
fmap idmap f $==
fmap (fun11_fun01_postcomp G o fun11_fun01_postcomp F)
  f $o
(fun K : Fun01 J C =>
 nattrans_prewhisker (adjunction_counit adj) K) a
      intros K K' θ j.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
(nattrans_prewhisker (adjunction_counit adj) K' $o
 fmap idmap θ) j $==
(fmap
   (fun11_fun01_postcomp G o fun11_fun01_postcomp F) θ $o
 nattrans_prewhisker (adjunction_counit adj) K) j
      apply GpdHom_path.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
(nattrans_prewhisker (adjunction_counit adj) K' $o
 fmap idmap θ) j =
(fmap
   (fun11_fun01_postcomp G o fun11_fun01_postcomp F) θ $o
 nattrans_prewhisker (adjunction_counit adj) K) j
      refine (_ @ is1natural_natequiv
        (natequiv_adjunction_r adj _) _ _ _ _).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
trans_comp
  (nattrans_prewhisker (adjunction_counit adj) K')
  (fmap idmap θ) j =
(natequiv_adjunction_r adj 
   (K j) (fun11_fun01_postcomp F K' j) $o
 fmap (opyon (F (K j))) (fmap (fun01_postcomp F) θ j))
  (Id (F (K j)))
      refine ((is1natural_natequiv
        (natequiv_adjunction_l adj _) _ _ _ _)^ @ _).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
(natequiv_adjunction_l adj
   (fun11_fun01_postcomp F K' j) 
   (K j) $o
 fmap (yon (fun11_fun01_postcomp F K' j) o F)
   (fmap idmap θ j)) (Id (F (K' j))) =
(natequiv_adjunction_r adj 
   (K j) (fun11_fun01_postcomp F K' j) $o
 fmap (opyon (F (K j))) (fmap (fun01_postcomp F) θ j))
  (Id (F (K j)))
      cbn; rapply ap.
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
Id (F (K' j)) $o fmap F (θ j) =
trans_postwhisker F θ j $o Id (F (K j))
      refine(cat_idl_strong _ @ _^).
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
K, K': Fun01 J C
θ: K $-> K'
j: J
trans_postwhisker F θ j $o Id (F (K j)) = fmap F (θ j)
      apply cat_idr_strong.
  -
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
nattrans_comp
  (nattrans_prewhisker
     {|
       trans_nattrans :=
         (fun K : Fun01 J D =>
          nattrans_prewhisker (adjunction_unit adj) K)
         :
         (fun x : Fun01 J D =>
          fun11_fun01_postcomp F
            (fun11_fun01_postcomp G x)) $=> idmap;
       is1natural_nattrans :=
         Build_Is1Natural
           (fun K : Fun01 J D =>
            nattrans_prewhisker 
              (adjunction_unit adj) K)
           (fun (K K' : Fun01 J D) (θ : K $-> K') =>
            (fun j : J =>
             GpdHom_path
               (((is1natural_natequiv
                    (natequiv_inverse
                      (natequiv_adjunction_l adj
                      (K' j)))
                    (fun11_fun01_postcomp G K' j)
                    (fun11_fun01_postcomp G K j)
                    (fmap (fun01_postcomp G) θ j)
                    (Id (G (K' j))))^ @
                 (ap
                    (equiv_adjunction adj 
                      (G (K j)) 
                      (K' j))^-1
                    (cat_idl_strong
                      (trans_postwhisker G θ j) @
                     (cat_idr_strong
                      (trans_postwhisker G θ j))^)
                  :
                  (natequiv_inverse
                     (natequiv_adjunction_l adj ...)
                     (fun11_fun01_postcomp G K j) $o
                   fmap (yon ...) (fmap ... θ j))
                    (Id (G (...))) =
                  (natequiv_inverse
                     (natequiv_adjunction_r adj ...)
                     (K' j) $o
                   fmap (... o G) (fmap idmap θ j))
                    (Id (G (...))))) @
                is1natural_natequiv
                  (natequiv_inverse
                     (natequiv_adjunction_r adj
                      (fun11_fun01_postcomp G K j)))
                  (K j) 
                  (K' j) 
                  (fmap idmap θ j) 
                  (Id (G (K j)))))
            :
            (fun K0 : Fun01 J D =>
             nattrans_prewhisker 
               (adjunction_unit adj) K0) K' $o
            fmap
              (fun11_fun01_postcomp F
               o fun11_fun01_postcomp G) θ $==
            fmap idmap θ $o
            (fun K0 : Fun01 J D =>
             nattrans_prewhisker 
               (adjunction_unit adj) K0) K)
     |} (fun11_fun01_postcomp F))
  (nattrans_postwhisker 
     (fun11_fun01_postcomp F)
     {|
       trans_nattrans :=
         (fun K : Fun01 J C =>
          nattrans_prewhisker 
            (adjunction_counit adj) K)
         :
         idmap $=>
         (fun x : Fun01 J C =>
          fun11_fun01_postcomp G
            (fun11_fun01_postcomp F x));
       is1natural_nattrans :=
         Build_Is1Natural
           (fun K : Fun01 J C =>
            nattrans_prewhisker
              (adjunction_counit adj) K)
           (fun (K K' : Fun01 J C) (θ : K $-> K') =>
            (fun j : J =>
             GpdHom_path
               (((is1natural_natequiv
                    (natequiv_adjunction_l adj
                      (fun11_fun01_postcomp F K' j))
                    (K' j) 
                    (K j) 
                    (fmap idmap θ j) 
                    (Id (F (K' j))))^ @
                 (ap
                    (equiv_adjunction adj 
                      (K j) 
                      (F (K' j)))
                    (cat_idl_strong (fmap F (...)) @
                     (cat_idr_strong (fmap F ...))^)
                  :
                  (natequiv_adjunction_l adj
                     (fun11_fun01_postcomp F K' j)
                     (K j) $o
                   fmap (... o F) (fmap idmap θ j))
                    (Id (F (...))) =
                  (natequiv_adjunction_r adj 
                     (K j)
                     (fun11_fun01_postcomp F K' j) $o
                   fmap (opyon ...) (fmap ... θ j))
                    (Id (F (...))))) @
                is1natural_natequiv
                  (natequiv_adjunction_r adj (K j))
                  (fun11_fun01_postcomp F K j)
                  (fun11_fun01_postcomp F K' j)
                  (fmap (fun01_postcomp F) θ j)
                  (Id (F (K j)))))
            :
            (fun K0 : Fun01 J C =>
             nattrans_prewhisker
               (adjunction_counit adj) K0) K' $o
            fmap idmap θ $==
            fmap
              (fun11_fun01_postcomp G
               o fun11_fun01_postcomp F) θ $o
            (fun K0 : Fun01 J C =>
             nattrans_prewhisker
               (adjunction_counit adj) K0) K)
     |}) $=>
nattrans_id
  (fun x : Fun01 J C =>
   fun11_fun01_postcomp F (idmap x)) exact (trans_prewhisker (adjunction_triangle1 adj)).
  -
C, D, J: Type
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
H2: HasEquivs D
H3: IsGraph J
H4: Is01Cat J
F: Fun11 C D
G: Fun11 D C
HasMorExt0: HasMorExt C
HasMorExt1: HasMorExt D
HasMorExt2: HasMorExt (Fun01 J C)
HasMorExt3: HasMorExt (Fun01 J D)
adj: F ⊣ G
nattrans_comp
  (nattrans_postwhisker 
     (fun11_fun01_postcomp G)
     {|
       trans_nattrans :=
         (fun K : Fun01 J D =>
          nattrans_prewhisker (adjunction_unit adj) K)
         :
         (fun x : Fun01 J D =>
          fun11_fun01_postcomp F
            (fun11_fun01_postcomp G x)) $=> idmap;
       is1natural_nattrans :=
         Build_Is1Natural
           (fun K : Fun01 J D =>
            nattrans_prewhisker 
              (adjunction_unit adj) K)
           (fun (K K' : Fun01 J D) (θ : K $-> K') =>
            (fun j : J =>
             GpdHom_path
               (((is1natural_natequiv
                    (natequiv_inverse
                      (natequiv_adjunction_l adj
                      (K' j)))
                    (fun11_fun01_postcomp G K' j)
                    (fun11_fun01_postcomp G K j)
                    (fmap (fun01_postcomp G) θ j)
                    (Id (G (K' j))))^ @
                 (ap
                    (equiv_adjunction adj 
                      (G (K j)) 
                      (K' j))^-1
                    (cat_idl_strong
                      (trans_postwhisker G θ j) @
                     (cat_idr_strong
                      (trans_postwhisker G θ j))^)
                  :
                  (natequiv_inverse
                     (natequiv_adjunction_l adj ...)
                     (fun11_fun01_postcomp G K j) $o
                   fmap (yon ...) (fmap ... θ j))
                    (Id (G (...))) =
                  (natequiv_inverse
                     (natequiv_adjunction_r adj ...)
                     (K' j) $o
                   fmap (... o G) (fmap idmap θ j))
                    (Id (G (...))))) @
                is1natural_natequiv
                  (natequiv_inverse
                     (natequiv_adjunction_r adj
                      (fun11_fun01_postcomp G K j)))
                  (K j) 
                  (K' j) 
                  (fmap idmap θ j) 
                  (Id (G (K j)))))
            :
            (fun K0 : Fun01 J D =>
             nattrans_prewhisker 
               (adjunction_unit adj) K0) K' $o
            fmap
              (fun11_fun01_postcomp F
               o fun11_fun01_postcomp G) θ $==
            fmap idmap θ $o
            (fun K0 : Fun01 J D =>
             nattrans_prewhisker 
               (adjunction_unit adj) K0) K)
     |})
  (nattrans_prewhisker
     {|
       trans_nattrans :=
         (fun K : Fun01 J C =>
          nattrans_prewhisker 
            (adjunction_counit adj) K)
         :
         idmap $=>
         (fun x : Fun01 J C =>
          fun11_fun01_postcomp G
            (fun11_fun01_postcomp F x));
       is1natural_nattrans :=
         Build_Is1Natural
           (fun K : Fun01 J C =>
            nattrans_prewhisker
              (adjunction_counit adj) K)
           (fun (K K' : Fun01 J C) (θ : K $-> K') =>
            (fun j : J =>
             GpdHom_path
               (((is1natural_natequiv
                    (natequiv_adjunction_l adj
                      (fun11_fun01_postcomp F K' j))
                    (K' j) 
                    (K j) 
                    (fmap idmap θ j) 
                    (Id (F (K' j))))^ @
                 (ap
                    (equiv_adjunction adj 
                      (K j) 
                      (F (K' j)))
                    (cat_idl_strong (fmap F (...)) @
                     (cat_idr_strong (fmap F ...))^)
                  :
                  (natequiv_adjunction_l adj
                     (fun11_fun01_postcomp F K' j)
                     (K j) $o
                   fmap (... o F) (fmap idmap θ j))
                    (Id (F (...))) =
                  (natequiv_adjunction_r adj 
                     (K j)
                     (fun11_fun01_postcomp F K' j) $o
                   fmap (opyon ...) (fmap ... θ j))
                    (Id (F (...))))) @
                is1natural_natequiv
                  (natequiv_adjunction_r adj (K j))
                  (fun11_fun01_postcomp F K j)
                  (fun11_fun01_postcomp F K' j)
                  (fmap (fun01_postcomp F) θ j)
                  (Id (F (K j)))))
            :
            (fun K0 : Fun01 J C =>
             nattrans_prewhisker
               (adjunction_counit adj) K0) K' $o
            fmap idmap θ $==
            fmap
              (fun11_fun01_postcomp G
               o fun11_fun01_postcomp F) θ $o
            (fun K0 : Fun01 J C =>
             nattrans_prewhisker
               (adjunction_counit adj) K0) K)
     |} (fun11_fun01_postcomp G)) $=>
nattrans_id
  (fun x : Fun01 J D =>
   idmap (fun11_fun01_postcomp G x)) exact (trans_prewhisker (adjunction_triangle2 adj)).
Defined.

(** We can compose adjunctions. Notice how the middle category must have equivalences. *)
Lemma adjunction_compose (A B C : Type)
  (F : A -> B) (G : B -> A) (F' : B -> C) (G' : C -> B)
  `{Is1Cat A, HasEquivs B, Is1Cat C}
  `{!Is0Functor F, !Is0Functor G, !Is0Functor F', !Is0Functor G'}
  : F ⊣ G -> F' ⊣ G' -> F' o F ⊣ G o G'.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
F ⊣ G -> F' ⊣ G' -> F' o F ⊣ G o G'
Proof.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
F ⊣ G -> F' ⊣ G' -> F' o F ⊣ G o G'
  intros adj1 adj2.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
F' o F ⊣ G o G'
  snapply Build_Adjunction_natequiv_nat_right.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
forall y : C,
NatEquiv (yon y o (fun x : A => F' (F x)))
  (yon ((fun x : C => G (G' x)) y))
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
forall x : A,
Is1Natural (opyon ((fun x0 : A => F' (F x0)) x))
  (opyon x o (fun x0 : C => G (G' x0)))
  (fun y : C => ?e y x)
  {
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
forall y : C,
NatEquiv (yon y o (fun x : A => F' (F x)))
  (yon ((fun x : C => G (G' x)) y)) intros y.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
y: C
NatEquiv (yon y o (fun x : A => F' (F x)))
  (yon ((fun x : C => G (G' x)) y))
    nrefine (natequiv_compose (natequiv_adjunction_l adj1 _) _).
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
y: C
NatEquiv (fun x : A => yon y (F' (F x)))
  (fun x : A => yon (G' y) (F x))
    exact (natequiv_prewhisker (A:=A^op) (B:=B^op)
      (natequiv_adjunction_l adj2 y) F). }
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
forall x : A,
Is1Natural (opyon ((fun x0 : A => F' (F x0)) x))
  (opyon x o (fun x0 : C => G (G' x0)))
  (fun y : C =>
   (fun y0 : C =>
    natequiv_compose
      (natequiv_adjunction_l adj1 (G' y0))
      (natequiv_prewhisker
         (natequiv_adjunction_l adj2 y0) F)) y x)
  intros x.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
x: A
Is1Natural (opyon ((fun x : A => F' (F x)) x))
  (opyon x o (fun x : C => G (G' x)))
  (fun y : C =>
   (fun y0 : C =>
    natequiv_compose
      (natequiv_adjunction_l adj1 (G' y0))
      (natequiv_prewhisker
         (natequiv_adjunction_l adj2 y0) F)) y x)
  rapply is1natural_comp.
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
x: A
Is1Natural (fun a : C => yon (G' a) (F x))
  (fun x0 : C => opyon x (G (G' x0)))
  (fun a : C => natequiv_adjunction_l adj1 (G' a) x)
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
x: A
Is1Natural (opyon (F' (F x)))
  (fun a : C => yon (G' a) (F x))
  (fun a : C =>
   natequiv_prewhisker 
     (natequiv_adjunction_l adj2 a) F x)
  +
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
x: A
Is1Natural (fun a : C => yon (G' a) (F x))
  (fun x0 : C => opyon x (G (G' x0)))
  (fun a : C => natequiv_adjunction_l adj1 (G' a) x) exact (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)).
  +
A, B, C: Type
F: A -> B
G: B -> A
F': B -> C
G': C -> B
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor F'
Is0Functor3: Is0Functor G'
adj1: F ⊣ G
adj2: F' ⊣ G'
x: A
Is1Natural (opyon (F' (F x)))
  (fun a : C => yon (G' a) (F x))
  (fun a : C =>
   natequiv_prewhisker 
     (natequiv_adjunction_l adj2 a) F x) napply is1natural_equiv_adjunction_r.
Defined.

(** Replace the left functor in an adjunction by a naturally equivalent one. *)
Lemma adjunction_natequiv_left {C D : Type} (F F' : C -> D) (G : D -> C)
  `{Is1Cat C, HasEquivs D, !HasMorExt D,
    !Is0Functor F, !Is0Functor F', !Is0Functor G} 
  : NatEquiv F F' -> F ⊣ G -> F' ⊣ G.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
NatEquiv F F' -> F ⊣ G -> F' ⊣ G
Proof.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
NatEquiv F F' -> F ⊣ G -> F' ⊣ G
  intros e adj.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
F' ⊣ G
  snapply Build_Adjunction_natequiv_nat_right.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
forall y : D, NatEquiv (yon y o F') (yon (G y))
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
forall x : C,
Is1Natural (opyon (F' x)) 
  (opyon x o G) (fun y : D => ?e y x)
  {
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
forall y : D, NatEquiv (yon y o F') (yon (G y)) intros y.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
y: D
NatEquiv (yon y o F') (yon (G y))
    refine (natequiv_compose (natequiv_adjunction_l adj _) _).
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
y: D
NatEquiv (fun x : C => yon y (F' x))
  (fun x : C => yon y (F x))
    exact (natequiv_postwhisker _ (natequiv_op e)). }
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
forall x : C,
Is1Natural (opyon (F' x)) 
  (opyon x o G)
  (fun y : D =>
   (fun y0 : D =>
    natequiv_compose (natequiv_adjunction_l adj y0)
      (natequiv_postwhisker (yon y0) (natequiv_op e)))
     y x)
  intros x.
C, D: Type
F, F': C -> D
G: D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H0: Is1Cat D
H1: HasEquivs D
HasMorExt0: HasMorExt D
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor F'
Is0Functor2: Is0Functor G
e: NatEquiv F F'
adj: F ⊣ G
x: C
Is1Natural (opyon (F' x)) 
  (opyon x o G)
  (fun y : D =>
   (fun y0 : D =>
    natequiv_compose (natequiv_adjunction_l adj y0)
      (natequiv_postwhisker (yon y0) (natequiv_op e)))
     y x)
  rapply is1natural_comp.
Defined.

(** Replace the right functor in an adjunction by a naturally equivalent one. *)
Lemma adjunction_natequiv_right {C D : Type} (F : C -> D) (G G' : D -> C)
  `{HasEquivs C, Is1Cat D, !HasMorExt C,
    !Is0Functor F, !Is0Functor G, !Is0Functor G'} 
  : NatEquiv G G' -> F ⊣ G -> F ⊣ G'.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
NatEquiv G G' -> F ⊣ G -> F ⊣ G'
Proof.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
NatEquiv G G' -> F ⊣ G -> F ⊣ G'
  intros e adj.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
F ⊣ G'
  snapply Build_Adjunction_natequiv_nat_left.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
forall x : C, NatEquiv (opyon (F x)) (opyon x o G')
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
forall y : D,
Is1Natural (yon y o F) 
  (yon (G' y)) (fun x : C^op => ?e x y)
  {
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
forall x : C, NatEquiv (opyon (F x)) (opyon x o G') intros x.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
x: C
NatEquiv (opyon (F x)) (opyon x o G')
    refine (natequiv_compose _ (natequiv_adjunction_r adj _)).
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
x: C
NatEquiv (fun x0 : D => opyon x (G x0))
  (fun x0 : D => opyon x (G' x0))
    exact (natequiv_postwhisker _ e). }
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
forall y : D,
Is1Natural (yon y o F) 
  (yon (G' y))
  (fun x : C^op =>
   (fun x0 : C =>
    natequiv_compose
      (natequiv_postwhisker (opyon x0) e)
      (natequiv_adjunction_r adj x0)) x y)
  intros y.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
y: D
Is1Natural (yon y o F) 
  (yon (G' y))
  (fun x : C^op =>
   (fun x0 : C =>
    natequiv_compose
      (natequiv_postwhisker (opyon x0) e)
      (natequiv_adjunction_r adj x0)) x y)
  rapply is1natural_comp.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
y: D
Is1Natural (fun a : C^op => opyon a (G y))
  (yon (G' y))
  (fun a : C^op => natequiv_postwhisker (opyon a) e y)
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
y: D
Is1Natural (fun x : C => yon y (F x))
  (fun a : C^op => opyon a (G y))
  (fun a : C^op => natequiv_adjunction_r adj a y)
  2: exact _.
C, D: Type
F: C -> D
G, G': D -> C
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H: Is1Cat C
H0: HasEquivs C
IsGraph1: IsGraph D
Is2Graph1: Is2Graph D
Is01Cat1: Is01Cat D
H1: Is1Cat D
HasMorExt0: HasMorExt C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor G'
e: NatEquiv G G'
adj: F ⊣ G
y: D
Is1Natural (fun a : C^op => opyon a (G y))
  (yon (G' y))
  (fun a : C^op => natequiv_postwhisker (opyon a) e y)
  rapply is1natural_yoneda.
Defined.