proposition: Theorem Terminal_Limit (C : Category) (F : 0 ⟶ C) : Limit F ↔ @Terminal C.
proof: Proof. split; intros. - construct. + exact (vertex_obj[X]). + given (cone : Cone F). { unshelve (refine {| vertex_obj := x |}); unshelve econstructor; intros. - inversion x0. - inversion x0. } destruct (@ump_limits _ _ _ X cone). apply unique_obj. + given (cone : Cone F). { unshelve (refine {| vertex_obj := x |}); unshelve econstructor; intros. - inversion x0. - inversion x0. } destruct (@ump_limits _ _ _ X cone). pose proof (uniqueness f). pose proof (uniqueness g). rewrite <- X0, <- X1. * reflexivity. * intro x0; inversion x0. * intro x0; inversion x0. - construct. + construct; [ | unshelve econstructor ]. * exact terminal_obj. * inversion x. * inversion x. + simpl. unshelve eexists. * exact one. * intros. inversion x. * intros. apply one_unique. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Structure.Cone Category.Structure.Limit Category.Structure.Terminal Category.Instance.Zero