Library UniMath.CategoryTheory.Quotobjects


Definition of quotient objects

Section def_quotobjects.

  Variable C : precategory.
  Hypothesis hs : has_homsets C.

  Definition Quotobjectscategory (c : C) : UU :=
    Undercategory (subprecategory_of_epis C hs)
                     (has_homsets_subprecategory_of_epis C hs)
                     (subprecategory_of_epis_ob C hs c).

Construction of a quotient object from an epi
  Definition Quotobjectscategory_ob {c c' : C} (h : Cc, c') (isE : isEpi h) :
    Quotobjectscategory c := tpair _ (subprecategory_of_epis_ob C hs c') (tpair _ h isE).

  Hypothesis hpo : @Pushouts C.

Given any quotient object Q of c and a morphism h : c -> c', by taking then pushout of Q by h we obtain a quotient object of c'.
  Definition PushoutQuotobject {c : C} (Q : Quotobjectscategory c) {c' : C} (h : Cc, c') :
    Quotobjectscategory c'.
    set (po := hpo _ _ _ h (pr1 (pr2 Q))).
    use Quotobjectscategory_ob.
    - exact po.
    - exact (limits.pushouts.PushoutIn1 po).
    - use EpiPushoutisEpi'.

End def_quotobjects.