proposition: Theorem SubObj_Functor_isfunctor : is_functor (SubObj_Functor_data).
proof: Proof. split. + intro c. cbn in c. use funextfun. intro S. change (pr1hSet (SubObj c)) in S. use (squash_to_prop (X:=pr1setquot _ S)). { exact (eqax0 (SubObj_iseqc S)). } { use isasetsetquot. } intro m. induction (setquotl0 _ S m). cbn. use (weqpathsinsetquot (z_iso_eqrel (C:=Subobjectscategory c))). use hinhpr. use make_z_iso_in_Subobjectscategory. - use PullbackPr2. - use Pullback_of_z_iso'. exact (identity_is_z_iso c). - cbn. rewrite <- PullbackSqrCommutes, id_right. apply idpath. + intros c c' c'' f f'. cbn in c, c', c'', f, f'. use funextfun. intro S. use (squash_to_prop (X:=pr1setquot _ S)). { exact (eqax0 (SubObj_iseqc S)). } { use isasetsetquot. } intro m. induction (setquotl0 _ S m). use weqpathsinsetquot. use hinhpr. induction m as (m,Sm). cbn. set (pb := (PB _ _ _ f ((Subobject_mor m)))). set (pbpb := PB _ _ _ f' (PullbackPr1 pb)). transparent assert (pb_glued : (Pullback (f'·f) (Subobject_mor m))). { use make_Pullback. - exact pbpb. - exact (PullbackPr1 pbpb). - exact ((PullbackPr2 pbpb)·(PullbackPr2 pb)). - use glueSquares. * exact (PullbackPr1 pb). * use PullbackSqrCommutes. * use PullbackSqrCommutes. - use (isPullbackGluedSquare (isPullback_Pullback pb) (isPullback_Pullback pbpb)). } use make_z_iso_in_Subobjectscategory. - cbn. fold pb. fold pbpb. assert (H : PullbackObject pb_glued = PullbackObject pbpb). { apply idpath. } induction H. use z_iso_from_Pullback_to_Pullback. - use z_iso_is_z_isomorphism. - cbn. fold pb. fold pbpb. assert (H : PullbackPr1 pb_glued = PullbackPr1 pbpb). { apply idpath. } induction H. apply pathsinv0. use (PullbackArrow_PullbackPr1 pb_glued). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.opp_precat