open import Cat.Univalent
open import Cat.Prelude

open import Order.Base

import Cat.Reasoning

module Order.Instances.Subobjects where


Posets of subobjectsπ

Let $\mathcal{C}$ be a category and $A : \mathcal{C}$ an arbitrary object. Weβre interested here in the restriction of the slice category $\mathcal{C}/A$ to those objects whose map is a monomorphism. This restriction turns out to be a poset.

module _ {o β} (C : Precategory o β) (c-cat : is-category C) where
private module C = Cat.Reasoning C
open C._βͺ_


Hereβs why: First, we define the $\le$ relation βas usualβ, i.e., $X \le Y$ consists of the commuting triangles as in the diagram below.

  Subobjects : C.Ob β Poset _ _
Subobjects A = to-poset (Ξ£ C.Ob Ξ» B β B C.βͺ A) mk where
open make-poset

mk : make-poset β (Ξ£ (C .Precategory.Ob) (Ξ» B β B C.βͺ A))
mk .rel (B , f) (C , h) = Ξ£ (C.Hom B C) Ξ» g β h .mor C.β g β‘ f .mor
mk .id = C.id , C.idr _
mk .trans (f , Ξ±) (g , Ξ²) = g C.β f , C.pulll Ξ² β Ξ±


The first thing we must verify is that this is indeed a proposition: there is at most one such triangle. Why? Well, $Y$ is a monomorphism! Suppose we have $f, f' : B \to C$ as in the diagram. Then we have $Yf = g = Yf'$, so $f = f'$.

    mk .thin {y = y} (f , Ξ±) (g , Ξ²) = Ξ£-prop-path! (y .snd .monic _ _ (Ξ± β sym Ξ²))


Now, itβs certainly not the case that you can get an isomorphism $A \cong B$ from any olβ pair of morphisms $f : A \to B$ and $g : B \to A$. But if weβre talking morphisms in a slice between monomorphisms, then we have a much better shot: Instead of having to show $fg = \mathrm{id}_{}$ (hard), we can show $Yfg = Y$, which follows from commutativity of the triangles. So the subjects of $A$ are a poset!

    mk .antisym {X , x} {Y , y} (f , Ξ±) (g , Ξ²) =
Ξ£-pathp (c-cat .to-path im) (C.βͺ-pathp (Univalent.Hom-pathp-refll-iso c-cat Ξ²))
where
im : X C.β Y
im = C.make-iso f g (y .monic _ _ (C.pulll Ξ± Β·Β· Ξ² Β·Β· C.intror refl))
(x .monic _ _ (C.pulll Ξ² Β·Β· Ξ± Β·Β· C.intror refl))