(** * The Yoneda Lemma *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Dual Functor.Dual.
Require Import Functor.Composition.Core.
Require Import Category.Morphisms FunctorCategory.Morphisms.
Require Import SetCategory.
Require Import Functor.Attributes.
Require Import Functor.Composition.Functorial.
Require Import Functor.Identity.
Require Import HomFunctor.
Require Import FunctorCategory.Core.
Require Import NaturalTransformation.Paths.
Require Import HoTT.Tactics.

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

Local Open Scope morphism_scope.
Local Open Scope category_scope.
Local Open Scope functor_scope.

(** Quoting Wikipedia on the Yoneda lemma (changing [A] to [a] and
    [C] to [A] so that we can use unicode superscripts and
    subscripts):

    In mathematics, specifically in category theory, the Yoneda lemma
    is an abstract result on functors of the type morphisms into a
    fixed object. It is a vast generalisation of Cayley's theorem from
    group theory (viewing a group as a particular kind of category
    with just one object). It allows the embedding of any category
    into a category of functors (contravariant set-valued functors)
    defined on that category. It also clarifies how the embedded
    category, of representable functors and their natural
    transformations, relates to the other objects in the larger
    functor category. It is an important tool that underlies several
    modern developments in algebraic geometry and representation
    theory. It is named after Nobuo Yoneda.

    ** Generalities

    The Yoneda lemma suggests that instead of studying the (locally
    small) category [A], one should study the category of all functors
    of [A] into [Set] (the category of sets with functions as
    morphisms). [Set] is a category we understand well, and a functor
    of [A] into [Set] can be seen as a "representation" of [A] in
    terms of known structures. The original category [A] is contained
    in this functor category, but new objects appear in the functor
    category which were absent and "hidden" in [A]. Treating these new
    objects just like the old ones often unifies and simplifies the
    theory.  This approach is akin to (and in fact generalizes) the
    common method of studying a ring by investigating the modules over
    that ring. The ring takes the place of the category [A], and the
    category of modules over the ring is a category of functors
    defined on [A].

    ** Formal statement

    *** General version

    Yoneda's lemma concerns functors from a fixed category [A] to the
    category of sets, [Set]. If [A] is a locally small category
    (i.e. the hom-sets are actual sets and not proper classes), then
    each object [a] of [A] gives rise to a natural functor to [Set]
    called a hom-functor. This functor is denoted:

    [hᵃ = Hom(a, ─)].

    The (covariant) hom-functor [hᵃ] sends [x] to the set of morphisms
    [Hom(a, x)] and sends a morphism [f] from [x] to [y] to the
    morphism [f ∘ ─] (composition with [f] on the left) that sends a
    morphism [g] in [Hom(a, x)] to the morphism [f ∘ g] in [Hom(a,
    y)]. That is,

    [f ↦ Hom(a, f) = ⟦ Hom(a, x) ∋ g ↦ f ∘ g ∈ Hom(a,y) ⟧].
 *)

(** ** The (co-)Yoneda functors [A → (Aᵒᵖ → set)] *)
Section yoneda.
  Context `{Funext}.

  (* TODO(JasonGross): Find a way to unify the [yoneda] and [coyoneda] lemmas into a single lemma which is more functorial. *)

  Definition coyoneda A : Functor A^op (A -> set_cat)
    := ExponentialLaws.Law4.Functors.inverse _ _ _ (hom_functor A).

  Definition yoneda A : Functor A (A^op -> set_cat)
    := coyoneda A^op.
End yoneda.

(** ** The (co-)Yoneda lemma *)
Section coyoneda_lemma.

  Section functor.
    Context `{Funext}.

    Variable A : PreCategory.
    (** Let [F] be an arbitrary functor from [A] to [Set]. Then Yoneda's
      lemma says that: *)
    (*Variable F : Functor A (@set_cat fs).*)
    (** For each object [a] of [A], *)
    (*Variable a : A.*)
    (** the natural transformations from [hᵃ] to [F] are in one-to-one
      correspondence with the elements of [F(a)]. That is,

      [Nat(hᵃ, F) ≅ F(a)].

      Moreover this isomorphism is natural in [a] and [F] when both
      sides are regarded as functors from [Setᴬ × A] to
      [Set].

      Given a natural transformation [Φ] from [hᵃ] to [F], the
      corresponding element of [F(a)] is [u = Φₐ(idₐ)]. *)

    (*   Definition coyoneda_lemma_morphism (a : A)
  : morphism set_cat
             (BuildhSet
                (morphism (A -> set_cat) (coyoneda A a) F)
                _)
             (F a)
    := fun phi => phi a 1%morphism. *)


    Definition coyoneda_functor
    : Functor (A -> set_cat)
              (A -> set_cat)
      := (compose_functor _ _ set_cat (coyoneda A)^op)
           o (yoneda (A -> set_cat)).
  End functor.

  Section nt.
    Context `{Funext}.

    Variable A : PreCategory.

    Definition coyoneda_natural_transformation_helper F
    : morphism (_ -> _) (coyoneda_functor A F) F.
H: Funext
A: PreCategory
F: A -> set_cat
morphism (A -> set_cat)
  ((coyoneda_functor A) _0 F)%object F
    Proof.
H: Funext
A: PreCategory
F: A -> set_cat
morphism (A -> set_cat)
  ((coyoneda_functor A) _0 F)%object F
      refine (Build_NaturalTransformation
                (coyoneda_functor A F) F
                (fun a phi => phi a 1%morphism)
                _).
H: Funext
A: PreCategory
F: A -> set_cat
forall (s d : A) (m : morphism A s d),
((fun
    phi : Trunc.trunctype_type
            (((coyoneda_functor A) _0 F) _0 d)%object
  => phi d 1)
 o ((coyoneda_functor A) _0 F)%object _1 m)%morphism =
(F _1 m
 o (fun
      phi : Trunc.trunctype_type
              (((coyoneda_functor A) _0 F) _0 s)%object
    => phi s 1))%morphism
      simpl.
H: Funext
A: PreCategory
F: A -> set_cat
forall (s d : A) (m : morphism A s d),
(fun
   x : NaturalTransformation
         (Functors.inverse_object_of_object_of
            (hom_functor A) s) F =>
 x d (1 o 1 o m)%morphism) =
(fun
   x : NaturalTransformation
         (Functors.inverse_object_of_object_of
            (hom_functor A) s) F =>
 (F _1 m) (x s 1%morphism))
      abstract (
          repeat (intro || apply path_forall);
          simpl in *;
            match goal with
              | [ T : NaturalTransformation _ _ |- _ ]
                => simpl rewrite <- (fun s d m => apD10 (commutes T s d m))
            end;
          rewrite ?left_identity, ?right_identity;
          reflexivity
        ).
    Defined.

    Definition coyoneda_natural_transformation
    : morphism (_ -> _)
               (coyoneda_functor A)
               1.
H: Funext
A: PreCategory
morphism ((A -> set_cat) -> A -> set_cat)
  (coyoneda_functor A) 1
    Proof.
H: Funext
A: PreCategory
morphism ((A -> set_cat) -> A -> set_cat)
  (coyoneda_functor A) 1
      hnf.
H: Funext
A: PreCategory
NaturalTransformation (coyoneda_functor A) 1
      simpl.
H: Funext
A: PreCategory
NaturalTransformation (coyoneda_functor A) 1
      let F := match goal with |- NaturalTransformation ?F ?G => constr:(F) end in
      let G := match goal with |- NaturalTransformation ?F ?G => constr:(G) end in
      refine (Build_NaturalTransformation
                F G
                coyoneda_natural_transformation_helper
                _).
H: Funext
A: PreCategory
forall (s d : (A -> set_cat)%category)
(m : morphism (A -> set_cat) s d),
(coyoneda_natural_transformation_helper d
 o (coyoneda_functor A) _1 m)%morphism =
(1 _1 m o coyoneda_natural_transformation_helper s)%morphism
      simpl.
H: Funext
A: PreCategory
forall (s d : Functor A set_cat)
(m : NaturalTransformation s d),
Core.compose
  (coyoneda_natural_transformation_helper d)
  (Core.whisker_r
     (Functors.inverse_object_of_morphism_of
        (hom_functor (A -> set_cat)^op) s d m)
     (coyoneda A)^op) =
Core.compose m
  (coyoneda_natural_transformation_helper s)
      abstract (repeat first [ intro
                             | progress path_natural_transformation
                             | reflexivity ]).
    Defined.
  End nt.

  Definition coyoneda_lemma_morphism_inverse
             `{Funext}
             A
             (F : object (A -> set_cat))
             a
  : morphism set_cat
             (F a)
             (coyoneda_functor A F a).
H: Funext
A: PreCategory
F: A -> set_cat
a: A
morphism set_cat (F _0 a)%object
  (((coyoneda_functor A) _0 F) _0 a)%object
  Proof.
H: Funext
A: PreCategory
F: A -> set_cat
a: A
morphism set_cat (F _0 a)%object
  (((coyoneda_functor A) _0 F) _0 a)%object
    intro Fa.
H: Funext
A: PreCategory
F: A -> set_cat
a: A
Fa: Trunc.trunctype_type (F _0 a)%object
Trunc.trunctype_type
  (((coyoneda_functor A) _0 F) _0 a)%object
    hnf.
H: Funext
A: PreCategory
F: A -> set_cat
a: A
Fa: Trunc.trunctype_type (F _0 a)%object
NaturalTransformation
  (snd (F, ((coyoneda A)^op _0 a)%object))
  (fst (F, ((coyoneda A)^op _0 a)%object))
    simpl in *.
H: Funext
A: PreCategory
F: Functor A set_cat
a: A
Fa: Trunc.trunctype_type (F _0 a)%object
NaturalTransformation
  (Functors.inverse_object_of_object_of
     (hom_functor A) a) F
    let F0 := match goal with |- NaturalTransformation ?F ?G => constr:(F) end in
    let G0 := match goal with |- NaturalTransformation ?F ?G => constr:(G) end in
    refine (Build_NaturalTransformation
              F0 G0
              (fun a' : A => (fun f : morphism A a a' => F _1 f Fa))
              _
           ).
H: Funext
A: PreCategory
F: Functor A set_cat
a: A
Fa: Trunc.trunctype_type (F _0 a)%object
forall (s d : A) (m : morphism A s d),
((fun f : morphism A a d => (F _1 f) Fa)
 o (Functors.inverse_object_of_object_of
      (hom_functor A) a) _1 m)%morphism =
(F _1 m o (fun f : morphism A a s => (F _1 f) Fa))%morphism
    simpl.
H: Funext
A: PreCategory
F: Functor A set_cat
a: A
Fa: Trunc.trunctype_type (F _0 a)%object
forall (s d : A) (m : morphism A s d),
(fun x : morphism A a s => (F _1 (m o x o 1)) Fa) =
(fun x : morphism A a s => (F _1 m) ((F _1 x) Fa))
    abstract (
        repeat first [ reflexivity
                     | intro
                     | apply path_forall
                     | progress rewrite ?composition_of, ?identity_of ]
      ).
  Defined.

  #[export] Instance coyoneda_lemma `{Funext} A
  : IsIsomorphism (coyoneda_natural_transformation A).
H: Funext
A: PreCategory
IsIsomorphism (coyoneda_natural_transformation A)
  Proof.
H: Funext
A: PreCategory
IsIsomorphism (coyoneda_natural_transformation A)
    eapply isisomorphism_natural_transformation.
H: Funext
A: PreCategory
forall x : (A -> set_cat)%category,
IsIsomorphism (coyoneda_natural_transformation A x)
    simpl.
H: Funext
A: PreCategory
forall x : Functor A set_cat,
IsIsomorphism
  (coyoneda_natural_transformation_helper x)
    intro F.
H: Funext
A: PreCategory
F: Functor A set_cat
IsIsomorphism
  (coyoneda_natural_transformation_helper F)
    eapply isisomorphism_natural_transformation.
H: Funext
A: PreCategory
F: Functor A set_cat
forall x : A,
IsIsomorphism
  (coyoneda_natural_transformation_helper F x)
    intro a.
H: Funext
A: PreCategory
F: Functor A set_cat
a: A
IsIsomorphism
  (coyoneda_natural_transformation_helper F a)
    simpl.
H: Funext
A: PreCategory
F: Functor A set_cat
a: A
IsIsomorphism
  (fun
     phi : NaturalTransformation
             (Functors.inverse_object_of_object_of
                (hom_functor A) a) F =>
   phi a 1%morphism)
    exists (coyoneda_lemma_morphism_inverse F a);
      simpl in *;
    abstract (
        repeat (intro || apply path_forall || path_natural_transformation);
        simpl in *;
          solve [ simpl rewrite <- (fun c d m => ap10 (commutes x c d m));
                  rewrite ?right_identity, ?left_identity;
                  reflexivity
                | rewrite identity_of;
                  reflexivity ]
      ).
  Defined.
End coyoneda_lemma.

Section yoneda_lemma.
  (** There is a contravariant version of Yoneda's lemma which
      concerns contravariant functors from [A] to [Set]. This version
      involves the contravariant hom-functor

      [hₐ = Hom(─, A)],

      which sends [x] to the hom-set [Hom(x, a)]. Given an arbitrary
      contravariant functor [G] from [A] to [Set], Yoneda's lemma
      asserts that

      [Nat(hₐ, G) ≅ G(a)]. *)

  Section functor.
    Context `{Funext}.

    Variable A : PreCategory.
    (** Let [F] be an arbitrary functor from [A] to [Set]. Then Yoneda's
      lemma says that: *)
    (*Variable F : Functor A (@set_cat fs).*)
    (** For each object [a] of [A], *)
    (*Variable a : A.*)
    (** the natural transformations from [hᵃ] to [F] are in one-to-one
      correspondence with the elements of [F(a)]. That is,

      [Nat(hᵃ, F) ≅ F(a)].

      Moreover this isomorphism is natural in [a] and [F] when both
      sides are regarded as functors from [Setᴬ × A] to
      [Set].

      Given a natural transformation [Φ] from [hᵃ] to [F], the
      corresponding element of [F(a)] is [u = Φₐ(idₐ)]. *)

    (* Definition yoneda_lemma_morphism A (G : object (A^op -> set_cat)) (a : A)
  : morphism set_cat
             (BuildhSet
                (morphism (A^op -> set_cat) (yoneda A a) G)
                _)
             (G a)
    := fun phi => phi a 1%morphism.*)

    Definition yoneda_functor
    : Functor (A^op -> set_cat)
              (A^op -> set_cat)
      := coyoneda_functor A^op.
  End functor.

  Context `{Funext}.

  Variable A : PreCategory.

  Definition yoneda_natural_transformation
  : morphism (_ -> _)
             1
             (yoneda_functor A)
    := @morphism_inverse _ _ _ _ (coyoneda_lemma A^op).

  #[export] Instance yoneda_lemma
  : IsIsomorphism yoneda_natural_transformation
    := @isisomorphism_inverse _ _ _ _ (coyoneda_lemma A^op).
End yoneda_lemma.

(** ** The Yoneda embedding

    An important special case of Yoneda's lemma is when the functor
    [F] from [A] to [Set] is another hom-functor [hᵇ]. In this case,
    the covariant version of Yoneda's lemma states that

    [Nat(hᵃ, hᵇ) ≅ Hom(b, a)].

    That is, natural transformations between hom-functors are in
    one-to-one correspondence with morphisms (in the reverse
    direction) between the associated objects. Given a morphism [f : b
    → a] the associated natural transformation is denoted [Hom(f, ─)].

    Mapping each object [a] in [A] to its associated hom-functor [hᵃ=
    Hom(a, ─)] and each morphism [f : B → A] to the corresponding
    natural transformation [Hom(f, ─)] determines a contravariant
    functor [h⁻] from [A] to [Setᴬ], the functor category of all
    (covariant) functors from [A] to [Set]. One can interpret [h⁻] as
    a covariant functor:

    [h⁻ : Aᵒᵖ → Setᴬ].

    The meaning of Yoneda's lemma in this setting is that the functor
    [h⁻] is fully faithful, and therefore gives an embedding of [Aᵒᵖ]
    in the category of functors to [Set]. The collection of all
    functors {[hᵃ], [a] in [A]} is a subcategory of [Set̂ᴬ]. Therefore,
    Yoneda embedding implies that the category [Aᵒᵖ] is isomorphic to
    the category {[hᵃ], [a] in [A]}.

    The contravariant version of Yoneda's lemma states that

    [Nat(hₐ, h_b) ≅ Hom(a, b)].

    Therefore, [h₋] gives rise to a covariant functor from [A] to the
    category of contravariant functors to [Set]:

    [h₋ : A → Set⁽⁽ᴬ⁾ᵒᵖ⁾].

    Yoneda's lemma then states that any locally small category [A] can
    be embedded in the category of contravariant functors from [A] to
    [Set] via [h₋]. This is called the Yoneda embedding. *)

Section FullyFaithful.
  Context `{Funext}.

  Definition coyoneda_embedding (A : PreCategory) : IsFullyFaithful (coyoneda A).
H: Funext
A: PreCategory
IsFullyFaithful (coyoneda A)
  Proof.
H: Funext
A: PreCategory
IsFullyFaithful (coyoneda A)
    intros a b.
H: Funext
A: PreCategory
a, b: A^op%category
IsIsomorphism
  (induced_hom_natural_transformation (coyoneda A)
     (a, b))
    pose proof (@isisomorphism_inverse
                  _ _ _ _
                  (@isisomorphism_components_of
                     _ _ _ _ _ _
                     (@isisomorphism_components_of
                        _ _ _ _ _ _
                        (@coyoneda_lemma _ A)
                        (@coyoneda _ A b))
                     a)) as H'.
H: Funext
A: PreCategory
a, b: A^op%category
H': IsIsomorphism
  (coyoneda_natural_transformation A
     ((coyoneda A) _0 b)%object a)^-1
IsIsomorphism
  (induced_hom_natural_transformation (coyoneda A)
     (a, b))
    simpl in *.
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (coyoneda_lemma_morphism_inverse
     (Functors.inverse_object_of_object_of
        (hom_functor A) b) a)
IsIsomorphism
  (fun m : morphism A b a =>
   Functors.inverse_object_of_morphism_of
     (hom_functor A) a b m)
    unfold coyoneda_lemma_morphism_inverse in *; simpl in *.
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
IsIsomorphism
  (fun m : morphism A b a =>
   Functors.inverse_object_of_morphism_of
     (hom_functor A) a b m)
    unfold Functors.inverse_object_of_morphism_of in *; simpl in *.
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
IsIsomorphism
  (fun m : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (c : A) (g : morphism A a c) =>
      (1 o g o m)%morphism)
     (Functors.inverse_object_of_morphism_of_subproof
        (hom_functor A) a b m))
    let m := match type of H' with IsIsomorphism ?m => constr:(m) end in
    apply isisomorphism_set_cat_natural_transformation_paths with (T1 := m).
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
forall
(x : Trunc.trunctype_type
       {|
         Trunc.trunctype_type := morphism A b a;
         Trunc.trunctype_istrunc :=
           trunc_morphism A b a
       |}) (y : A),
Build_NaturalTransformation
  (Functors.inverse_object_of_object_of
     (hom_functor A) a)
  (Functors.inverse_object_of_object_of
     (hom_functor A) b)
  (fun (a' : A) (f : morphism A a a') =>
   (f o x o 1)%morphism)
  (coyoneda_lemma_morphism_inverse_subproof
     (Functors.inverse_object_of_object_of
        (hom_functor A) b) a x) y =
Build_NaturalTransformation
  (Functors.inverse_object_of_object_of
     (hom_functor A) a)
  (Functors.inverse_object_of_object_of
     (hom_functor A) b)
  (fun (c : A) (g : morphism A a c) =>
   (1 o g o x)%morphism)
  (Functors.inverse_object_of_morphism_of_subproof
     (hom_functor A) a b x) y
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
    -
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
forall
(x : Trunc.trunctype_type
       {|
         Trunc.trunctype_type := morphism A b a;
         Trunc.trunctype_istrunc :=
           trunc_morphism A b a
       |}) (y : A),
Build_NaturalTransformation
  (Functors.inverse_object_of_object_of
     (hom_functor A) a)
  (Functors.inverse_object_of_object_of
     (hom_functor A) b)
  (fun (a' : A) (f : morphism A a a') =>
   (f o x o 1)%morphism)
  (coyoneda_lemma_morphism_inverse_subproof
     (Functors.inverse_object_of_object_of
        (hom_functor A) b) a x) y =
Build_NaturalTransformation
  (Functors.inverse_object_of_object_of
     (hom_functor A) a)
  (Functors.inverse_object_of_object_of
     (hom_functor A) b)
  (fun (c : A) (g : morphism A a c) =>
   (1 o g o x)%morphism)
  (Functors.inverse_object_of_morphism_of_subproof
     (hom_functor A) a b x) y simpl.
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
forall (x : morphism A b a) (y : A),
(fun f : morphism A a y => (f o x o 1)%morphism) =
(fun g : morphism A a y => (1 o g o x)%morphism)
      clear H'.
H: Funext
A: PreCategory
a, b: A
forall (x : morphism A b a) (y : A),
(fun f : morphism A a y => (f o x o 1)%morphism) =
(fun g : morphism A a y => (1 o g o x)%morphism)
      intros; apply path_forall;
      intro;
      rewrite left_identity, right_identity;
      reflexivity.
    -
H: Funext
A: PreCategory
a, b: A
H': IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa)) destruct H' as [m' H0' H1'].
H: Funext
A: PreCategory
a, b: A
m': morphism set_cat
  {|
    Trunc.trunctype_type :=
      NaturalTransformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b);
    Trunc.trunctype_istrunc :=
      trunc_natural_transformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b)
  |}
  {|
    Trunc.trunctype_type := morphism A b a;
    Trunc.trunctype_istrunc :=
      trunc_morphism A b a
  |}
H0': (m'
o (fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)))%morphism =
1%morphism
H1': ((fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
IsIsomorphism
  (fun Fa : morphism A b a =>
   Build_NaturalTransformation
     (Functors.inverse_object_of_object_of
        (hom_functor A) a)
     (Functors.inverse_object_of_object_of
        (hom_functor A) b)
     (fun (a' : A) (f : morphism A a a') =>
      (f o Fa o 1)%morphism)
     (coyoneda_lemma_morphism_inverse_subproof
        (Functors.inverse_object_of_object_of
           (hom_functor A) b) a Fa))
      (exists m').
H: Funext
A: PreCategory
a, b: A
m': morphism set_cat
  {|
    Trunc.trunctype_type :=
      NaturalTransformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b);
    Trunc.trunctype_istrunc :=
      trunc_natural_transformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b)
  |}
  {|
    Trunc.trunctype_type := morphism A b a;
    Trunc.trunctype_istrunc :=
      trunc_morphism A b a
  |}
H0': (m'
o (fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)))%morphism =
1%morphism
H1': ((fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
(m'
 o (fun Fa : morphism A b a =>
    Build_NaturalTransformation
      (Functors.inverse_object_of_object_of
         (hom_functor A) a)
      (Functors.inverse_object_of_object_of
         (hom_functor A) b)
      (fun (a' : A) (f : morphism A a a') =>
       f o Fa o 1)
      (coyoneda_lemma_morphism_inverse_subproof
         (Functors.inverse_object_of_object_of
            (hom_functor A) b) a Fa)))%morphism =
1%morphism
H: Funext
A: PreCategory
a, b: A
m': morphism set_cat
  {|
    Trunc.trunctype_type :=
      NaturalTransformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b);
    Trunc.trunctype_istrunc :=
      trunc_natural_transformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b)
  |}
  {|
    Trunc.trunctype_type := morphism A b a;
    Trunc.trunctype_istrunc :=
      trunc_morphism A b a
  |}
H0': (m'
o (fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)))%morphism =
1%morphism
H1': ((fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
((fun Fa : morphism A b a =>
  Build_NaturalTransformation
    (Functors.inverse_object_of_object_of
       (hom_functor A) a)
    (Functors.inverse_object_of_object_of
       (hom_functor A) b)
    (fun (a' : A) (f : morphism A a a') => f o Fa o 1)
    (coyoneda_lemma_morphism_inverse_subproof
       (Functors.inverse_object_of_object_of
          (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
      +
H: Funext
A: PreCategory
a, b: A
m': morphism set_cat
  {|
    Trunc.trunctype_type :=
      NaturalTransformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b);
    Trunc.trunctype_istrunc :=
      trunc_natural_transformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b)
  |}
  {|
    Trunc.trunctype_type := morphism A b a;
    Trunc.trunctype_istrunc :=
      trunc_morphism A b a
  |}
H0': (m'
o (fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)))%morphism =
1%morphism
H1': ((fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
(m'
 o (fun Fa : morphism A b a =>
    Build_NaturalTransformation
      (Functors.inverse_object_of_object_of
         (hom_functor A) a)
      (Functors.inverse_object_of_object_of
         (hom_functor A) b)
      (fun (a' : A) (f : morphism A a a') =>
       f o Fa o 1)
      (coyoneda_lemma_morphism_inverse_subproof
         (Functors.inverse_object_of_object_of
            (hom_functor A) b) a Fa)))%morphism =
1%morphism exact H0'.
      +
H: Funext
A: PreCategory
a, b: A
m': morphism set_cat
  {|
    Trunc.trunctype_type :=
      NaturalTransformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b);
    Trunc.trunctype_istrunc :=
      trunc_natural_transformation
        (Functors.inverse_object_of_object_of
           (hom_functor A) a)
        (Functors.inverse_object_of_object_of
           (hom_functor A) b)
  |}
  {|
    Trunc.trunctype_type := morphism A b a;
    Trunc.trunctype_istrunc :=
      trunc_morphism A b a
  |}
H0': (m'
o (fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)))%morphism =
1%morphism
H1': ((fun Fa : morphism A b a =>
Build_NaturalTransformation
(Functors.inverse_object_of_object_of (hom_functor A) a)
(Functors.inverse_object_of_object_of (hom_functor A) b)
(fun (a' : A) (f : morphism A a a') => f o Fa o 1)
(coyoneda_lemma_morphism_inverse_subproof
(Functors.inverse_object_of_object_of (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism
((fun Fa : morphism A b a =>
  Build_NaturalTransformation
    (Functors.inverse_object_of_object_of
       (hom_functor A) a)
    (Functors.inverse_object_of_object_of
       (hom_functor A) b)
    (fun (a' : A) (f : morphism A a a') => f o Fa o 1)
    (coyoneda_lemma_morphism_inverse_subproof
       (Functors.inverse_object_of_object_of
          (hom_functor A) b) a Fa)) o m')%morphism =
1%morphism exact H1'.
  Qed.

  Definition yoneda_embedding (A : PreCategory) : IsFullyFaithful (yoneda A).
H: Funext
A: PreCategory
IsFullyFaithful (yoneda A)
  Proof.
H: Funext
A: PreCategory
IsFullyFaithful (yoneda A)
    intros a b.
H: Funext
A: PreCategory
a, b: A
IsIsomorphism
  (induced_hom_natural_transformation (yoneda A)
     (a, b))
    pose proof (@coyoneda_embedding A^op a b) as CYE.
H: Funext
A: PreCategory
a, b: A
CYE: IsIsomorphism (induced_hom_natural_transformation (coyoneda A^op) (a, b))
IsIsomorphism
  (induced_hom_natural_transformation (yoneda A)
     (a, b))
    unfold yoneda.
H: Funext
A: PreCategory
a, b: A
CYE: IsIsomorphism (induced_hom_natural_transformation (coyoneda A^op) (a, b))
IsIsomorphism
  (induced_hom_natural_transformation (coyoneda A^op)
     (a, b))
    let T := type of CYE in
    let T' := (eval simpl in T) in
    pose proof ((fun x : T => (x : T')) CYE) as CYE'.
H: Funext
A: PreCategory
a, b: A
CYE: IsIsomorphism (induced_hom_natural_transformation (coyoneda A^op) (a, b))
CYE': IsIsomorphism
  (fun m : morphism A a b =>
   Functors.inverse_object_of_morphism_of
     (hom_functor A^op) a b m)
IsIsomorphism
  (induced_hom_natural_transformation (coyoneda A^op)
     (a, b))
    let G := match goal with |- ?G => constr:(G) end in
    let G' := (eval simpl in G) in
    exact ((fun x : G' => (x : G)) CYE').
  Qed.
End FullyFaithful.