module Cat.Displayed.Doctrine {o β} (B : Precategory o β) where

# Regular hyperdoctrinesπ

A **regular hyperdoctrine** is a generalisation of the
defining features of the poset
of subobjects of a regular category; More
abstractly, it axiomatises exactly what is necessary to interpret
first-order (regular) logic *over* a finitely
complete category. There is quite a lot of data involved, so weβll
present it in stages.

While the *raison dβΓͺtre* of regular hyperdoctrines is the
interpretation of regular logic, that is far too much stuff for Agda to
handle if it were placed in this module. **The interpretation of
logic lives at logic
in a hyperdoctrine**.

record Regular-hyperdoctrine o' β' : Type (o β β β lsuc (o' β β')) where

To start with, fix a category
$B,$
which we think of as the *category of contexts* of our logic β
though keep in mind the definition works over a completely arbitrary
category. The heart of a regular hyperdoctrine is a displayed
category
$PB,$
which, a priori, assigns to every object
$Ξ:B$
a category
$P(Ξ)$
of **predicates** over it, where the set
$Hom(Ο,Ο)$
for
$Ο,Ο:P(Ξ)$
interprets the **entailment** relation between predicates;
we therefore write
$Οβ’_{Ξ}Ο.$

field β : Displayed B o' β' module β = Displayed β

However, having an entire *category* of predicates is hard to
make well-behaved: that would lend itself more to an interpretation of
dependent type theory, rather than the first-order logic we are
concerned with. Therefore, we impose the following three restrictions on
$P:$

field has-is-set : β Ξ β is-set β.Ob[ Ξ ] has-is-thin : β {x y} {f : Hom x y} x' y' β is-prop (β.Hom[ f ] x' y') has-univalence : β x β is-category (Fibre β x)

First, the space of predicates over
$Ξ$
must be a set. Second, the entailment
relation
$Οβ’_{Ξ}Ο$
must be a proposition, rather
than an arbitrary set β which we will use as justification to omit the
names of its inhabitants. Finally, each fibre category
$P(Ξ)$
must be univalent.
In light of the previous restriction, this means that each fibre
satisfies *antisymmetry*, or, specialising to logic, that
inter-derivable propositions are indistinguishable.

Next, each fibre $P(Ξ)$ must be finitely complete. The binary products interpret conjunction, and the terminal object interprets the true proposition; since we are working with posets, these two shapes of limit suffice to have full finite completeness.

fibrewise-meet : β {x} x' y' β Product (Fibre β x) x' y' fibrewise-top : β x β Terminal (Fibre β x)

Everything we have so far is fine, but it only allows us to talk
about predicates over a *specific* context, and we do not yet
have an interpretation of *substitution* that would allow us to
move between fibres. This condition is fortunately very easy to state:
it suffices to ask that
$P$
be a Cartesian
fibration.

cartesian : Cartesian-fibration β

Weβre almost done with the structure. To handle existential quantification, the remaining connective of regular logic, we use the key insight of Lawvere: the existential elimination and introduction rules

say precisely that existential quantification along $x$ is left adjoint to weakening by $x!$ Since weakening will be interpreted by cartesian lifts, we will interpret the existential quantification by a left adjoint to that: in other words, $P$ must also be a cocartesian fibration over $P.$

cocartesian : Cocartesian-fibration β

Note that we have assumed the existence of left adjoints to arbitrary substitutions, which correspond to forms of existential quantification more general than quantification over the latest variable. For example, if the base category $B$ has finite products, then existential quantification of a predicate $Ο:P(A)$ over $Ξ΄:AβAΓA$ corresponds to the predicate β$(i,j)β¦(i=j)β§Ο(i)$β.

##
That concludes the *data* of a regular hyperdoctrine. We will
soon write down the axioms it must satisfy: but before that, we need a
digression to introduce better notation for working with the
deeply-nested data we have introduced.

module cartesian = Cartesian-fibration cartesian module cocartesian = Cocartesian-fibration cocartesian module fibrewise-meet {x} (x' y' : β.Ob[ x ]) = Product (fibrewise-meet x' y') module fibrewise-top x = Terminal (fibrewise-top x) _[_] : β {x y} β β.Ob[ x ] β Hom y x β β.Ob[ y ] _[_] x f = cartesian.has-lift.x' f x exists : β {x y} (f : Hom x y) β β.Ob[ x ] β β.Ob[ y ] exists = cocartesian.has-lift.y' _&_ : β {x} (p q : β.Ob[ x ]) β β.Ob[ x ] _&_ = fibrewise-meet.apex aye : β {x} β β.Ob[ x ] aye = fibrewise-top.top _ infix 30 _[_] infix 25 _&_

The first two axioms concern the commutativity of substitution and the conjunctive connectives:

field subst-& : β {x y} (f : Hom y x) (x' y' : β.Ob[ x ]) β (x' & y') [ f ] β‘ x' [ f ] & y' [ f ] subst-aye : β {x y} (f : Hom y x) β aye [ f ] β‘ aye

Next, we have a *structural rule*, called **Frobenius
reciprocity**, governing the interaction of existential
quantification and conjunction. If substitution were invisible, it would
say that
$(βΟ)β§Ο$
is
$β(Οβ§Ο);$
Unfortunately, proof assistants force us to instead say that if we have
$Ο:P(Ξ),$
$Ο:P(Ξ),$
and
$Ο:ΞβΞ,$
then
$β_{Ο}(Ο)β§Ο$
is
$β_{Ο}(Οβ§Ο[Ο]).$

field frobenius : β {x y} (f : Hom x y) {Ξ± : β.Ob[ x ]} {Ξ² : β.Ob[ y ]} β exists f Ξ± & Ξ² β‘ exists f (Ξ± & Ξ² [ f ])

Finally, we have a general rule for the commutativity of existential
quantification and substitution. While in general the order matters, the
**Beck-Chevalley condition** says that we can conclude

provided that the square

is a pullback.

beck-chevalley : β {a b c d} {f : Hom a c} {g : Hom b c} {h : Hom d a} {k : Hom d b} β is-pullback B h f k g β β {Ξ±} β exists h (Ξ± [ k ]) β‘ (exists g Ξ±) [ f ]

That concludes the definition of regular hyperdoctrine. Said
snappily, a **regular hyperdoctrine**
$PB$
is a bifibration into
(meet-)semilattices
satisfying Frobenius reciprocity and the Beck-Chevalley condition.

β€-Poset : β {x : Ob} β Poset o' β' β€-Poset {x = x} .Poset.Ob = β.Ob[ x ] β€-Poset {x = x} .Poset._β€_ = β.Hom[ id ] β€-Poset {x = x} .Poset.β€-thin = has-is-thin _ _ β€-Poset {x = x} .Poset.β€-refl = β.id' β€-Poset {x = x} .Poset.β€-trans Ξ± Ξ² = Precategory._β_ (Fibre β _) Ξ² Ξ± β€-Poset {x = x} .Poset.β€-antisym Ξ± Ξ² = has-univalence _ .to-path $ Cat.make-iso (Fibre β _) Ξ± Ξ² (has-is-thin _ _ _ _) (has-is-thin _ _ _ _) module _ {x} where open Order.Reasoning (β€-Poset {x}) hiding (Ob-is-set ; Ob) public open Disp β public subst-β : β {x y z} (f : Hom y z) (g : Hom x y) {Ξ±} β (Ξ± [ f ]) [ g ] β‘ Ξ± [ f β g ] subst-β f g = β€-antisym (cartesian.has-lift.universalv _ _ (cartesian.has-lift.lifting _ _ β.β' cartesian.has-lift.lifting _ _)) (cartesian.has-lift.universalv _ _ (cartesian.has-lift.universal f _ g (cartesian.has-lift.lifting _ _))) subst-id : β {x} (Ξ± : β.Ob[ x ]) β Ξ± [ id ] β‘ Ξ± subst-id Ξ± = β€-antisym (cartesian.has-lift.lifting id Ξ±) (cartesian.has-lift.universal id Ξ± _ (β.id' β.β' β.id')) subst-β€ : β {x y} (f : Hom x y) {Ξ± Ξ² : β.Ob[ y ]} β Ξ± β€ Ξ² β Ξ± [ f ] β€ Ξ² [ f ] subst-β€ f p = cartesian.has-lift.universalv f _ $ hom[ idl _ ] (p β.β' cartesian.has-lift.lifting f _) exists-id : β {x} (Ξ± : β.Ob[ x ]) β exists id Ξ± β‘ Ξ± exists-id Ξ± = β€-antisym (cocartesian.has-lift.universal id Ξ± _ (β.id' β.β' β.id')) (cocartesian.has-lift.lifting id Ξ±) &-univ : β {x} {Ξ± Ξ² Ξ³ : β.Ob[ x ]} β Ξ± β€ Ξ² β Ξ± β€ Ξ³ β Ξ± β€ (Ξ² & Ξ³) &-univ p q = fibrewise-meet.β¨_,_β© _ _ p q &-comm : β {x} {Ξ± Ξ² : β.Ob[ x ]} β Ξ± & Ξ² β‘ Ξ² & Ξ± &-comm = β€-antisym (&-univ (fibrewise-meet.Οβ _ _) (fibrewise-meet.Οβ _ _)) (&-univ (fibrewise-meet.Οβ _ _) (fibrewise-meet.Οβ _ _)) β€-exists : β {x y} (f : Hom x y) {Ξ± Ξ²} β Ξ± β€ Ξ² [ f ] β exists f Ξ± β€ Ξ² β€-exists f p = cocartesian.has-lift.universalv f _ $ hom[ idr f ] (cartesian.has-lift.lifting f _ β.β' p) subst-! : β {x y} (f : Hom y x) {Ξ±} β β.Hom[ id ] Ξ± (aye [ f ]) subst-! f {Ξ±} = subst (Ξ» e β β.Hom[ id ] Ξ± e) (sym (subst-aye f)) (Terminal.! (fibrewise-top _))