Definition PullbackSubObj (PB : Pullbacks C) {c : C} (S : SubObj c) {c' : C} (h : C⟦c', c⟧) : SubObj c'. Proof. use (setquotfun (z_iso_eqrel (C:=Subobjectscategory c))). + intro s. use (PullbackSubobject PB s h). + intros u v. use hinhfun. intro uv. use make_z_iso_in_Subobjectscategory. - use (iso_between_pullbacks (PullbackSqrCommutes (PB _ _ _ h (Subobject_mor u))) (PullbackSqrCommutes (PB _ _ _ h (Subobject_mor v))) (isPullback_Pullback (PB _ _ _ h (Subobject_mor u))) (isPullback_Pullback (PB _ _ _ h (Subobject_mor v))) ). * exact (identity_z_iso c'). * use z_iso_from_z_iso_in_Subobjectcategory. exact uv. * exact (identity_z_iso c). * rewrite id_left, id_right. apply idpath. * rewrite id_right. apply pathsinv0. use Subobjectmor_tri. - use z_iso_is_z_isomorphism. - rewrite <-(id_right (Subobject_mor _)). use pathsinv0. use PullbackArrow_PullbackPr1. + exact S. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.opp_precat.