Library UniMath.CategoryTheory.Quotobjects

Quotobjects


Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.CategoryTheory.Core.Categories.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.UnderCategories.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Subcategory.Core.

Require Import UniMath.CategoryTheory.limits.pushouts.

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 : C⟦c, 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 : C⟦c, c'⟧) :
    Quotobjectscategory c'.
  Proof.
    set (po := hpo _ _ _ h (pr1 (pr2 Q))).
    use Quotobjectscategory_ob.
    - exact po.
    - exact (limits.pushouts.PushoutIn1 po).
    - use EpiPushoutisEpi'.
  Defined.

End def_quotobjects.