open import Cat.Morphism.Factorisation
open import Cat.Diagram.Limit.Finite
open import Cat.Morphism.Orthogonal
open import Cat.Morphism.StrongEpi
open import Cat.Diagram.Pullback
open import Cat.Instances.Slice
open import Cat.Prelude
open import Cat.Regular

import Cat.Reasoning as Cr

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.

private
module r = is-regular reg
C/y = Slice C y
module C/y = Cr C/y
open Cr C
open Factorisation
open is-regular
open Functor
open /-Obj
open /-Hom

private
C/y-lex : Finitely-complete C/y
C/y-lex = with-pullbacks C/y Slice-terminal-object pb where
pb : β {A B X} (f : C/y.Hom A X) (g : C/y.Hom B X) β Pullback C/y f g
pb {A = A} f g = below where
above = r.lex.pullbacks (f .map) (g .map)

below : Pullback C/y f g
below .Pullback.apex = cut (A .map β above .Pullback.pβ)
below .Pullback.pβ .map      = above .Pullback.pβ
below .Pullback.pβ .commutes = refl
below .Pullback.pβ .map      = above .Pullback.pβ
below .Pullback.pβ .commutes =
pushl (sym (g .commutes)) β apβ _β_ refl (sym (above .Pullback.square)) β pulll (f .commutes)
below .Pullback.has-is-pb = pullback-aboveβpullback-below (above .Pullback.has-is-pb)

pres-mono
: β {a b} (h : a C/y.βͺ b)
β a .domain βͺ b .domain
pres-mono h .mor = h .mor .map
pres-mono {a = A} h .monic a b p = ap map $h .C/y.monic {c = cut (A .map β a)} (record { commutes = refl }) (record { commutes = pushl (sym (h .mor .commutes)) Β·Β· apβ _β_ refl (sym p) Β·Β· pulll (h .mor .commutes) }) (ext p)  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