(A : PreCategory) : IsFullyFaithful (yoneda A). Proof. intros a b. pose proof (@coyoneda_embedding A^op a b) as CYE. unfold yoneda. let T := type of CYE in let T' := (eval simpl in T) in pose proof ((fun x : T => (x : T')) CYE) as CYE'. 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.
Require Import Category.Core Functor.Core NaturalTransformation.Core. 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.