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.

\ 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

    β„™ : 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

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

  infix 30 _[_]
  infix 25 _&_

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

      : βˆ€ {x y} (f : Hom y x) (x' y' : β„™.Ob[ x ])
      β†’ (x' & y') [ f ] ≑ x' [ f ] & y' [ f ]

      : βˆ€ {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

      : βˆ€ {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.

      : βˆ€ {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 _))