open import Cat.Displayed.Cocartesian
open import Cat.Diagram.Limit.Finite
open import Cat.Displayed.Cartesian
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Displayed.Fibre
open import Cat.Displayed.Base
open import Cat.Prelude

open import Order.Base

import Cat.Displayed.Reasoning as Disp
import Cat.Reasoning as Cat

import Order.Reasoning

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

open Cat B


# 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.

Warning

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 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 which, a priori, assigns to every object a category of predicates over it, where the set for 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

  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 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 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 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 is left adjoint to weakening by Since weakening will be interpreted by cartesian lifts, we will interpret the existential quantification by a left adjoint to that: in other words, must also be a cocartesian fibration over

    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 has finite products, then existential quantification of a predicate over corresponds to the predicate ββ.

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 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 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 _))