open import Cat.Prelude
open import Cat.Univalent

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.

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))