Lemma initial_in_full_subcategory {C : category} (C' : hsubtype (ob C)) (IC : Initial C) (IC' : C' (InitialObject IC)) : Initial (full_sub_precategory C'). Proof. use tpair. - use precategory_object_in_subcat. + exact (InitialObject IC). + assumption. - cbn. intros X. use make_iscontr. + use morphism_in_full_subcat. apply InitialArrow. + intro; apply eq_in_sub_precategory; cbn. apply InitialArrowUnique. 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.