proposition: Proposition cone_equiv_to_morphism_equiv (c z : C) (H : IsALimit F z) (f g : c ~> z) : (forall a : J, vertex_map limit_acone a ∘ f ≈ vertex_map limit_acone a ∘ g) -> f ≈ g.
proof: Proof. intro e. set (C' := fmap[ConePresheaf F] f limit_acone). assert (A: (unique_obj (ump_limit {| vertex_obj := c ; coneFrom := C' |})) ≈ f) by (apply uniqueness; reflexivity). rewrite <- A. set (C'' := fmap[ConePresheaf F] g limit_acone). apply uniqueness. intro. simpl. symmetry. trivial. Qed.
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.Instance.Sets Category.Structure.UniversalProperty Category.Structure.Cone Category.Structure.Limit Category.Functor.Hom.Yoneda