Definition and theory about subobjects of an object c Contents: - 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]) Written by: Tomi Pannila and Anders Mörtberg, 2016-2017 *****************************************************************************) Require Import UniMath.
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.