Library UniMath.CategoryTheory.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.
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).
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.
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'.
Show proof.
End def_quotobjects.
Quotobjectscategory c'.
Show proof.
set (po := hpo _ _ _ h (pr1 (pr2 Q))).
use Quotobjectscategory_ob.
- exact po.
- exact (limits.pushouts.PushoutIn1 po).
- use EpiPushoutisEpi'.
use Quotobjectscategory_ob.
- exact po.
- exact (limits.pushouts.PushoutIn1 po).
- use EpiPushoutisEpi'.
End def_quotobjects.