Theorem SubObj_Functor_isfunctor : is_functor (SubObj_Functor_data). 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.
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.