Definition cone_in_full_subcategory {C : category} {g : graph} (C' : hsubtype (ob C)) {d : diagram g (full_sub_precategory C')} (c : ob C) (tip : C' c) : cone (lift_diagram_full_subcategory d) c ≃ cone d (c,, tip). Proof. unfold cone. use weqbandf. - apply weqonsecfibers; intros x. cbn beta. apply (@weq_hom_in_subcat_from_hom_in_precat C C' (c,, tip) (dob d x)). - intro legs. cbn beta. apply weqonsecfibers; intros u; apply weqonsecfibers; intros v; apply weqonsecfibers; intros e. cbn. apply invweq. refine (subtypeInjectivity _ _ _ _). intro; apply propproperty. Defined.
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.