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.

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

To start with, fix a category $\mathcal{B}\text{,}$ 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 $\mathbb{P}\mathcal{B}\text{,}$ which, a priori, assigns to every object $\Gamma :\mathcal{B}$ a category $\mathbb{P}(\Gamma )$ of predicates over it, where the set $\mathbf{Hom}(\varphi ,\psi )$ for $\varphi ,\psi :\mathbb{P}(\Gamma )$ interprets the entailment relation between predicates; we therefore write $\varphi {⊢}_{\Gamma }\psi \text{.}$

  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 $\mathbb{P}\text{:}$

  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 $\Gamma$ must be a set. Second, the entailment relation $\varphi {⊢}_{\Gamma }\psi$ 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 $\mathbb{P}(\Gamma )$ 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 $\mathbb{P}(\Gamma )$ 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 $\mathbb{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\text{!}$ Since weakening will be interpreted by cartesian lifts, we will interpret the existential quantification by a left adjoint to that: in other words, $\mathbb{P}$ must also be a cocartesian fibration over $\mathbb{P}\text{.}$

    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 $\mathcal{B}$ has finite products, then existential quantification of a predicate $\varphi :\mathbb{P}(A)$ over $\delta :A\to A\times A$ corresponds to the predicate “$(i,j)\mapsto (i=j)\wedge \varphi (i)$”.

  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  _[_]
  infix  _&_

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 $(\exists \varphi )\wedge \psi$ is $\exists (\varphi \wedge \psi )\text{;}$ Unfortunately, proof assistants force us to instead say that if we have $\varphi :\mathbb{P}(\Gamma )\text{,}$ $\psi :\mathbb{P}(\Delta )\text{,}$ and $\rho :\Gamma \to \Delta \text{,}$ then ${\exists }_{\rho }(\varphi )\wedge \psi$ is ${\exists }_{\rho }(\varphi \wedge \psi [\rho ])\text{.}$

  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 $\mathbb{P}\mathcal{B}$ 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 _))