module Cat.Displayed.Instances.Subobjects
  {o ℓ} (B : Precategory o ℓ)

The fibration of subobjects🔗

Given a base category B\mathcal{B}, we can define the displayed category of subobjects over B\mathcal{B}. This is, in essence, a restriction of the codomain fibration of B\mathcal{B}, but with our attention restricted to the monomorphisms a↪ba \hookrightarrow b rather than arbitrary maps a→ba \to b.

record Subobject (y : Ob) : Type (o ⊔ ℓ) where
    {domain} : Ob
    map   : Hom domain y
    monic : is-monic map

open Subobject public

To make formalisation smoother, we define our own version of displayed morphisms in the subobject fibration, rather than reusing those of the fundamental self-indexing. The reason for this is quite technical: the type of maps in the self-indexing is only dependent (the domains and) the morphisms being considered, meaning nothing constrains the proofs that these are monomorphisms, causing unification to fail at the determining the full Subobjects involved.

record ≤-over {x y} (f : Hom x y) (a : Subobject x) (b : Subobject y) : Type ℓ where
    map : Hom (a .domain) (b .domain)
    sq : f ∘ a ≡ b ∘ map

open ≤-over public

We will denote the type of maps x′→fy′x' \to_f y' in the subobject fibration by x′≤fy′x' \le_f y', since there is at most one such map: if g,hg, h satisfy y′g=fx′=y′hy'g = fx' = y'h, then, since y′y' is a mono, g=hg = h.

Setting up the displayed category is now nothing more than routine verification: the identity map satisfies id⁡a=aid⁡\operatorname{id}_{} a = a \operatorname{id}_{}, and commutative squares can be pasted together.

Subobjects : Displayed B (o ⊔ ℓ) ℓ
Subobjects .Ob[_] y = Subobject y
Subobjects .Hom[_]  = ≤-over
Subobjects .Hom[_]-set f a b = is-prop→is-set ≤-over-is-prop

Subobjects .id' .map = id
Subobjects .id' .sq  = id-comm-sym

Subobjects ._∘'_ α β .map = α .map ∘ β .map
Subobjects ._∘'_ α β .sq  = pullr (β .sq) ∙ extendl (α .sq)

As a fibration🔗

By exactly the same construction as for the fundamental self-indexing, if B\mathcal{B} has pullbacks, the displayed category we have built is actually a fibration. The construction is slightly simpler now that we have no need to worry about uniqueness, but we can remind ourselves of the universal property:

On the first stage, we are given the data in black: we can complete an open span y′↪y←fxy' \hookrightarrow y \xleftarrow{f} x to a Cartesian square (in blue) by pulling y′y' back along ff; this base change remains a monomorphism. Now given the data in red, we verify that the dashed arrow exists, which is enough for its uniqueness.

  : has-pullbacks B
  → Cartesian-fibration Subobjects
Subobject-fibration pb .has-lift f y' = l where
  it : Pullback _ _ _
  it = pb (y' .map) f
  l : Cartesian-lift Subobjects f y'

  -- The blue square:
  l .x' .domain = it .apex
  l .x' .map    = it .p₂
  l .x' .monic  = is-monic→pullback-is-monic (y' .monic) (it .has-is-pb)
  l .lifting .map = it .p₁
  l .lifting .sq  = sym (it .square)

  -- The dashed red arrow:
  l .cartesian .universal {u' = u'} m h' = λ where
    .map → it .Pullback.universal (sym (h' .sq) ∙ sym (assoc f m (u' .map)))
    .sq  → sym (it .p₂∘universal)
  l .cartesian .commutes _ _ = ≤-over-is-prop _ _
  l .cartesian .unique _ _   = ≤-over-is-prop _ _

As a (weak) cocartesian fibration🔗

If B\mathcal{B} has an image factorisation for every morphism, then its fibration of subobjects is a weak cocartesian fibration. By a general fact, if B\mathcal{B} also has pullbacks, then Sub⁡(−)\operatorname*{Sub}(-) is a cocartesian fibration.

  : (∀ {x y} (f : Hom x y) → Image B f)
  → is-weak-cocartesian-fibration Subobjects
Subobject-weak-opfibration ims .weak-lift f x' = l where
  module im = Image B (ims (f ∘ x' .map))

To understand this result, we remind ourselves of the universal property of an image factorisation for f:a→bf : a \to b: It is the initial subobject through with ff factors. That is to say, if m:Sub⁡(b)m : \operatorname*{Sub}(b) is another subobject, and f=mef = me for some map e:a→me : a \to m, then m≤im⁡fm \le \operatorname*{im}f. Summarised diagramatically, the universal property of an image factorisation looks like a kite:

Now compare this with the universal property required of a weak co-cartesian lift:

By smooshing the corner x′↪x→yx' \hookrightarrow x \to y together (i.e., composing x′x' and ff), we see that this is exactly the kite-shaped universal property of im⁡fx′\operatorname*{im}fx'.

  l : Weak-cocartesian-lift Subobjects f x'
  l .y' .domain = im.Im
  l .y' .map    = im.Im→codomain
  l .y' .monic  = im.Im→codomain-is-M

  l .lifting .map = im.corestrict
  l .lifting .sq  = sym im.image-factors

  l .weak-cocartesian .universal {x' = y'} h .map = im.universal _ (y' .monic) (h .map) (sym (h .sq))
  l .weak-cocartesian .universal h .sq = idl _ ∙ sym im.universal-factors

  l .weak-cocartesian .commutes g' = is-prop→pathp (λ _ → hlevel 1) _ _
  l .weak-cocartesian .unique _ _  = hlevel 1 _ _

The aforementioned general fact says that any cartesian and weak cocartesian fibration must actually be a full opfibration.

  : (∀ {x y} (f : Hom x y) → Image B f)
  → (pb : has-pullbacks B)
  → Cocartesian-fibration Subobjects
Subobject-opfibration images pb = cartesian+weak-opfibration→opfibration _
  (Subobject-fibration pb)
  (Subobject-weak-opfibration images)

Subobjects over a base🔗

We define the category Sub⁡(y)\operatorname*{Sub}(y) of subobjects of yy as a fibre of the subobject fibration. However, we use a purpose-built transport function to cut down on the number of coherences required to work with Sub⁡(y)\operatorname*{Sub}(y) at use-sites.

Sub : Ob → Precategory (o ⊔ ℓ) ℓ
Sub y = Fibre' Subobjects y re coh where
  re : ∀ {a b} → ≤-over (id ∘ id) a b → ≤-over id a b
  re x .map = x .map
  re x .sq  = ap₂ _∘_ (introl refl) refl ∙ x .sq

    coh : ∀ {a b} (f : ≤-over (id ∘ id) a b) → re f ≡ transport (λ i → ≤-over (idl id i) a b) f
    coh f = hlevel 1 _ _

module Sub {y} = Cr (Sub y)

Fibrewise cartesian structure🔗

Since products in slice categories are given by pullbacks, and pullbacks preserve monomorphisms, if B\mathcal{B} has pullbacks, then Sub⁡(y)\operatorname*{Sub}(y) has products, regardless of what yy is.

  : ∀ {y}
  → has-pullbacks B
  → has-products (Sub y)
Sub-products {y} pb a b = prod where
  it = pb (a .map) (b .map)

  prod : Product (Sub y) a b
  prod .Product.apex .domain = it .apex
  prod .Product.apex .map = a .map ∘ it .p₁
  prod .Product.apex .monic = monic-∘
    (a .monic)
    (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb)))

  prod .Product.π₁ .map = it .p₁
  prod .Product.π₁ .sq  = idl _

  prod .Product.π₂ .map = it .p₂
  prod .Product.π₂ .sq  = idl _ ∙ it .square

  prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .map =
    it .Pullback.universal {p₁' = q≤a .map} {p₂' = q≤b .map} (sym (q≤a .sq) ∙ q≤b .sq)
  prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .sq =
    idl _ ∙ sym (pullr (it .p₁∘universal) ∙ sym (q≤a .sq) ∙ idl _)
  prod .Product.has-is-product .is-product.π₁∘factor = hlevel 1 _ _
  prod .Product.has-is-product .is-product.π₂∘factor = hlevel 1 _ _
  prod .Product.has-is-product .is-product.unique _ _ _ = hlevel 1 _ _


Since identity of m,n:Sub⁡(y)m, n : \operatorname*{Sub}(y) is given by identity of they underlying objects and identity-over of the corresponding morphisms, if B\mathcal{B} is univalent, we can conclude that Sub⁡(y)\operatorname*{Sub}(y) is, too. Since Sub⁡(y)\operatorname*{Sub}(y) is always thin, we can summarise the situation by saying that Sub⁡(y)\operatorname*{Sub}(y) is a partial order if B\mathcal{B} is univalent.

Sub-is-category : ∀ {y} → is-category B → is-category (Sub y)
Sub-is-category b-cat .to-path {a} {b} x =
    (b-cat .to-path i)
    (Univalent.Hom-pathp-refll-iso b-cat (sym (x .Sub.from .sq) ∙ idl _))
    i : a .domain ≅ b .domain
    i = make-iso (x .map) (x .Sub.from .map) (ap map (Sub.invl x)) (ap map (Sub.invr x))
Sub-is-category b-cat .to-path-over p =
  Sub.≅-pathp refl _ $ is-prop→pathp (λ _ → hlevel 1) _ _