(A : PreCategory) : IsFullyFaithful (coyoneda A). Proof. intros a b. pose proof (@isisomorphism_inverse _ _ _ _ (@isisomorphism_components_of _ _ _ _ _ _ (@isisomorphism_components_of _ _ _ _ _ _ (@coyoneda_lemma _ A) (@coyoneda _ A b)) a)) as H'. simpl in *. unfold coyoneda_lemma_morphism_inverse in *; simpl in *. unfold Functors.inverse_object_of_morphism_of in *; simpl in *. let m := match type of H' with IsIsomorphism ?m => constr:(m) end in apply isisomorphism_set_cat_natural_transformation_paths with (T1 := m). - simpl. clear H'. intros; apply path_forall; intro; rewrite left_identity, right_identity; reflexivity. - destruct H' as [m' H0' H1']. (exists m'). + exact H0'. + exact H1'. 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.