Lemma terminal_in_full_subcategory {C : category} (C' : hsubtype (ob C)) (TC : Terminal C) (TC' : C' (TerminalObject TC)) : Terminal (full_sub_precategory C'). Proof. use tpair. - use precategory_object_in_subcat. + exact (TerminalObject TC). + assumption. - cbn. intros X. use make_iscontr. + use morphism_in_full_subcat. apply TerminalArrow. + intro; apply eq_in_sub_precategory; cbn. apply TerminalArrowUnique. 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.