module Cat.Regular.Slice
  {o β„“} {C : Precategory o β„“} (y : ⌞ C ⌟) (reg : is-regular C) where

Regular categories are stable under slicingπŸ”—

Let be a regular category: a finitely complete category where maps have pullback-stable strong epi-mono factorisations. In this module, we’ll establish that, for any object the slice is also a regular category. If we motivate regular categories by the well-behaved calculus of relations of their internal language, stability under slicing means that relations remain well-behaved under passing to arbitrary contexts.

Other than finite limits, which we have already extensively investigated in slice categories (see limits in slices), what remains of the proof is a characterisation of the strong epimorphisms in a slice To do this, we will freely use that and are finitely complete, and instead characterise the extremal epimorphisms.

For this, it will suffice to show that the inclusion functor both preserves and reflects extermal epimorphisms. Given an extremal epi over and a non-trivial factorisation of through a monomorphism in we can show that itself is a monomorphism over and that it factors in It follows that is invertible as a map over meaning it is invertible in

  preserve-cover
    : βˆ€ {a b} (h : C/y.Hom a b)
    β†’ is-strong-epi C/y h
    β†’ is-strong-epi C (h .map)
  preserve-cover {b = B} h cover = is-extremal-epi→is-strong-epi C r.has-is-lex λ m g p →
    let
      mono : cut (B .map ∘ m .mor) C/y.β†ͺ B
      mono = record
        { mor   = record { map = m .mor ; commutes = refl }
        ; monic = Ξ» g h p β†’ ext (m .monic _ _ (ap map p))
        }

      inv : C/y.is-invertible (record { map = m .mor ; commutes = refl })
      inv = extreme mono
        (record { map = g ; commutes = pullr (sym p) βˆ™ h .commutes })
        (ext p)
    in make-invertible
      (inv .C/y.is-invertible.inv .map)
      (ap map (inv .C/y.is-invertible.invl))
      (ap map (inv .C/y.is-invertible.invr))
    where extreme = is-strong-epi→is-extremal-epi C/y cover

In the converse direction, suppose is a map over which is a strong epimorphism in Since the projection functor preserves monos (it preserves pullbacks), any non-trivial factorisation of through a monomorphism over must still be a non-trivial factorisation when regarded in We can then calculate that the inverse to is still a map over

  reflect-cover
    : βˆ€ {a b} (h : C/y.Hom a b)
    β†’ is-strong-epi C (h .map)
    β†’ is-strong-epi C/y h
  reflect-cover h cover = is-extremal-epi→is-strong-epi C/y C/y-lex λ m g p →
    let inv = extn (pres-mono m) (g .map) (ap map p)
    in C/y.make-invertible
      (record
        { map      = inv .is-invertible.inv
        ; commutes = invertible→epic inv _ _ $
          cancelr (inv .is-invertible.invr) βˆ™ sym (m .mor .commutes)
        })
      (ext (inv .is-invertible.invl))
      (ext (inv .is-invertible.invr))
    where extn = is-strong-epi→is-extremal-epi C cover

Since the projection functor preserves and reflects strong epimorphisms, we can compute image factorisations over as image factorisations in And since the projection functor additionally preserves pullbacks, by the same argument, it suffices for strong epimorphisms to be stable under pullback in for them to be stable under pullback in too.

slice-is-regular : is-regular (Slice C y)
slice-is-regular .factor {a} {b} f = fact' where
  fact = r.factor (f .map)
  private module f = Factorisation fact

  fact' : Factorisation C/y (StrongEpi C/y) (Mono C/y) f
  fact' .mediating = cut (b .map ∘ f.forget)
  fact' .mediate = record { commutes = pullr (sym f.factors) βˆ™ f .commutes }
  fact' .forget .map      = f.forget
  fact' .forget .commutes = refl
  fact' .mediate∈E = do
    c ← f.mediate∈E
    pure (reflect-cover (fact' .mediate) c)
  fact' .forget∈M = inc Ξ» g h p β†’ ext $ out! f.forget∈M (g .map) (h .map) (ap map p)
  fact' .factors = ext f.factors

slice-is-regular .stable {B = B} f g {p1} {p2} cover is-pb =
  reflect-cover p1 $ r.stable _ _
    (preserve-cover _ cover)
    (pullback-below→pullback-above is-pb)

slice-is-regular .has-is-lex = C/y-lex