proposition: 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: 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.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits