module Cat.Regular where

# Regular categoriesπ

A **regular category** is a category with pullback-stable image factorisations. To define
regular categories, we use the theory of orthogonal morphisms,
specifically strong
epimorphisms: A regular category is one where every morphism factors
as a strong epimorphism followed by a monomorphism, and strong
epimorphisms are stable under pullback.

At face value, itβs a bit weird to take the definition of regular
categories to talk about strong, rather than *regular*,
epimorphisms. But it turns out that strong epimorphisms correspond
pretty directly to the idea of an image factorisation, or at least much
*more* directly than regular epimorphisms do. As we shall see, in
a regular category, every strong epimorphism is regular.

open Functor module _ {o β} (π : Precategory o β) where private module C = Cr π StrongEpi : β {a b} β C.Hom a b β Ξ© StrongEpi x = elΞ© (is-strong-epi π x) Mono : β {a b} β C.Hom a b β Ξ© Mono x = elΞ© (C.is-monic x)

record is-regular : Type (o β β) where field factor : β {a b} (f : C.Hom a b) β Factorisation π StrongEpi Mono f stable : is-pullback-stable π (is-strong-epi π) has-is-lex : Finitely-complete π module factor {a b} (f : C.Hom a b) = Factorisation (factor f) module lex = Finitely-complete has-is-lex

We also introduce some more palatable names for the components of the
provided factorisations: Letting
$f:AβB$
be a map and
$AβXβͺB$
its image factorisation, we refer to
$X$
as
$im(f),$
to
$AβX$
as `aβ im[_]`

, and
$XβͺB$
as `im[_]βͺb`

. These latter
two names have a placeholder for the morphism we are factoring.

im[_] : β {a b} (f : C.Hom a b) β C.Ob im[ f ] = factor f .Factorisation.mediating im[_]βͺb : β {a b} (f : C.Hom a b) β im[ f ] C.βͺ b im[ f ]βͺb = record { monic = β‘-out! (factor f .Factorisation.forgetβM) } aβ im[_] : β {a b} (f : C.Hom a b) β C.Hom a im[ f ] aβ im[ f ] = factor f .Factorisation.mediate

module _ (r : is-regular) where private module r = is-regular r open C monoβim-iso : β {a b} (f : C.Hom a b) β C.is-monic f β C.is-invertible r.aβ im[ f ] monoβim-iso f x = res where open Factorisation remβ : f β‘ r.im[ f ]βͺb .C.mor C.β r.aβ im[ f ] remβ = r.factor f .factors p = β‘-out! (r.factor f .mediateβE) .snd (record { monic = x }) (sym (r.factor f .factors) β sym (C.idr _)) res = C.make-invertible (p .centre .fst) (β‘-out! (r.factor f .mediateβE) .fst _ _ (C.pullr (p .centre .snd .fst) β C.id-comm)) (p .centre .snd .fst)

## Motivationπ

Regular categories are interesting in the study of categorical logic
since they have exactly the structure required for their subobject fibrations
to interpret existential quantifiers, *and* for these to commute
with substitution which, in this case, is interpreted as pullback.

Weβve already seen that, in a category with pullbacks, arbitrary
morphisms
$f:aβb$
induce an adjunction
$f_{!}β£f_{β}$
between
$C/bβC/a:$
the right adjoint models the substitution (base change) along
$f,$
and the left adjoint
models the *dependent sum* over
$f.$
Between subobject categories, though, pullbacks are not enough
structure: this can be seen type-theoretically by noting that, even if
$P:AβΞ©$
is a family of propositions, the sum
$Ξ£_{(}x:A)P(x)$
will generally not be.

Instead, the existential quantifier must be *truncated* to
work correctly, and it is this truncation that the pullback-stable image
factorisations in a regular category exist to model. In a category with
pullbacks and images, we have adjunctions
$β_{f}β£f_{β},$
now between
$Sub(a)βSub(b).$
However, the existence of images is not enough to guarantee they behave
type-theoretically. In a regular category, since images are stable under
pullback, the equation

holds as long as $f,$ $g,$ $h$ and $k$ fit into a pullback square, expressing that existential quantification commutes with substitution.

Another reason to be interested in regular categories is their
well-behaved calculus of relations: any category with
pullbacks has an associated bicategory of spans, but images
are precisely whatβs missing to interpret composition *of
relations*. Indeed, the existential quantifier in a regular category
allows us to interpret the formula for relational composition,

internally to an arbitrary category. Regularity comes in when we want
to show that composition of relations is *associative*: indeed,
associativity in the formula above, modulo associativity of the
conjunction
$Aβ§B,$
is exactly a question of *commutativity between
$β$
and substitution*. It follows, but we do not establish here, that a
category is regular *exactly when* its composition of relations
is associative.

As a universe for interpreting logic, regular categories allow us to
talk about formulae (in arbitrary contexts) consisting of conjunction,
equality, truth, and existential quantification, and all of these
connectives commute with substitution. This subset of logic is,
unsurprisingly, called **regular logic**. For working with
regular categories, one notes that $Sets$
is regular, and that regularity is
preserved by slicing.

## Strong epis are regularπ

This section formalises the proof of A1.3.4 from (Johnstone
2002), which says that every strong epimorphism^{1} in
a regular category is regular. Actually, weβll show that every strong
epimorphism in a regular category is **effective**: itβs
the coequaliser of its kernel pair.

-- Johnstone, A.1.3.4 module _ (r : is-regular) {A B} (f : C.Hom A B) (is-s : is-strong-epi π f) where private module r = is-regular r module kp = Pullback (r.lex.pullbacks f f) renaming (apex to R ; pβ to a ; pβ to b)

For a strong epimorphism $f:AβB,$ start by pulling $f$ back along itself to form the kernel pair $(a,b):RβA.$ We want to show that $f$ coequalises $a$ and $b,$ which means that any morphism $c:AβC$ satisfying $ca=cb$ should have a unique factorisation through $f.$ So, quantify over such morphisms and letβs get started.

private module Make {C} {c : C.Hom A C} (w : c C.β a β‘ c C.β b) where

We start by calculating the image factorisation of $(f,c):AβBΓC,$

$AdD(g,h)βBΓC.$dgh : Factorisation π StrongEpi Mono β¨ f , c β© dgh = r.factor β¨ f , c β© module dgh = Factorisation dgh renaming (mediating to D ; forget to gh ; mediate to d) open dgh using (D ; d ; gh) g : C.Hom D B g = Οβ C.β gh h : C.Hom D C h = Οβ C.β gh

Following Johnstone, we show that
$g$
is an isomorphism, so that
$hg_{β1}$
is the factorisation weβre looking for.^{2}
Since
$f$
is an extremal epimorphism, any monomorphism through which it factors
must be an iso. And since we have

it will suffice to show that $g$ is a monomorphism. So assume youβre given $k,l:EβD$ with $gk=gl;$ Letβs show that $k=l.$ Start by pulling back $(k,l):EβDΓD$ along $dΓd:AΓA,$ obtaining

g-monic : C.is-monic g g-monic {e} k l w' = β‘-out! dgh.forgetβM _ _ remβ where dΓd = Γ-functor .Fβ (d , d) module pb = Pullback (r.lex.pullbacks β¨ k , l β© dΓd) renaming (pβ to p ; apex to P ; pβ to mn ; square to sq'-) open pb using (p ; P ; mn ; sq'-) m = Οβ C.β mn n = Οβ C.β mn sq' : β¨ k C.β p , l C.β p β© β‘ β¨ d C.β m , d C.β n β© sq' = sym (β¨β©β _) β sq'- β β¨β©-unique (C.pulll Οβββ¨β© β C.pullr refl) (C.pulll Οβββ¨β© β C.pullr refl)

We define a map
$q:PβR$
into the kernel pair of
$a,$
factoring
$(m,n)$
through
$(a,b).$
Using this morphism we may conclude that
$hkp=hlp$
(`remβ`

).

q : C.Hom P R q = kp.universal $ f β m β‘β¨ C.pushl (extend-Οβ dgh.factors β C.pulll refl) β©β‘ g β d β m β‘Λβ¨ reflβ©ββ¨ by-Οβ sq' β©β‘Λ g β k β p β‘β¨ C.extendl w' β©β‘ g β l β p β‘β¨ reflβ©ββ¨ by-Οβ sq' β©β‘ g β d β n β‘Λβ¨ C.pushl (extend-Οβ dgh.factors β C.pulll refl) β©β‘Λ f β n β remβ = h β k β p β‘β¨ reflβ©ββ¨ by-Οβ sq' β©β‘ h β d β m β‘β¨ pulll (pullr (sym dgh.factors) β Οβββ¨β©) β©β‘ c β m β‘Λβ¨ reflβ©ββ¨ kp.pββuniversal β©β‘Λ c β a β q β‘β¨ extendl w β©β‘ c β b β q β‘β¨ reflβ©ββ¨ kp.pββuniversal β©β‘ c β n β‘Λβ¨ pulll (pullr (sym dgh.factors) β Οβββ¨β©) β©β‘Λ h β d β n β‘Λβ¨ reflβ©ββ¨ by-Οβ sq' β©β‘Λ h β l β p β

We want to show that
$hl=hk,$
for which it will suffice for
$p$
to be an epimorphism. Since weβre working in a regular category, we can
show that
$p$
is a *strong* epimorphism by showing that
$dΓd$
is a composite of strong epis. But
$dΓd$
is the composite
$(dΓid)(idΓd),$
and both of those maps are pullbacks of
$d,$
which *is* a strong epimorphism since it arises from an image
factorisation.

##
This `<details>`

tag contains the proof that
$dΓ1$
and
$1Γd$
are pullbacks of
$d.$
You may choose to unfold or skip it.

open is-pullback remβ : is-strong-epi π (Γ-functor .Fβ (d , id)) remβ = r.stable d Οβ {p2 = Οβ} (β‘-out! dgh.mediateβE) Ξ» where .square β Οβββ¨β© .universal {pβ' = pβ'} {pβ'} p β β¨ pβ' , Οβ β pβ' β© .pββuniversal {pβ' = pβ'} {pβ'} {p = p} β β¨β©β _ Β·Β· apβ β¨_,_β© (pullr Οβββ¨β© β sym p) (pullr Οβββ¨β© β idl _) Β·Β· sym (β¨β©-unique refl refl) .pββuniversal β Οβββ¨β© .unique {p = p} {lim'} q r β β¨β©-unique r $ sym $ ap (Οβ β_) (sym q) β pulll Οβββ¨β© β ap (_β lim') (idl _) remβ : is-strong-epi π (Γ-functor .Fβ (id , d)) remβ = r.stable d Οβ {p2 = Οβ} (β‘-out! dgh.mediateβE) Ξ» where .square β Οβββ¨β© .universal {pβ' = pβ'} {pβ'} p β β¨ Οβ β pβ' , pβ' β© .pββuniversal {p = p} β β¨β©β _ Β·Β· apβ β¨_,_β© (pullr Οβββ¨β© β idl _) (pullr Οβββ¨β©) Β·Β· sym (β¨β©-unique refl p) .pββuniversal β Οβββ¨β© .unique {p = p} {lim'} q r β β¨β©-unique (sym (ap (Οβ β_) (sym q) β pulll Οβββ¨β© β ap (_β lim') (idl _))) r remβ = sym (Γ-functor .F-β _ _) β ap (Γ-functor .Fβ) (Ξ£-pathp (idl _) (idr _))

So
$dΓd$
is a strong epimorphism by the above remarks, and
$p$
is a pullback of
$dΓd,$
so it is also strong epic (`remβ`

); We obtain
$hk=hl$
(`remβ`

). By pushing some symbols,
this gives
$(g,h)k=(g,h)l$
(`remβ`

), but
$(g,h)$
is a monomorphism by construction, so
$k=l$
β so
$g$
is *also* monic.

remβ : is-strong-epi π dΓd remβ = subst (is-strong-epi π) remβ (strong-epi-compose π _ _ remβ remβ) remβ : is-strong-epi π p remβ = r.stable _ _ remβ pb.has-is-pb remβ : h β k β‘ h β l remβ = remβ .fst _ _ $ (h β k) β p β‘β¨ sym (assoc _ _ _) β remβ β©β‘ h β l β p β‘β¨ pulll refl β©β‘ (h β l) β p β remβ : gh C.β k β‘ gh C.β l remβ = gh β k β‘β¨ β¨β©-unique refl refl β©ββ¨refl β©β‘ β¨ g , h β© β k β‘β¨ β¨β©β _ β©β‘ β¨ g β k , h β k β© β‘β¨ apβ β¨_,_β© w' remβ β©β‘ β¨ g β l , h β l β© β‘Λβ¨ β¨β©β _ β©β‘Λ β¨ g , h β© β l β‘Λβ¨ β¨β©-unique refl refl β©ββ¨refl β©β‘Λ gh β l β

Having shown that
$g$
is monic, and knowing that
$f$
β a strong (thus extremal) epimorphism β factors through it, we conclude
that
$g$
is an isomorphism. It remains to `compute`

that
$hg_{β1}f=c,$
which we do below.

g-iso : is-invertible g g-iso = make-invertible (p .centre .fst) (p .centre .snd .snd) (β‘-out! dgh.mediateβE .fst _ _ ( pullr (pullr (sym dgh.factors) β Οβββ¨β©) β p .centre .snd .fst β introl refl)) module g-ortho where p = is-s .snd (record { monic = g-monic }) (idl _ β sym (pullr (sym dgh.factors) β Οβββ¨β©)) module g = _β _ (invertibleβiso _ g-iso)

compute = (h β g.from) β f β‘β¨ pullr refl β pullr refl β©β‘ Οβ β dgh.gh β g.from β f β‘β¨ refl β©ββ¨ β¨β©-unique refl refl β©ββ¨ refl β©β‘ Οβ β β¨ g , h β© β g.from β f β‘β¨ reflβ©ββ¨ β¨β©β _ β©β‘ Οβ β β¨ g β g.from β f , h β g.from β f β© β‘β¨ Οβββ¨β© β©β‘ h β g.from β f β‘β¨ reflβ©ββ¨ g-ortho.p .centre .snd .fst β©β‘ h β dgh.d β‘β¨ pullr (sym dgh.factors) β©β‘ Οβ β β¨ f , c β© β‘β¨ Οβββ¨β© β©β‘ c β

This proves that
$f,$
an arbitrary strong epi, coequalises its kernel pair. Itβs an effective
epimorphism! So itβs definitely the case that it coequalises
*some* pair of maps.

open is-regular-epi renaming (r to Kp) open is-coequaliser is-strong-epiβis-regular-epi : is-regular-epi π f is-strong-epiβis-regular-epi = go where go : is-regular-epi π f go .Kp = kp.R go .arrβ = kp.a go .arrβ = kp.b go .has-is-coeq .coequal = kp.square go .has-is-coeq .universal w = Make.h w β Make.g.from w go .has-is-coeq .factors {e' = e'} {p = w} = Make.compute w go .has-is-coeq .unique {e' = e'} {p = p} {colim} q = is-s .fst _ _ $ colim β f β‘β¨ q β©β‘ e' β‘Λβ¨ Make.compute p β©β‘Λ (Make.h p β Make.g.from p) β f β

Note: Johnstone prefers to work with βcoversβ instead, which in our lingo are

*extremal*epimorphisms. In a finitely complete category, strong and extremal epimorphisms coincideβ©οΈJohnstone says itβs

*clearly*unique, but the tiny calculation is included at the end of the proof since it wasnβt clear to meβ©οΈ

## References

- Johnstone, Peter T. 2002.
*Sketches of an Elephant: a Topos Theory Compendium*. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.