proposition: Proposition representability_by_yoneda (C : Category) (F : C^op ⟶ Sets) (c : C): @Isomorphism Sets {| carrier := { x : F c & IsIsomorphism (from (Yoneda_Lemma C F c ) x) } |} (Build_SetoidObject (Isomorphism [Hom ─,c] F) _) .
proof: Proof. unshelve econstructor. - unshelve econstructor. + intros [elt yoneda_is_iso]. unshelve econstructor. * exact (from (Yoneda_Lemma C F c) elt). * exact (from (IsIsoToIso _ yoneda_is_iso)). * apply is_right_inverse. * apply is_left_inverse. + abstract(intros [eltx x_is_iso] [elty y_is_iso] eltx_eq_elty; simpl in eltx_eq_elty; apply to_equiv_implies_iso_equiv; simpl; intros; rewrite eltx_eq_elty; reflexivity). - unshelve econstructor. + simpl. intro X; simpl in X. destruct X as [Xto Xfrom tofromid fromtoid]; simpl in *. exists (morphism (to (Yoneda_Lemma C F c)) Xto). simpl. unshelve econstructor. * exact Xfrom. * abstract(simpl; intros; rewrite <- tofromid; symmetry; apply preyoneda). * abstract(simpl; intros; rewrite <- preyoneda; apply fromtoid). + abstract(intros x y eq; simpl; destruct eq as [e ?]; simpl in e; apply e). - abstract(unshelve econstructor; simpl; intros ? ?; [ symmetry; apply preyoneda | reflexivity ] ). - abstract(simpl; intros [x f]; simpl; set (k := @fmap_id _ _ F); simpl in k; apply k). Defined.
imports: Category.Lib Category.Lib.Tactics2 Category.Theory.Category Category.Theory.Isomorphism Category.Construction.Opposite Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Hom Category.Functor.Hom.Yoneda Category.Instance.Sets Category.Construction.Groupoid