(* -*- mode: coq; mode: visual-line -*-  *)

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

(** ** Two-variable hom-functors *)

Global Instance is0functor_hom {A} `{Is01Cat A}
  : @Is0Functor (A^op * A) Type _ _ (uncurry (@Hom A _)).
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Functor (uncurry Hom)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Functor (uncurry Hom)
  apply Build_Is0Functor.
A: Type
H: IsGraph A
H0: Is01Cat A
forall a b : A^op * A,
(a $-> b) -> uncurry Hom a $-> uncurry Hom b
  intros [a1 a2] [b1 b2] [f1 f2] g; cbn in *.
A: Type
H: IsGraph A
H0: Is01Cat A
a1: A^op
a2: A
b1: A^op
b2: A
f1: b1 $-> a1
f2: a2 $-> b2
g: uncurry Hom (a1, a2)
uncurry Hom (b1, b2)
  exact (f2 $o g $o f1).
Defined.

(** This requires morphism extensionality! *)
Global Instance is1functor_hom {A} `{HasMorExt A}
  : @Is1Functor (A^op * A) Type _ _ _ _ _ _ _ _ (uncurry (@Hom A _)) _.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
Is1Functor (uncurry Hom)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
Is1Functor (uncurry Hom)
  apply Build_Is1Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall (a b : A^op * A) 
(f g : a $-> b),
f $== g ->
fmap (uncurry Hom) f $== fmap (uncurry Hom) g
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall a : A^op * A,
fmap (uncurry Hom) (Id a) $== Id (uncurry Hom a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall (a b c : A^op * A) 
(f : a $-> b) (g : b $-> c),
fmap (uncurry Hom) (g $o f) $==
fmap (uncurry Hom) g $o fmap (uncurry Hom) f
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall (a b : A^op * A) 
(f g : a $-> b),
f $== g ->
fmap (uncurry Hom) f $== fmap (uncurry Hom) g intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p1 p2] q;
      unfold fst, snd in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
f1: a1 $-> b1
f2: a2 $-> b2
g1: a1 $-> b1
g2: a2 $-> b2
p1: f1 $-> g1
p2: f2 $-> g2
q: uncurry Hom (a1, a2)
fmap (uncurry Hom) (f1, f2) q =
fmap (uncurry Hom) (g1, g2) q
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
f1: a1 $-> b1
f2: a2 $-> b2
g1: a1 $-> b1
g2: a2 $-> b2
p1: f1 $-> g1
p2: f2 $-> g2
q: uncurry Hom (a1, a2)
fmap (uncurry Hom) (f1, f2) q $==
fmap (uncurry Hom) (g1, g2) q
    refine (((p2 $@R q) $@R _) $@ ((g2 $o q) $@L p1)).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall a : A^op * A,
fmap (uncurry Hom) (Id a) $== Id (uncurry Hom a) intros [a1 a2] f; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
f: uncurry Hom (a1, a2)
Id a2 $o f $o Id a1 = f
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
f: uncurry Hom (a1, a2)
Id a2 $o f $o Id a1 $== f
    exact (cat_idr _ $@ cat_idl f).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
forall (a b c : A^op * A) 
(f : a $-> b) (g : b $-> c),
fmap (uncurry Hom) (g $o f) $==
fmap (uncurry Hom) g $o fmap (uncurry Hom) f intros [a1 a2] [b1 b2] [c1 c2] [f1 f2] [g1 g2] h; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
g2 $o f2 $o h $o (f1 $o g1) =
g2 $o (f2 $o h $o f1) $o g1
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
g2 $o f2 $o h $o (f1 $o g1) $==
g2 $o (f2 $o h $o f1) $o g1
    refine (cat_assoc _ _ _ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
g2 $o f2 $o (h $o (f1 $o g1)) $==
g2 $o (f2 $o h $o f1) $o g1
    refine (cat_assoc _ _ _ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
g2 $o (f2 $o (h $o (f1 $o g1))) $==
g2 $o (f2 $o h $o f1) $o g1
    refine (_ $@ cat_assoc_opp _ _ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
g2 $o (f2 $o (h $o (f1 $o g1))) $==
g2 $o (f2 $o h $o f1 $o g1)
    refine (g2 $@L _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
f2 $o (h $o (f1 $o g1)) $== f2 $o h $o f1 $o g1
    refine (_ $@ cat_assoc_opp _ _ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasMorExt A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: b1 $-> a1
f2: a2 $-> b2
g1: c1 $-> b1
g2: b2 $-> c2
h: uncurry Hom (a1, a2)
f2 $o (h $o (f1 $o g1)) $== f2 $o h $o (f1 $o g1)
    refine (cat_assoc_opp _ _ _).
Defined.

Global Instance is0bifunctor_hom {A} `{Is01Cat A}
  : Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _).
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Bifunctor Hom
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Bifunctor Hom
  nrapply Build_Is0Bifunctor'.
A: Type
H: IsGraph A
H0: Is01Cat A
Is01Cat A^op
A: Type
H: IsGraph A
H0: Is01Cat A
Is01Cat A
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Functor (uncurry Hom)
  1-2: exact _.
A: Type
H: IsGraph A
H0: Is01Cat A
Is0Functor (uncurry Hom)
  exact is0functor_hom.
Defined.

(** While it is possible to prove the bifunctor coherence condition from [Is1Cat_Strong], 1-functoriality requires morphism extensionality.*)
Global Instance is1bifunctor_hom {A} `{Is1Cat A} `{HasMorExt A}
  : Is1Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph A
Is2Graph1: Is2Graph A
Is01Cat1: Is01Cat A
H0: Is1Cat A
H1: HasMorExt A
Is1Bifunctor Hom
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph A
Is2Graph1: Is2Graph A
Is01Cat1: Is01Cat A
H0: Is1Cat A
H1: HasMorExt A
Is1Bifunctor Hom
  nrapply Build_Is1Bifunctor'.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph A
Is2Graph1: Is2Graph A
Is01Cat1: Is01Cat A
H0: Is1Cat A
H1: HasMorExt A
Is1Functor (uncurry Hom)
  exact is1functor_hom.
Defined.

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

(** ** The covariant Yoneda lemma *)

(** This is easier than the contravariant version because it doesn't involve any "op"s. *)

Definition opyon {A : Type} `{IsGraph A} (a : A) : A -> Type
  := fun b => (a $-> b).

(** We prove this explicitly instead of using the bifunctor instance above so that we can apply [fmap] in each argument independently without mapping an identity in the other. *)
Global Instance is0functor_opyon {A : Type} `{Is01Cat A} (a : A)
  : Is0Functor (opyon a).
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
Is0Functor (opyon a)
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
Is0Functor (opyon a)
  apply Build_Is0Functor.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
forall a0 b : A,
(a0 $-> b) -> opyon a a0 $-> opyon a b
  unfold opyon; intros b c f g; cbn in *.
A: Type
H: IsGraph A
H0: Is01Cat A
a, b, c: A
f: b $-> c
g: a $-> b
a $-> c
  exact (f $o g).
Defined.

Global Instance is1functor_opyon {A : Type} `{Is1Cat A} `{!HasMorExt A} (a : A)
  : Is1Functor (opyon a).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
Is1Functor (opyon a)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
Is1Functor (opyon a)
  rapply Build_Is1Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall (a0 b : A) (f g : a0 $-> b),
f $== g -> fmap (opyon a) f $== fmap (opyon a) g
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall a0 : A,
fmap (opyon a) (Id a0) $== Id (opyon a a0)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall (a0 b c : A) (f : a0 $-> b) 
(g : b $-> c),
fmap (opyon a) (g $o f) $==
fmap (opyon a) g $o fmap (opyon a) f
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall (a0 b : A) (f g : a0 $-> b),
f $== g -> fmap (opyon a) f $== fmap (opyon a) g intros x y f g p h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x, y: A
f, g: x $-> y
p: f $== g
h: opyon a x
fmap (opyon a) f h = fmap (opyon a) g h
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x, y: A
f, g: x $-> y
p: f $== g
h: opyon a x
fmap (opyon a) f h $== fmap (opyon a) g h
    apply (cat_prewhisker p).
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall a0 : A,
fmap (opyon a) (Id a0) $== Id (opyon a a0) intros x h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x: A
h: opyon a x
fmap (opyon a) (Id x) h = Id (opyon a x) h
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x: A
h: opyon a x
fmap (opyon a) (Id x) h $== Id (opyon a x) h
    apply cat_idl.
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
forall (a0 b c : A) (f : a0 $-> b) 
(g : b $-> c),
fmap (opyon a) (g $o f) $==
fmap (opyon a) g $o fmap (opyon a) f intros x y z f g h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x, y, z: A
f: x $-> y
g: y $-> z
h: opyon a x
fmap (opyon a) (g $o f) h =
(fmap (opyon a) g $o fmap (opyon a) f) h
    apply path_hom.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a, x, y, z: A
f: x $-> y
g: y $-> z
h: opyon a x
fmap (opyon a) (g $o f) h $==
(fmap (opyon a) g $o fmap (opyon a) f) h
    apply cat_assoc.
Defined.

(** We record these corollaries here, since we use some of them below. *)
Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
  {x y z : A} (f : y $<~> z)
  : (x $-> y) <~> (x $-> z)
  := emap (opyon x) f.

Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
  {x y z : A} (f : x $<~> y)
  : (y $-> z) <~> (x $-> z)
  := @equiv_postcompose_cat_equiv A^op _ _ _ _ _ _ z y x f.

(* The following implicitly use [hasequivs_core].  Note that when [A] has morphism extensionality, it doesn't follow that [core A] does.  We'd need to know that being an equivalence is a proposition, and we don't assume that (since even for [Type] it requires [Funext], see [hasmorext_core_type]). So we need to assume this in the following results. *)

(** Postcomposition with a cat_equiv is an equivalence between the types of equivalences. *)
Definition equiv_postcompose_core_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt (core A)}
  {x y z : A} (f : y $<~> z)
  : (x $<~> y) <~> (x $<~> z).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: y $<~> z
(x $<~> y) <~> (x $<~> z)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: y $<~> z
(x $<~> y) <~> (x $<~> z)
  change ((Build_core x $-> Build_core y) <~> (Build_core x $-> Build_core z)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: y $<~> z
({| uncore := x |} $-> {| uncore := y |}) <~>
({| uncore := x |} $-> {| uncore := z |})
  refine (equiv_postcompose_cat_equiv (A := core A) _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: y $<~> z
{| uncore := y |} $<~> {| uncore := z |}
  exact f.  (* It doesn't work to insert [f] on the previous line. *)
Defined.

Definition equiv_precompose_core_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt (core A)}
  {x y z : A} (f : x $<~> y)
  : (y $<~> z) <~> (x $<~> z).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: x $<~> y
(y $<~> z) <~> (x $<~> z)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: x $<~> y
(y $<~> z) <~> (x $<~> z)
  change ((Build_core y $-> Build_core z) <~> (Build_core x $-> Build_core z)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: x $<~> y
({| uncore := y |} $-> {| uncore := z |}) <~>
({| uncore := x |} $-> {| uncore := z |})
  refine (equiv_precompose_cat_equiv (A := core A) _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt (core A)
x, y, z: A
f: x $<~> y
{| uncore := x |} $<~> {| uncore := y |}
  exact f.  (* It doesn't work to insert [f] on the previous line. *)
Defined.

Definition opyoneda {A : Type} `{Is01Cat A} (a : A)
           (F : A -> Type) {ff : Is0Functor F}
  : F a -> (opyon a $=> F).
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
F: A -> Type
ff: Is0Functor F
F a -> opyon a $=> F
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
F: A -> Type
ff: Is0Functor F
F a -> opyon a $=> F
  intros x b f.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
F: A -> Type
ff: Is0Functor F
x: F a
b: A
f: opyon a b
F b
  exact (fmap F f x).
Defined.

Definition un_opyoneda {A : Type} `{Is01Cat A}
  (a : A) (F : A -> Type) {ff : Is0Functor F}
  : (opyon a $=> F) -> F a
  := fun alpha => alpha a (Id a).

Global Instance is1natural_opyoneda {A : Type} `{Is1Cat A}
  (a : A) (F : A -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
  : Is1Natural (opyon a) F (opyoneda a F x).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
Is1Natural (opyon a) F (opyoneda a F x)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
Is1Natural (opyon a) F (opyoneda a F x)
  unfold opyon, opyoneda; intros b c f g; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b, c: A
f: b $-> c
g: a $-> b
fmap F (f $o g) x = fmap F f (fmap F g x)
  exact (fmap_comp F g f x).
Defined.

(** This is form of injectivity of [opyoneda]. *)
Definition opyoneda_isinj {A : Type} `{Is1Cat A} (a : A)
  (F : A -> Type) `{!Is0Functor F, !Is1Functor F}
  (x x' : F a) (p : forall b, opyoneda a F x b == opyoneda a F x' b)
  : x = x'.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda a F x b == opyoneda a F x' b
x = x'
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda a F x b == opyoneda a F x' b
x = x'
  refine ((fmap_id F a x)^ @ _ @ fmap_id F a x').
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda a F x b == opyoneda a F x' b
fmap F (Id a) x = fmap F (Id a) x'
  cbn in p.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda a F x b == opyoneda a F x' b
fmap F (Id a) x = fmap F (Id a) x'
  exact (p a (Id a)).
Defined.

(** This says that [opyon] is faithful, although we haven't yet defined a graph structure on natural transformations to express this in that way.  This follows from the previous result, but then would need [HasMorExt A], since the previous result assumes that [F] is a 1-functor, which is stronger than what is needed.  The direct proof below only needs the weaker assumption [Is1Cat_Strong A]. *)
Definition opyon_faithful {A : Type} `{Is1Cat_Strong A}
  (a b : A) (f g : b $-> a)
  (p : forall (c : A) (h : a $-> c), h $o f = h $o g)
  : f = g
  := (cat_idl_strong f)^ @ p a (Id a) @ cat_idl_strong g.

(** The composite in one direction is the identity map. *)
Definition opyoneda_issect {A : Type} `{Is1Cat A} (a : A)
           (F : A -> Type) `{!Is0Functor F, !Is1Functor F}
           (x : F a)
  : un_opyoneda a F (opyoneda a F x) = x
  := fmap_id F a x.

(** We assume for the converse that the coherences in [A] are equalities (this is a weak funext-type assumption).  Note that we do not in general recover the witness of 1-naturality.  Indeed, if [A] is fully coherent, then a transformation of the form [opyoneda a F x] is always also fully coherently natural, so an incoherent witness of 1-naturality could not be recovered in this way.  *)
Definition opyoneda_isretr {A : Type} `{Is1Cat_Strong A} (a : A)
           (F : A -> Type) `{!Is0Functor F, !Is1Functor F}
           (alpha : opyon a $=> F) {alnat : Is1Natural (opyon a) F alpha}
           (b : A)
  : opyoneda a F (un_opyoneda a F alpha) b $== alpha b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
opyoneda a F (un_opyoneda a F alpha) b $== alpha b
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
opyoneda a F (un_opyoneda a F alpha) b $== alpha b
  unfold opyoneda, un_opyoneda, opyon; intros f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
f: a $-> b
fmap F f (alpha a (Id a)) = alpha b f
  refine ((isnat alpha f (Id a))^ @ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
f: a $-> b
(alpha b $o fmap (opyon a) f) (Id a) = alpha b f
  cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
f: a $-> b
alpha b (f $o Id a) = alpha b f
  apply ap.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat_Strong A
a: A
F: A -> Type
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon a $=> F
alnat: Is1Natural (opyon a) F alpha
b: A
f: a $-> b
f $o Id a = f
  exact (cat_idr_strong f).
Defined.

(** A natural transformation between representable functors induces a map between the representing objects. *)
Definition opyon_cancel {A : Type} `{Is01Cat A} (a b : A)
  : (opyon a $=> opyon b) -> (b $-> a)
  := un_opyoneda a (opyon b).

Definition opyon1 {A : Type} `{Is01Cat A} (a : A) : Fun01 A Type.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
Fun01 A Type
Proof.
A: Type
H: IsGraph A
H0: Is01Cat A
a: A
Fun01 A Type
  rapply (Build_Fun01 _ _ (opyon a)).
Defined.

Definition opyon11 {A : Type} `{Is1Cat A} `{!HasMorExt A} (a : A) : Fun11 A Type.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
Fun11 A Type
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
HasMorExt0: HasMorExt A
a: A
Fun11 A Type
  rapply (Build_Fun11 _ _ (opyon a)).
Defined.

(** An equivalence between representable functors induces an equivalence between the representing objects. *)
Definition opyon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
           {a b : A}
  : (opyon1 a $<~> opyon1 b) -> (b $<~> a).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
opyon1 a $<~> opyon1 b -> b $<~> a
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
opyon1 a $<~> opyon1 b -> b $<~> a
  intros f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
b $<~> a
  refine (cate_adjointify (f a (Id a)) (f^-1$ b (Id b)) _ _);
    apply GpdHom_path; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
f a (Id a) $o (f b)^-1 (Id b) = Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
(f b)^-1 (Id b) $o f a (Id a) = Id b
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
f a (Id a) $o (f b)^-1 (Id b) = Id a refine ((isnat_natequiv (natequiv_inverse f) (f a (Id a)) (Id b))^ @ _); cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
(f a)^-1 (f a (Id a) $o Id b) = Id a
    refine (_ @ cate_issect (f a) (Id a)); cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
(f a)^-1 (f a (Id a) $o Id b) = (f a)^-1 (f a (Id a))
    apply ap.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
f a (Id a) $o Id b = f a (Id a)
    srapply cat_idr_strong.
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
(f b)^-1 (Id b) $o f a (Id a) = Id b refine ((isnat_natequiv f (f^-1$ b (Id b)) (Id a))^ @ _); cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
f b ((f b)^-1 (Id b) $o Id a) = Id b
    refine (_ @ cate_isretr (f b) (Id b)); cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
f b ((f b)^-1 (Id b) $o Id a) = f b ((f b)^-1 (Id b))
    apply ap.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
Is1Cat_Strong0: Is1Cat_Strong A
a, b: A
f: opyon1 a $<~> opyon1 b
(f b)^-1 (Id b) $o Id a = (f b)^-1 (Id b)
    srapply cat_idr_strong.
Defined.

Definition natequiv_opyon_equiv {A : Type} `{HasEquivs A}
  `{!HasMorExt A} {a b : A}
  : (b $<~> a) -> (opyon1 a $<~> opyon1 b).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
b $<~> a -> opyon1 a $<~> opyon1 b
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
b $<~> a -> opyon1 a $<~> opyon1 b
  intro e.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
opyon1 a $<~> opyon1 b
  snrapply Build_NatEquiv.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
forall a0 : A, opyon a a0 $<~> opyon b a0
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
Is1Natural (opyon a) (opyon b) (fun a0 : A => ?e a0)
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
forall a0 : A, opyon a a0 $<~> opyon b a0 intros c.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
c: A
opyon a c $<~> opyon b c
    exact (equiv_precompose_cat_equiv e).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
HasMorExt0: HasMorExt A
a, b: A
e: b $<~> a
Is1Natural (opyon a) (opyon b)
  (fun a0 : A =>
   (fun c : A => equiv_precompose_cat_equiv e) a0) rapply is1natural_opyoneda.
Defined.

(** ** The covariant Yoneda lemma using 0-groupoids *)

(** We repeat the above, regarding [opyon] as landing in 0-groupoids, using the 1-category structure on [ZeroGpd] in [ZeroGroupoid.v].  This has many advantages.  It avoids [HasMorExt], which means that we don't need [Funext] in many examples.  It also avoids [Is1Cat_Strong], which means the results all have the same hypotheses, namely that [A] is a 1-category.  This allows us to simplify the proof of [opyon_equiv_0gpd], making use of [opyoneda_isretr_0gpd]. *)

Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd
  := fun b => Build_ZeroGpd (a $-> b) _ _ _.

Global Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A}
  : Is0Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Functor (uncurry opyon_0gpd)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Functor (uncurry opyon_0gpd)
  nrapply Build_Is0Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a b : A^op * A,
(a $-> b) ->
uncurry opyon_0gpd a $-> uncurry opyon_0gpd b
  intros [a1 a2] [b1 b2] [f1 f2]; unfold op in *; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1, a2, b1, b2: A
f1: b1 $-> a1
f2: a2 $-> b2
Morphism_0Gpd (uncurry opyon_0gpd (a1, a2))
  (uncurry opyon_0gpd (b1, b2))
  rapply (Build_Morphism_0Gpd (opyon_0gpd a1 a2) (opyon_0gpd b1 b2)
          (cat_postcomp b1 f2 o cat_precomp a2 f1)).
Defined.

Global Instance is1functor_hom_0gpd {A : Type} `{Is1Cat A}
  : Is1Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Functor (uncurry opyon_0gpd)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Functor (uncurry opyon_0gpd)
  nrapply Build_Is1Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A^op * A) 
(f g : a $-> b),
f $== g ->
fmap (uncurry opyon_0gpd) f $==
fmap (uncurry opyon_0gpd) g
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a : A^op * A,
fmap (uncurry opyon_0gpd) (Id a) $==
Id (uncurry opyon_0gpd a)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A^op * A) 
(f : a $-> b) (g : b $-> c),
fmap (uncurry opyon_0gpd) (g $o f) $==
fmap (uncurry opyon_0gpd) g $o
fmap (uncurry opyon_0gpd) f
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b : A^op * A) 
(f g : a $-> b),
f $== g ->
fmap (uncurry opyon_0gpd) f $==
fmap (uncurry opyon_0gpd) g intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p q] h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
b1: A^op
b2: A
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (a1, a2) $-> fst (b1, b2)
g2: snd (a1, a2) $-> snd (b1, b2)
p: fst (f1, f2) $-> fst (g1, g2)
q: snd (f1, f2) $-> snd (g1, g2)
h: uncurry opyon_0gpd (a1, a2)
fmap (uncurry opyon_0gpd) (f1, f2) h $==
fmap (uncurry opyon_0gpd) (g1, g2) h
    exact (h $@L p $@@ q).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall a : A^op * A,
fmap (uncurry opyon_0gpd) (Id a) $==
Id (uncurry opyon_0gpd a) intros [a1 a2] h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
h: uncurry opyon_0gpd (a1, a2)
fmap (uncurry opyon_0gpd) (Id (a1, a2)) h $==
Id (uncurry opyon_0gpd (a1, a2)) h
    exact (cat_idl _ $@ cat_idr _).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
forall (a b c : A^op * A) 
(f : a $-> b) (g : b $-> c),
fmap (uncurry opyon_0gpd) (g $o f) $==
fmap (uncurry opyon_0gpd) g $o
fmap (uncurry opyon_0gpd) f intros [a1 a2] [b1 b2] [c1 c2] [f1 f2] [g1 g2] h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h: uncurry opyon_0gpd (a1, a2)
fmap (uncurry opyon_0gpd) ((g1, g2) $o (f1, f2)) h $==
(fmap (uncurry opyon_0gpd) (g1, g2) $o
 fmap (uncurry opyon_0gpd) (f1, f2)) h
    refine (cat_assoc _ _ _ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h: uncurry opyon_0gpd (a1, a2)
g2 $o
(f2 $o cat_precomp a2 (fst ((g1, g2) $o (f1, f2))) h) $==
(fmap (uncurry opyon_0gpd) (g1, g2) $o
 fmap (uncurry opyon_0gpd) (f1, f2)) h
    refine (g2 $@L _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h: uncurry opyon_0gpd (a1, a2)
f2 $o cat_precomp a2 (fst ((g1, g2) $o (f1, f2))) h $==
cat_precomp b2 g1
  (fmap (uncurry opyon_0gpd) (f1, f2) h)
    refine (_ $@L (cat_assoc_opp _ _ _) $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a1: A^op
a2: A
b1: A^op
b2: A
c1: A^op
c2: A
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h: uncurry opyon_0gpd (a1, a2)
f2 $o (h $o f1 $o g1) $==
cat_precomp b2 g1
  (fmap (uncurry opyon_0gpd) (f1, f2) h)
    exact (cat_assoc_opp _ _ _).
Defined.

Global Instance is0bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
  : Is0Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor opyon_0gpd
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Bifunctor opyon_0gpd
  snrapply Build_Is0Bifunctor'.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is01Cat A^op
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is01Cat A
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Functor (uncurry opyon_0gpd)
  1,2: exact _.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is0Functor (uncurry opyon_0gpd)
  exact is0functor_hom_0gpd.
Defined.

Global Instance is1bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
  : Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Bifunctor opyon_0gpd
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Bifunctor opyon_0gpd
  snrapply Build_Is1Bifunctor'.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
Is1Functor (uncurry opyon_0gpd)
  exact is1functor_hom_0gpd.
Defined.

Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
  : Is0Functor (opyon_0gpd a).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
Is0Functor (opyon_0gpd a)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
Is0Functor (opyon_0gpd a)
  apply Build_Is0Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall a0 b : A,
(a0 $-> b) -> opyon_0gpd a a0 $-> opyon_0gpd a b
  intros b c f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, b, c: A
f: b $-> c
opyon_0gpd a b $-> opyon_0gpd a c
  exact (Build_Morphism_0Gpd (opyon_0gpd a b) (opyon_0gpd a c) (cat_postcomp a f) _).
Defined.

Global Instance is1functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
  : Is1Functor (opyon_0gpd a).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
Is1Functor (opyon_0gpd a)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
Is1Functor (opyon_0gpd a)
  rapply Build_Is1Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall (a0 b : A) (f g : a0 $-> b),
f $== g ->
fmap (opyon_0gpd a) f $== fmap (opyon_0gpd a) g
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall a0 : A,
fmap (opyon_0gpd a) (Id a0) $== Id (opyon_0gpd a a0)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall (a0 b c : A) (f : a0 $-> b) 
(g : b $-> c),
fmap (opyon_0gpd a) (g $o f) $==
fmap (opyon_0gpd a) g $o fmap (opyon_0gpd a) f
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall (a0 b : A) (f g : a0 $-> b),
f $== g ->
fmap (opyon_0gpd a) f $== fmap (opyon_0gpd a) g intros x y f g p h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, x, y: A
f, g: x $-> y
p: f $== g
h: opyon_0gpd a x
fmap (opyon_0gpd a) f h $== fmap (opyon_0gpd a) g h
    apply (cat_prewhisker p).
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall a0 : A,
fmap (opyon_0gpd a) (Id a0) $== Id (opyon_0gpd a a0) intros x h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, x: A
h: opyon_0gpd a x
fmap (opyon_0gpd a) (Id x) h $== Id (opyon_0gpd a x) h
    apply cat_idl.
  +
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
forall (a0 b c : A) (f : a0 $-> b) 
(g : b $-> c),
fmap (opyon_0gpd a) (g $o f) $==
fmap (opyon_0gpd a) g $o fmap (opyon_0gpd a) f intros x y z f g h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a, x, y, z: A
f: x $-> y
g: y $-> z
h: opyon_0gpd a x
fmap (opyon_0gpd a) (g $o f) h $==
(fmap (opyon_0gpd a) g $o fmap (opyon_0gpd a) f) h
    apply cat_assoc.
Defined.

Definition opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A)
           (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  : F a -> (opyon_0gpd a $=> F).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F a -> opyon_0gpd a $=> F
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
F a -> opyon_0gpd a $=> F
  intros x b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b: A
opyon_0gpd a b $-> F b
  refine (Build_Morphism_0Gpd (opyon_0gpd a b) (F b) (fun f => fmap F f x) _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b: A
Is0Functor (fun f : opyon_0gpd a b => fmap F f x)
  rapply Build_Is0Functor.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b: A
forall a0 b0 : opyon_0gpd a b,
(a0 $-> b0) -> fmap F a0 x $-> fmap F b0 x
  intros f1 f2 h.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b: A
f1, f2: opyon_0gpd a b
h: f1 $-> f2
fmap F f1 x $-> fmap F f2 x
  exact (fmap2 F h x).
Defined.

Definition un_opyoneda_0gpd {A : Type} `{Is1Cat A}
  (a : A) (F : A -> ZeroGpd) {ff : Is0Functor F}
  : (opyon_0gpd a $=> F) -> F a
  := fun alpha => alpha a (Id a).

Global Instance is1natural_opyoneda_0gpd {A : Type} `{Is1Cat A}
  (a : A) (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F} (x : F a)
  : Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x)
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x)
  unfold opyon_0gpd, opyoneda_0gpd; intros b c f g; cbn in *.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x: F a
b, c: A
f: b $-> c
g: a $-> b
fmap F (cat_postcomp a f g) x $==
fmap F f (fmap F g x)
  exact (fmap_comp F g f x).
Defined.

(** This is form of injectivity of [opyoneda_0gpd]. *)
Definition opyoneda_isinj_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (x x' : F a) (p : forall b : A, opyoneda_0gpd a F x b $== opyoneda_0gpd a F x' b)
  : x $== x'.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda_0gpd a F x b $== opyoneda_0gpd a F x' b
x $== x'
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda_0gpd a F x b $== opyoneda_0gpd a F x' b
x $== x'
  refine ((fmap_id F a x)^$ $@ _ $@ fmap_id F a x').
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall b : A,
opyoneda_0gpd a F x b $== opyoneda_0gpd a F x' b
fmap F (Id a) x $== fmap F (Id a) x'
  cbn in p.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
x, x': F a
p: forall (b : A) (x0 : a $-> b),
fmap F x0 x $== fmap F x0 x'
fmap F (Id a) x $== fmap F (Id a) x'
  exact (p a (Id a)).
Defined.

(** This says that [opyon_0gpd] is faithful, although we haven't yet defined a graph structure on natural transformations to express this in that way. *)
Definition opyon_faithful_0gpd {A : Type} `{Is1Cat A} (a b : A)
  (f g : b $-> a) (p : forall (c : A) (h : a $-> c), h $o f $== h $o g)
  : f $== g
  := opyoneda_isinj_0gpd a _ f g p.

(** The composite in one direction is the identity map. *)
Definition opyoneda_issect_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (x : F a)
  : un_opyoneda_0gpd a F (opyoneda_0gpd a F x) $== x
  := fmap_id F a x.

(** For the other composite, note that we do not in general recover the witness of 1-naturality.  Indeed, if [A] is fully coherent, then a transformation of the form [opyoneda a F x] is always also fully coherently natural, so an incoherent witness of 1-naturality could not be recovered in this way.  *)
Definition opyoneda_isretr_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (alpha : opyon_0gpd a $=> F) {alnat : Is1Natural (opyon_0gpd a) F alpha}
  (b : A)
  : opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b $== alpha b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b $==
alpha b
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b $==
alpha b
  unfold opyoneda, un_opyoneda, opyon; intros f.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
f: opyon_0gpd a b
opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b f $==
alpha b f
  refine ((isnat alpha f (Id a))^$ $@ _).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
f: opyon_0gpd a b
(alpha b $o fmap (opyon_0gpd a) f) (Id a) $==
alpha b f
  cbn.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
f: opyon_0gpd a b
alpha b (cat_postcomp a f (Id a)) $== alpha b f
  apply (fmap (alpha b)).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
a: A
F: A -> ZeroGpd
Is0Functor0: Is0Functor F
Is1Functor0: Is1Functor F
alpha: opyon_0gpd a $=> F
alnat: Is1Natural (opyon_0gpd a) F alpha
b: A
f: opyon_0gpd a b
cat_postcomp a f (Id a) $-> f
  exact (cat_idr f).
Defined.

(** A natural transformation between representable functors induces a map between the representing objects. *)
Definition opyon_cancel_0gpd {A : Type} `{Is1Cat A} (a b : A)
  : (opyon_0gpd a $=> opyon_0gpd b) -> (b $-> a)
  := un_opyoneda_0gpd a (opyon_0gpd b).

(** Since no extra hypotheses are needed, we use the name with "1" for the [Fun11] version. *)
Definition opyon1_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun11 A ZeroGpd
  := Build_Fun11 _ _ (opyon_0gpd a).

(** An equivalence between representable functors induces an equivalence between the representing objects.  We explain how this compares to [opyon_equiv] above.  Instead of assuming that each [f c : (a $-> c) -> (b $-> c)] is an equivalence of types, it only needs to be an equivalence of 0-groupoids.  For example, this means that we have a map [g c : (b $-> c) -> (a $-> c)] such that for each [k : a $-> c], [g c (f c k) $== k], rather than [g c (f c k) = k] as the version with types requires.  Similarly, the naturality is up to 2-cells, instead of up to paths.  This allows us to avoid [Funext] and [HasMorExt] when using this result.  As a side benefit, we also don't require that [A] is strong. The proof is also simpler, since we can re-use the work done in [opyoneda_isretr_0gpd]. *)
Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A}
  {a b : A} (f : opyon1_0gpd a $<~> opyon1_0gpd b)
  : b $<~> a.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
b $<~> a
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
b $<~> a
  (* These are the maps that will define the desired equivalence: *)
  set (fa := (cate_fun f a) (Id a)).     (* Equivalently, [un_opyoneda_0gpd a _ f]. *)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
b $<~> a
  set (gb := (cate_fun f^-1$ b) (Id b)). (* Equivalently, [un_opyoneda_0gpd b _ f^-1$]. *)
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
gb:= f^-1$ b (Id b): opyon1_0gpd a b
b $<~> a
  srapply (cate_adjointify fa gb).
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
gb:= f^-1$ b (Id b): opyon1_0gpd a b
fa $o gb $== Id a
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
gb:= f^-1$ b (Id b): opyon1_0gpd a b
gb $o fa $== Id b
  (* [opyoneda_0gpd] is defined by postcomposition, so [opyoneda_isretr_0gpd] simplifies both LHSs.*)
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
gb:= f^-1$ b (Id b): opyon1_0gpd a b
fa $o gb $== Id a exact (opyoneda_isretr_0gpd _ _ f^-1$ a fa $@ cat_eissect (f a) (Id a)).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
f: opyon1_0gpd a $<~> opyon1_0gpd b
fa:= f a (Id a): opyon1_0gpd b a
gb:= f^-1$ b (Id b): opyon1_0gpd a b
gb $o fa $== Id b exact (opyoneda_isretr_0gpd _ _ f     b gb $@ cat_eisretr (f b) (Id b)).
Defined.

(** Since [opyon_0gpd] is a 1-functor, postcomposition with a [cat_equiv] is an equivalence between the hom 0-groupoids. Note that we do not require [HasMorExt], as [equiv_postcompose_cat_equiv] does. *)
Definition equiv_postcompose_cat_equiv_0gpd {A : Type} `{HasEquivs A}
  {x y z : A} (f : y $<~> z)
  : opyon_0gpd x y $<~> opyon_0gpd x z
  := emap (opyon_0gpd x) f.

(** The dual result, which is used in the next result. *)
Definition equiv_precompose_cat_equiv_0gpd {A : Type} `{HasEquivs A}
  {x y z : A} (f : x $<~> y)
  : opyon_0gpd y z $<~> opyon_0gpd x z
  := @equiv_postcompose_cat_equiv_0gpd A^op _ _ _ _ _ z y x f.

(** A converse to [opyon_equiv_0gpd].  Together, we get a logical equivalence between [b $<~> a] and [opyon_0gpd a $<~> opyon_0gpd b], without [HasMorExt]. *)
Definition natequiv_opyon_equiv_0gpd {A : Type} `{HasEquivs A}
  {a b : A} (e : b $<~> a)
  : opyon1_0gpd a $<~> opyon1_0gpd b.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
opyon1_0gpd a $<~> opyon1_0gpd b
Proof.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
opyon1_0gpd a $<~> opyon1_0gpd b
  snrapply Build_NatEquiv.
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
forall a0 : A, opyon1_0gpd a a0 $<~> opyon1_0gpd b a0
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
Is1Natural (opyon1_0gpd a) 
  (opyon1_0gpd b) (fun a0 : A => ?e a0)
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
forall a0 : A, opyon1_0gpd a a0 $<~> opyon1_0gpd b a0 intro c; exact (equiv_precompose_cat_equiv_0gpd e).
  -
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
a, b: A
e: b $<~> a
Is1Natural (opyon1_0gpd a) 
  (opyon1_0gpd b)
  (fun a0 : A =>
   (fun c : A => equiv_precompose_cat_equiv_0gpd e) a0) rapply is1natural_opyoneda_0gpd.
Defined.

(** ** The contravariant Yoneda lemma *)

(** We can deduce this from the covariant version with some boilerplate. *)

Definition yon {A : Type} `{IsGraph A} (a : A) : A^op -> Type
  := opyon (A:=A^op) a.

Global Instance is0functor_yon {A : Type} `{H : Is01Cat A} (a : A)
  : Is0Functor (yon a)
  := is0functor_opyon (A:=A^op) a.

Global Instance is1functor_yon {A : Type} `{H : Is1Cat A} `{!HasMorExt A} (a : A)
  : Is1Functor (yon a)
  := is1functor_opyon (A:=A^op) a.

Definition yoneda {A : Type} `{Is01Cat A} (a : A)
           (F : A^op -> Type) `{!Is0Functor F}
  : F a -> (yon a $=> F)
  := @opyoneda (A^op) _ _ a F _.

Definition un_yoneda {A : Type} `{Is01Cat A} (a : A)
           (F : A^op -> Type) `{!Is0Functor F}
  : (yon a $=> F) -> F a
  := un_opyoneda (A:=A^op) a F.

Global Instance is1natural_yoneda {A : Type} `{Is1Cat A} (a : A)
       (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
  : Is1Natural (yon a) F (yoneda a F x)
  := is1natural_opyoneda (A:=A^op) a F x.

Definition yoneda_isinj {A : Type} `{Is1Cat A} (a : A)
  (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F}
  (x x' : F a) (p : forall b, yoneda a F x b == yoneda a F x' b)
  : x = x'
  := opyoneda_isinj (A:=A^op) a F x x' p.

Definition yon_faithful {A : Type} `{Is1Cat_Strong A}
  (a b : A) (f g : b $-> a)
  (p : forall (c : A) (h : c $-> b), f $o h = g $o h)
  : f = g
  := opyon_faithful (A:=A^op) b a f g p.

Definition yoneda_issect {A : Type} `{Is1Cat A} (a : A)
           (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
  : un_yoneda a F (yoneda a F x) = x
  := opyoneda_issect (A:=A^op) a F x.

Definition yoneda_isretr {A : Type} `{Is1Cat_Strong A} (a : A)
           (F : A^op -> Type) `{!Is0Functor F}
           (* Without the hint here, Coq guesses to first project from [Is1Cat_Strong A] and then pass to opposites, whereas what we need is to first pass to opposites and then project. *)
           `{@Is1Functor _ _ _ _ _ (is1cat_is1cat_strong A^op) _ _ _ _ F _}
           (alpha : yon a $=> F) {alnat : Is1Natural (yon a) F alpha}
           (b : A)
  : yoneda a F (un_yoneda a F alpha) b $== alpha b
  := opyoneda_isretr (A:=A^op) a F alpha b.

Definition yon_cancel {A : Type} `{Is01Cat A} (a b : A)
  : (yon a $=> yon b) -> (a $-> b)
  := un_yoneda a (yon b).

Definition yon1 {A : Type} `{Is01Cat A} (a : A) : Fun01 A^op Type
  := opyon1 (A:=A^op) a.

Definition yon11 {A : Type} `{Is1Cat A} `{!HasMorExt A} (a : A) : Fun11 A^op Type
  := opyon11 (A:=A^op) a.

Definition yon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
           (a b : A)
  : (yon1 a $<~> yon1 b) -> (a $<~> b)
  := opyon_equiv (A:=A^op).

Definition natequiv_yon_equiv {A : Type} `{HasEquivs A}
  `{!HasMorExt A} (a b : A)
  : (a $<~> b) -> (yon1 a $<~> yon1 b)
  := natequiv_opyon_equiv (A:=A^op).

(** ** The contravariant Yoneda lemma using 0-groupoids *)

Definition yon_0gpd {A : Type} `{Is1Cat A} (a : A) : A^op -> ZeroGpd
  := opyon_0gpd (A:=A^op) a.

Global Instance is0functor_yon_0gpd {A : Type} `{Is1Cat A} (a : A)
  : Is0Functor (yon_0gpd a)
  := is0functor_opyon_0gpd (A:=A^op) a.

Global Instance is1functor_yon_0gpd {A : Type} `{Is1Cat A} (a : A)
  : Is1Functor (yon_0gpd a)
  := is1functor_opyon_0gpd (A:=A^op) a.

Definition yoneda_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  : F a -> (yon_0gpd a $=> F)
  := opyoneda_0gpd (A:=A^op) a F.

Definition un_yoneda_0gpd {A : Type} `{Is1Cat A}
  (a : A) (F : A^op -> ZeroGpd) {ff : Is0Functor F}
  : (yon_0gpd a $=> F) -> F a
  := un_opyoneda_0gpd (A:=A^op) a F.

Global Instance is1natural_yoneda_0gpd {A : Type} `{Is1Cat A}
  (a : A) (F : A^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F} (x : F a)
  : Is1Natural (yon_0gpd a) F (yoneda_0gpd a F x)
  := is1natural_opyoneda_0gpd (A:=A^op) a F x.

Definition yoneda_isinj_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (x x' : F a) (p : forall b : A, yoneda_0gpd a F x b $== yoneda_0gpd a F x' b)
  : x $== x'
  := opyoneda_isinj_0gpd (A:=A^op) a F x x' p.

Definition yon_faithful_0gpd {A : Type} `{Is1Cat A} (a b : A)
  (f g : b $-> a) (p : forall (c : A) (h : c $-> b), f $o h $== g $o h)
  : f $== g
  := opyon_faithful_0gpd (A:=A^op) b a f g p.

Definition yoneda_issect_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (x : F a)
  : un_yoneda_0gpd a F (yoneda_0gpd a F x) $== x
  := opyoneda_issect_0gpd (A:=A^op) a F x.

Definition yoneda_isretr_0gpd {A : Type} `{Is1Cat A} (a : A)
  (F : A^op -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
  (alpha : yon_0gpd a $=> F) {alnat : Is1Natural (yon_0gpd a) F alpha}
  (b : A)
  : yoneda_0gpd a F (un_yoneda_0gpd a F alpha) b $== alpha b
  := opyoneda_isretr_0gpd (A:=A^op) a F alpha b.

Definition yon_cancel_0gpd {A : Type} `{Is1Cat A} (a b : A)
  : (yon_0gpd a $=> yon_0gpd b) -> (a $-> b)
  := opyon_cancel_0gpd (A:=A^op) a b.

Definition yon1_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun11 A^op ZeroGpd
  := opyon1_0gpd (A:=A^op) a.

Definition yon_equiv_0gpd {A : Type} `{HasEquivs A}
  {a b : A} (f : yon1_0gpd a $<~> yon1_0gpd b)
  : a $<~> b
  := opyon_equiv_0gpd (A:=A^op) f.

Definition natequiv_yon_equiv_0gpd {A : Type} `{HasEquivs A}
  {a b : A} (e : a $<~> b)
  : yon1_0gpd (A:=A) a $<~> yon1_0gpd b
  := natequiv_opyon_equiv_0gpd (A:=A^op) (e : CatEquiv (A:=A^op) b a).