Lemma lim_cone_in_full_subcategory {C : category} (C' : hsubtype (ob C)) {g : graph} {d : diagram g (full_sub_precategory C')} (LC : Lims_of_shape g C) : C' (lim (LC (lift_diagram_full_subcategory d))) -> LimCone d. Proof. intro. pose (Z := LC (lift_diagram_full_subcategory d)). unfold LimCone. use tpair. - use tpair. + use precategory_object_in_subcat. * eapply lim; eassumption. * assumption. + apply cone_in_full_subcategory, limCone. - apply (reflects_all_limits_sub_precategory_inclusion C' g d). apply (pr2 Z). Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.