open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Morphism.Factorisation
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Coequaliser
open import Cat.Morphism.StrongEpi
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Reasoning as Cr

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 be a map and its image factorisation, we refer to as to as aβ im[_], and 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 induce an adjunction between the right adjoint models the substitution (base change) along and the left adjoint models the dependent sum over Between subobject categories, though, pullbacks are not enough structure: this can be seen type-theoretically by noting that, even if is a family of propositions, the sum 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 now between 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 and 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 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 is regular, and that regularity is preserved by slicing.

## Strong epis are regularπ

This section formalises the proof of A1.3.4 from , which says that every strong epimorphism1 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)

      open kp using (R ; a ; b ; square)
open Binary-products π r.lex.products
open C


For a strong epimorphism start by pulling back along itself to form the kernel pair We want to show that coequalises and which means that any morphism satisfying should have a unique factorisation through 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

      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 is an isomorphism, so that is the factorisation weβre looking for.2 Since is an extremal epimorphism, any monomorphism through which it factors must be an iso. And since we have

it will suffice to show that is a monomorphism. So assume youβre given with Letβs show that Start by pulling back along 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 β©


We define a map into the kernel pair of factoring through Using this morphism we may conclude that (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 for which it will suffice for to be an epimorphism. Since weβre working in a regular category, we can show that is a strong epimorphism by showing that is a composite of strong epis. But is the composite and both of those maps are pullbacks of which is a strong epimorphism since it arises from an image factorisation. This <details> tag contains the proof that and are pullbacks of 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 is a strong epimorphism by the above remarks, and is a pullback of so it is also strong epic (remβ); We obtain (remβ). By pushing some symbols, this gives (remβ), but is a monomorphism by construction, so β so 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 β l              β


Having shown that is monic, and knowing that β a strong (thus extremal) epimorphism β factors through it, we conclude that is an isomorphism. It remains to compute that 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 β©β‘
Οβ β β¨ 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) β©β‘
c                                          β


This proves that 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 β©β‘