Library UniMath.CategoryTheory.Subobjects
*************************************************************************
Definition and theory about subobjects of an object c
Contents:
Written by: Tomi Pannila and Anders Mörtberg, 2016-2017
- Category of subobjects (monos) of c (Subobjectscategory)
- Set of subobjects as equivalence classes of monos (SubObj)
- Proof that the set of subobjects of an object is a poset (SubObjPoset)
- The definition of the functor from C^op to hset_category which maps c to the set of the subobject (module z_isomorphism) of c and maps morphism "by pullback" (SubObj_Functor)
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.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.
Local Open Scope cat.
Section def_subobjects.
Context {C : category}.
Definition Subobjectscategory (c : C) : category :=
slice_cat (subcategory_of_monics C)
(subprecategory_of_monics_ob C c).
Lemma has_homsets_Subobjectscategory (c : C) :
has_homsets (Subobjectscategory c).
Show proof.
Context {C : category}.
Definition Subobjectscategory (c : C) : category :=
slice_cat (subcategory_of_monics C)
(subprecategory_of_monics_ob C c).
Lemma has_homsets_Subobjectscategory (c : C) :
has_homsets (Subobjectscategory c).
Show proof.
Construction of a subobject from a monic
Definition Subobjectscategory_ob {c c' : C} (h : C⟦c', c⟧) (isM : isMonic h) :
Subobjectscategory c := (subprecategory_of_monics_ob C c',,(h,,isM)).
Subobjectscategory c := (subprecategory_of_monics_ob C c',,(h,,isM)).
Accessor for an object of Subobjectscategory
Section obAccessor.
Context {c:C} (S : Subobjectscategory c).
Definition Subobject_dom : C := pr1 (pr1 S).
Definition Subobject_Monic := pr2 S.
Definition Subobject_mor : C⟦ Subobject_dom , c ⟧ := pr1 (pr2 S).
Definition Subobject_isM : isMonic(Subobject_mor) := pr2 (pr2 S).
End obAccessor.
Context {c:C} (S : Subobjectscategory c).
Definition Subobject_dom : C := pr1 (pr1 S).
Definition Subobject_Monic := pr2 S.
Definition Subobject_mor : C⟦ Subobject_dom , c ⟧ := pr1 (pr2 S).
Definition Subobject_isM : isMonic(Subobject_mor) := pr2 (pr2 S).
End obAccessor.
Accessor for a morphism of Subobjectscategory
Section morAccessor.
Context {c:C} {S S' : Subobjectscategory c} (h : S --> S').
Definition Subobjectmor_Cmor : C⟦ Subobject_dom S, Subobject_dom S' ⟧ := pr1 (pr1 h).
Definition Subobjectmor_isM : isMonic(Subobjectmor_Cmor) := pr2 (pr1 h).
Definition Subobjectmor_tri := maponpaths (pr1) (pr2 h).
End morAccessor.
Context {c:C} {S S' : Subobjectscategory c} (h : S --> S').
Definition Subobjectmor_Cmor : C⟦ Subobject_dom S, Subobject_dom S' ⟧ := pr1 (pr1 h).
Definition Subobjectmor_isM : isMonic(Subobjectmor_Cmor) := pr2 (pr1 h).
Definition Subobjectmor_tri := maponpaths (pr1) (pr2 h).
End morAccessor.
Given any subobject S of c and a morphism h : c' -> c, by taking then pullback of S by h we
obtain a subobject of c'.
Definition PullbackSubobject (PB : Pullbacks C) {c : C} (S : Subobjectscategory c) {c' : C} (h : C⟦c', c⟧) :
Subobjectscategory c'.
Show proof.
Definition make_z_iso_in_Subobjectscategory {c : C} {S S' : Subobjectscategory c}
(h : C ⟦Subobject_dom S ,Subobject_dom S'⟧)
(is_z_iso : is_z_isomorphism h)
(tri : Subobject_mor S = h · Subobject_mor S')
: z_iso S S'.
Show proof.
Subobjectscategory c'.
Show proof.
set (pb := PB _ _ _ h (Subobject_mor S)).
use Subobjectscategory_ob.
- exact pb.
- exact (PullbackPr1 pb).
- use MonicPullbackisMonic'.
use Subobjectscategory_ob.
- exact pb.
- exact (PullbackPr1 pb).
- use MonicPullbackisMonic'.
Definition make_z_iso_in_Subobjectscategory {c : C} {S S' : Subobjectscategory c}
(h : C ⟦Subobject_dom S ,Subobject_dom S'⟧)
(is_z_iso : is_z_isomorphism h)
(tri : Subobject_mor S = h · Subobject_mor S')
: z_iso S S'.
Show proof.
use make_z_iso'.
+ use tpair.
- use precategory_morphisms_in_subcat.
* exact h.
* use is_iso_isMonic.
exact is_z_iso.
- use eq_in_sub_precategory.
exact tri.
+ use z_iso_to_slice_precat_z_iso.
use is_z_iso_in_subcategory_of_monics_weq.
exact is_z_iso.
+ use tpair.
- use precategory_morphisms_in_subcat.
* exact h.
* use is_iso_isMonic.
exact is_z_iso.
- use eq_in_sub_precategory.
exact tri.
+ use z_iso_to_slice_precat_z_iso.
use is_z_iso_in_subcategory_of_monics_weq.
exact is_z_iso.
a z_iso is Subobjectcategory gives, in particular, a z_iso of C between domains
Definition z_iso_from_z_iso_in_Subobjectcategory {c : C}
{S S' : Subobjectscategory c} (h : z_iso S S')
: (z_iso (Subobject_dom S) (Subobject_dom S')).
Show proof.
End def_subobjects.
{S S' : Subobjectscategory c} (h : z_iso S S')
: (z_iso (Subobject_dom S) (Subobject_dom S')).
Show proof.
use make_z_iso.
+ exact (Subobjectmor_Cmor h).
+ exact (Subobjectmor_Cmor (inv_from_z_iso h)).
+ induction h as (h, (g,(hg,gh))).
use make_is_inverse_in_precat.
- exact (maponpaths Subobjectmor_Cmor hg).
- exact (maponpaths Subobjectmor_Cmor gh).
+ exact (Subobjectmor_Cmor h).
+ exact (Subobjectmor_Cmor (inv_from_z_iso h)).
+ induction h as (h, (g,(hg,gh))).
use make_is_inverse_in_precat.
- exact (maponpaths Subobjectmor_Cmor hg).
- exact (maponpaths Subobjectmor_Cmor gh).
End def_subobjects.
Equivalence classes of subobjects defined by identifying monos into c
with isomorphic source
Definition SubObj (c : C) : hSet :=
make_hSet (setquot (z_iso_eqrel (C:=Subobjectscategory c))) (isasetsetquot _).
Definition SubObj_iseqc {c:C} (S : SubObj c) := pr2 S.
Definition PullbackSubObj (PB : Pullbacks C) {c : C} (S : SubObj c)
{c' : C} (h : C⟦c', c⟧)
: SubObj c'.
Show proof.
Definition monorel (c : C) : hrel (Subobjectscategory c) :=
λ f g, ∃ h, pr1 (pr2 f) = h · pr1 (pr2 g).
Lemma isrefl_monorel (c : C) : isrefl (monorel c).
Show proof.
Lemma istrans_monorel (c : C) : istrans (monorel c).
Show proof.
Lemma ispreorder_monorel c : ispreorder (monorel c).
Show proof.
Lemma are_z_isomorphic_monorel {c : C} {x1 y1 x2 y2 : Subobjectscategory c}
(h1 : are_z_isomorphic x1 y1) (h2 : are_z_isomorphic x2 y2) :
monorel c x1 x2 → monorel c y1 y2.
Show proof.
make_hSet (setquot (z_iso_eqrel (C:=Subobjectscategory c))) (isasetsetquot _).
Definition SubObj_iseqc {c:C} (S : SubObj c) := pr2 S.
Definition PullbackSubObj (PB : Pullbacks C) {c : C} (S : SubObj c)
{c' : C} (h : C⟦c', c⟧)
: SubObj c'.
Show 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.
+ 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.
Definition monorel (c : C) : hrel (Subobjectscategory c) :=
λ f g, ∃ h, pr1 (pr2 f) = h · pr1 (pr2 g).
Lemma isrefl_monorel (c : C) : isrefl (monorel c).
Show proof.
Lemma istrans_monorel (c : C) : istrans (monorel c).
Show proof.
intros x y z h1.
apply hinhuniv; intros h2; generalize h1; clear h1.
apply hinhuniv; intros h1; apply hinhpr.
exists (pr1 h1 · pr1 h2).
now rewrite <- assoc, <- (pr2 h2), <- (pr2 h1).
apply hinhuniv; intros h2; generalize h1; clear h1.
apply hinhuniv; intros h1; apply hinhpr.
exists (pr1 h1 · pr1 h2).
now rewrite <- assoc, <- (pr2 h2), <- (pr2 h1).
Lemma ispreorder_monorel c : ispreorder (monorel c).
Show proof.
Lemma are_z_isomorphic_monorel {c : C} {x1 y1 x2 y2 : Subobjectscategory c}
(h1 : are_z_isomorphic x1 y1) (h2 : are_z_isomorphic x2 y2) :
monorel c x1 x2 → monorel c y1 y2.
Show proof.
apply hinhuniv; intros f.
change (ishinh_UU (z_iso x1 y1)) in h1.
change (ishinh_UU (z_iso x2 y2)) in h2.
apply h1; clear h1; intro h1.
apply h2; clear h2; intro h2.
intros P H; apply H; clear P H.
set (h1_inv := inv_from_z_iso h1).
set (Hh1 := z_iso_after_z_iso_inv h1).
exists (pr1 (pr1 h1_inv) · pr1 f · pr1 (pr1 (pr1 h2))).
set (Htemp := maponpaths pr1 (pr2 (pr1 h2))).
apply pathsinv0; simpl in *.
rewrite <-!assoc, <- Htemp.
intermediate_path (pr1 (pr1 h1_inv) · pr1 (pr2 x1)).
{ apply maponpaths, pathsinv0, (pr2 f). }
etrans; [ apply maponpaths, (maponpaths pr1 (pr2 (pr1 h1))) |]; simpl.
rewrite assoc.
etrans; [ eapply cancel_postcomposition, (maponpaths pr1 (maponpaths pr1 Hh1)) |].
apply id_left.
change (ishinh_UU (z_iso x1 y1)) in h1.
change (ishinh_UU (z_iso x2 y2)) in h2.
apply h1; clear h1; intro h1.
apply h2; clear h2; intro h2.
intros P H; apply H; clear P H.
set (h1_inv := inv_from_z_iso h1).
set (Hh1 := z_iso_after_z_iso_inv h1).
exists (pr1 (pr1 h1_inv) · pr1 f · pr1 (pr1 (pr1 h2))).
set (Htemp := maponpaths pr1 (pr2 (pr1 h2))).
apply pathsinv0; simpl in *.
rewrite <-!assoc, <- Htemp.
intermediate_path (pr1 (pr1 h1_inv) · pr1 (pr2 x1)).
{ apply maponpaths, pathsinv0, (pr2 f). }
etrans; [ apply maponpaths, (maponpaths pr1 (pr2 (pr1 h1))) |]; simpl.
rewrite assoc.
etrans; [ eapply cancel_postcomposition, (maponpaths pr1 (maponpaths pr1 Hh1)) |].
apply id_left.
Construct a quotient relation on the Subobjects from the relation on monos
Definition SubObj_rel (c : C) : hrel (pr1 (SubObj c)).
Show proof.
Lemma istrans_SubObj_rel (c : C) : istrans (SubObj_rel c).
Show proof.
Lemma isrefl_SubObj_rel (c : C) : isrefl (SubObj_rel c).
Show proof.
Lemma ispreorder_SubObj_rel (c : C) : ispreorder (SubObj_rel c).
Show proof.
Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c).
Show proof.
Definition SubObjPoset (c : C) : Poset :=
(SubObj c,,SubObj_rel c,,ispreorder_SubObj_rel c,,isantisymm_SubObj_rel c).
End subobj.
Section SubObj_functor.
Context (C : category) (PB : Pullbacks C).
Definition SubObj_Functor_data : functor_data (op_cat C) hset_category.
Show proof.
Theorem SubObj_Functor_isfunctor : is_functor (SubObj_Functor_data).
Show proof.
Definition SubObj_Functor : C^op ⟶ hset_category.
Show proof.
End SubObj_functor.
Show proof.
use quotrel.
- apply monorel.
- intros x1 y1 x2 y2 h1 h2.
apply hPropUnivalence.
+ apply (are_z_isomorphic_monorel h1 h2).
+ apply (are_z_isomorphic_monorel (eqrelsymm (z_iso_eqrel) _ _ h1)
(eqrelsymm (z_iso_eqrel) _ _ h2)).
- apply monorel.
- intros x1 y1 x2 y2 h1 h2.
apply hPropUnivalence.
+ apply (are_z_isomorphic_monorel h1 h2).
+ apply (are_z_isomorphic_monorel (eqrelsymm (z_iso_eqrel) _ _ h1)
(eqrelsymm (z_iso_eqrel) _ _ h2)).
Lemma istrans_SubObj_rel (c : C) : istrans (SubObj_rel c).
Show proof.
Lemma isrefl_SubObj_rel (c : C) : isrefl (SubObj_rel c).
Show proof.
Lemma ispreorder_SubObj_rel (c : C) : ispreorder (SubObj_rel c).
Show proof.
Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c).
Show proof.
unfold isantisymm; simpl.
assert (int : ∏ x1 x2, isaprop (SubObj_rel c x1 x2 → SubObj_rel c x2 x1 -> x1 = x2)).
{ intros x1 x2.
repeat (apply impred; intro).
apply (isasetsetquot _ x1 x2).
}
apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))).
intros x y h1 h2.
simpl in *. apply (iscompsetquotpr (z_iso_eqrel (C:=Subobjectscategory c))).
generalize h1; clear h1; apply hinhuniv; intros [h1 Hh1].
generalize h2; clear h2; apply hinhuniv; intros [h2 Hh2].
apply hinhpr, (invmap (weq_z_iso _ (subprecategory_of_monics_ob C c) _ _)).
induction x as [[x []] [fx Hfx]].
induction y as [[y []] [fy Hfy]].
simpl in *.
assert (mon_h1 : isMonic h1).
{ apply (isMonic_postcomp _ h1 fy); rewrite <- Hh1; apply Hfx. }
assert (mon_h2 : isMonic h2).
{ apply (isMonic_postcomp _ h2 fx); rewrite <- Hh2; apply Hfy. }
use tpair.
- exists (h1,,mon_h1).
exists (h2,,mon_h2).
split; apply subtypePath.
+ intros xx. apply isapropisMonic.
+ simpl; apply Hfx.
now rewrite <- assoc, <- Hh2, <- Hh1, id_left.
+ intros xx. apply isapropisMonic.
+ simpl; apply Hfy.
now rewrite <- assoc, <- Hh1, <- Hh2, id_left.
- apply subtypePath; simpl; try apply Hh1.
now intros xx; apply isapropisMonic.
assert (int : ∏ x1 x2, isaprop (SubObj_rel c x1 x2 → SubObj_rel c x2 x1 -> x1 = x2)).
{ intros x1 x2.
repeat (apply impred; intro).
apply (isasetsetquot _ x1 x2).
}
apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))).
intros x y h1 h2.
simpl in *. apply (iscompsetquotpr (z_iso_eqrel (C:=Subobjectscategory c))).
generalize h1; clear h1; apply hinhuniv; intros [h1 Hh1].
generalize h2; clear h2; apply hinhuniv; intros [h2 Hh2].
apply hinhpr, (invmap (weq_z_iso _ (subprecategory_of_monics_ob C c) _ _)).
induction x as [[x []] [fx Hfx]].
induction y as [[y []] [fy Hfy]].
simpl in *.
assert (mon_h1 : isMonic h1).
{ apply (isMonic_postcomp _ h1 fy); rewrite <- Hh1; apply Hfx. }
assert (mon_h2 : isMonic h2).
{ apply (isMonic_postcomp _ h2 fx); rewrite <- Hh2; apply Hfy. }
use tpair.
- exists (h1,,mon_h1).
exists (h2,,mon_h2).
split; apply subtypePath.
+ intros xx. apply isapropisMonic.
+ simpl; apply Hfx.
now rewrite <- assoc, <- Hh2, <- Hh1, id_left.
+ intros xx. apply isapropisMonic.
+ simpl; apply Hfy.
now rewrite <- assoc, <- Hh1, <- Hh2, id_left.
- apply subtypePath; simpl; try apply Hh1.
now intros xx; apply isapropisMonic.
Definition SubObjPoset (c : C) : Poset :=
(SubObj c,,SubObj_rel c,,ispreorder_SubObj_rel c,,isantisymm_SubObj_rel c).
End subobj.
Section SubObj_functor.
Context (C : category) (PB : Pullbacks C).
Definition SubObj_Functor_data : functor_data (op_cat C) hset_category.
Show proof.
use make_functor_data.
+ intro c.
cbn in c.
exact (SubObj c).
+ intros c c' f Sm.
use PullbackSubObj.
- exact PB.
- exact c.
- exact Sm.
- exact f.
+ intro c.
cbn in c.
exact (SubObj c).
+ intros c c' f Sm.
use PullbackSubObj.
- exact PB.
- exact c.
- exact Sm.
- exact f.
Theorem SubObj_Functor_isfunctor : is_functor (SubObj_Functor_data).
Show 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).
+ 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).
Definition SubObj_Functor : C^op ⟶ hset_category.
Show proof.
End SubObj_functor.