Definition lift_diagram_full_subcategory {C : category} {C' : hsubtype (ob C)} {g : graph} (d : diagram g (full_sub_precategory C')) : diagram g C. Proof. use tpair. - intros v. apply (precategory_object_from_sub_precategory_object _ (full_sub_precategory C')). exact (dob d v). - intros u v e. apply (precategory_morphism_from_sub_precategory_morphism _ (full_sub_precategory C')). exact (dmor d e). 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.