proposition: Proposition LimitIsUniversalProperty : IsUniversalProperty C^op (fun c => IsALimit F c) (fun c => @LimitSetoid J C F c).
proof: Proof. exists (@ConePresheaf J C F); intro c. repeat(unshelve econstructor; try intros); simpl in *. - auto with cat limit. - abstract(auto with cat limit). - abstract(auto with cat). - abstract(auto with cat). - abstract(auto with cat). - auto with limit. - abstract(intros f g a; apply uniqueness; auto with limit). - abstract(auto with cat limit). - abstract(auto with cat limit). - abstract(auto with cat limit). - abstract(auto with cat limit). - abstract(auto with cat limit). - intros x1 x2. apply_cone_equiv_to_morphism_equiv. intro. autorewrite with limit. rewrite <- X. now autorewrite with limit. - destruct X; apply to; exact id. - abstract(auto with cat limit). - destruct N; now apply X. - abstract(destruct X as [[X_to_transform X_to_nat ?] [X_from_transform X_from_nat ?] iso_to_from ?]; simpl in *; rewrite X_to_nat; revert x; change _ with (X_to_transform vertex_obj[N] (id{C} ∘ X_from_transform vertex_obj[N] coneFrom) ≈ (@coneFrom _ _ _ N)); rewrite (proper_morphism (X_to_transform vertex_obj[N]) _ _(id_left (X_from_transform vertex_obj[N] coneFrom))); intro j; now rewrite (iso_to_from N (@coneFrom _ _ _ N) j), id_right). - abstract(destruct X as [[X_to_transform X_to_nat ?] [X_from_transform X_from_nat ?] ? ?]; simpl in *; set (k:= X_from_nat _ _ v (X_to_transform c id{C})); symmetry in k; rewrite iso_from_to, 2 id_left in k; rewrite <- k; apply (proper_morphism (X_from_transform vertex_obj[N])); simpl; intro j; symmetry; apply X0). - abstract(simpl; intros a b eq; destruct a, b as [to1 from1 tofrom1 fromto1]; destruct eq as [eql eqr]; simpl in *; apply eql). - abstract(intros a f j; destruct x, to; simpl in *; rewrite naturality; revert j; change _ with (transform a (id{C} ∘ f) ≈ transform a f); now rewrite id_left). - abstract(now unfold ump_limit_construct). - abstract(auto with cat limit). 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.Instance.Sets Category.Structure.UniversalProperty Category.Structure.Cone Category.Structure.Limit Category.Functor.Hom.Yoneda