Add category of subobjects.

agda · Aug 17, 2023 · bb35d73 · bb35d73
1 parent 14b2c23
commit bb35d73
Showing 1 changed file with 35 additions and 0 deletions.
diff --git a/Cubical/Categories/Constructions/SubObject.agda b/Cubical/Categories/Constructions/SubObject.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --safe #-}
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Powerset
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Morphism
+
+open Category
+
+module Cubical.Categories.Constructions.SubObject
+  {ℓ ℓ' : Level}
+  (C : Category ℓ ℓ')
+  (c : C .ob)
+  where
+
+open import Cubical.Categories.Constructions.Slice C c
+
+isSubObj : ℙ (SliceCat .ob)
+isSubObj (sliceob arr) = isMonic C arr , isPropIsMonic C arr
+
+SubObjCat : Category (ℓ-max ℓ ℓ') ℓ'
+SubObjCat = ΣPropCat SliceCat isSubObj
+
+SubObjCat→SliceCat : Functor SubObjCat SliceCat
+SubObjCat→SliceCat = forgetΣPropCat SliceCat isSubObj
+
+subObjMorIsMonic : {s t : SubObjCat .ob} (f : SubObjCat [ s , t ])
+  → isMonic C (S-hom f)
+subObjMorIsMonic {s = s} {t = t} f = postcompCreatesMonic C
+  (S-hom f) (S-arr (t .fst)) comp-is-monic
+  where comp-is-monic = subst (isMonic C) (sym (S-comm f)) (s .snd)