open import Cat.Instances.Sets.Complete
open import Cat.Displayed.Cocartesian
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Doctrine
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.Frame
open import Order.Base

import Cat.Reasoning as Cat

import Order.Frame.Reasoning as Frm

open Regular-hyperdoctrine
open Cocartesian-fibration
open Cartesian-fibration
open Cocartesian-lift
open Cartesian-lift
open is-cocartesian
open is-cartesian
open is-product
open Displayed
open Terminal
open Product

module Cat.Displayed.Doctrine.Frame where


# Indexed framesπ

An example of regular hyperdoctrine that is not the poset of subobjects of a regular category is given by the canonical indexing of a frame the bifibration corresponding through the Grothendieck construction to We will construct this in very explicit stages.

Indexed-frame : β {o β ΞΊ} β Frame o β β Regular-hyperdoctrine (Sets ΞΊ) (o β ΞΊ) (β β ΞΊ)
Indexed-frame {o = o} {β} {ΞΊ} F = idx where

  module F = Frm (F .snd)

private opaque
isp : β {x : Type ΞΊ} {f g : x β β F β} β is-prop (β x β f x F.β€ g x)
isp = Ξ -is-hlevel 1 Ξ» _ β F.β€-thin


## The indexingπ

As the underlying displayed category of our hyperdoctrine, weβll fibre the slice category over The objects over a set are the functions However, rather than a discrete fibration, we have a fibration into posets: the ordering at each fibre is pointwise, and we can extend this to objects in different fibres by the equivalence of maps into a Cartesian lift of the codomain.

  disp : Displayed (Sets ΞΊ) (o β ΞΊ) (β β ΞΊ)
disp .Ob[_] S          = β S β β β F β
disp .Hom[_]     f g h = β x β g x F.β€ h (f x)
disp .Hom[_]-set f g h = is-propβis-set isp

disp .id'      x = F.β€-refl
disp ._β'_ p q x = F.β€-trans (q x) (p _)

  disp .idr' f'         = isp _ _
disp .idl' f'         = isp _ _
disp .assoc' f' g' h' = isp _ _


Since our ordering at each fibre is the pointwise ordering, it follows that our limits are also pointwise limits: the meet is the function and the terminal object is the function which is constantly the top element.

  prod : β {S : Set ΞΊ} (f g : β S β β β F β) β Product (Fibre disp S) f g
prod f g .apex x = f x F.β© g x
prod f g .Οβ i   = F.β©β€l
prod f g .Οβ i   = F.β©β€r
prod f g .has-is-product .β¨_,_β© Ξ± Ξ² i = F.β©-universal _ (Ξ± i) (Ξ² i)

  prod f g .has-is-product .Οββfactor    = isp _ _
prod f g .has-is-product .Οββfactor    = isp _ _
prod f g .has-is-product .unique _ _ _ = isp _ _

  term : β S β Terminal (Fibre disp S)
term S .top  _ = F.top
term S .hasβ€ f = is-propββis-contr isp (Ξ» i β F.!)


## As a fibrationπ

As we have defined the ordering by exploiting the existence of Cartesian lifts, it should not be surprising that the lift a function along a function is simply the composite

  cart : Cartesian-fibration disp
cart .has-lift f g .x' x = g (f x)
cart .has-lift f g .lifting i = F.β€-refl
cart .has-lift f g .cartesian = record
{ universal = Ξ» m p x β p x
; commutes  = Ξ» m h'  β isp _ _
; unique    = Ξ» m p   β isp _ _
}


However, the cocartesian lifts are a lot more interesting, and their construction involves a pretty heavy dose of propositional resizing. In ordinary predicative type theory, each frame is associated with a particular level for which it admits arbitrary joins. But our construction of the hyperdoctrine associated with a frame works for indexing a frame over an arbitrary category of sets! How does that work?

The key observation is that the join of a family can be replaced by the join of its image; and since can be made to exist at the same level as regardless of how large is, this replacement allows us to compute joins of arbitrary families. More relevantly, itβll let us compute the cocartesian lift of a function along a function

  cocart : Cocartesian-fibration disp
cocart .has-lift {x = X} {y = Y} f g = lifted module cocart where


At each we would like to take the join

indexed by the fibre of over But since we do not control the size of that type, we can replace this by the join over the subset

which is the image of as a function

    img : β Y β β Type _
img y = Ξ£[ e β F ] β‘ (Ξ£[ x β X ] ((f x β‘ y) Γ (g x β‘ e)))

exist : β Y β β β F β
exist y = F.β {I = img y} fst


That this satisfies the universal property of a cocartesian lift is then a calculation:

    lifted : Cocartesian-lift disp f g
lifted .y' y      = exist y
lifted .lifting i = F.β-inj (g i , inc (i , refl , refl))
lifted .cocartesian .universal {u' = u'} m h' i = F.β-universal _ Ξ» (e , b) β
β‘-rec! (Ξ» { (x , p , q) β
g x          F.β€β¨ h' x β©F.β€
u' (m (f x)) F.=β¨ ap u' (ap m p) β©F.=
u' (m i)     F.β€β }) b
lifted .cocartesian .commutes m h = isp _ _
lifted .cocartesian .unique   m x = isp _ _


## Putting it togetherπ

Weβre ready to put everything together. By construction, we have a βcategory displayed in posetsβ,

  idx : Regular-hyperdoctrine (Sets ΞΊ) _ _
idx .β                = disp
idx .has-is-set  x    = Ξ -is-hlevel 2 Ξ» _ β F.Ob-is-set
idx .has-is-thin f g  = isp
idx .has-univalence S = set-identity-system
(Ξ» _ _ _ _ β Cat.β-path (Fibre disp _) (isp _ _))
Ξ» im β funextP Ξ» i β F.β€-antisym (Cat.to im i) (Cat.from im i)


which is both a fibration and an opfibration over

  idx .cartesian   = cart
idx .cocartesian = cocart


with finite fibrewise limits preserved by reindexing,

  idx .fibrewise-meet x' y' = prod x' y'
idx .fibrewise-top  S     = term S
idx .subst-& f x' y'      = refl
idx .subst-aye f          = refl


which satisfies Frobenius reciprocity and the Beck-Chevalley condition. Frobenius reciprocity follows by some pair mangling and the infinite distributive law in

  idx .frobenius {X} {Y} f {Ξ±} {Ξ²} = funext Ξ» i β F.β€-antisym
( exist Ξ± i F.β© Ξ² i                         F.=β¨ F.β-distribr _ _ β©F.=
F.β {I = img Ξ± i} (Ξ» (x , _) β x F.β© Ξ² i) F.β€β¨
F.β-universal _ (Ξ» img β F.β-inj
( img .fst F.β© Ξ² i
, β‘-map (Ξ» { (x , p , q) β x , p , apβ F._β©_ q (ap Ξ² p) }) (img .snd)))
exist (Ξ» x β Ξ± x F.β© Ξ² (f x)) i           F.β€β )
( exist (Ξ» x β Ξ± x F.β© Ξ² (f x)) i           F.β€β¨
F.β-universal _ (Ξ» (e , p) β β‘-rec! (Ξ» { (x , p , q) β
Ξ± x F.β© Ξ² i                               F.β€β¨ F.β-inj (Ξ± x , inc (x , p , refl)) β©F.β€
F.β {I = img Ξ± i} (Ξ» (x , _) β x F.β© Ξ² i) F.β€β }) p)
F.β {I = img Ξ± i} (Ξ» (x , _) β x F.β© Ξ² i) F.=β¨ sym (F.β-distribr _ _) β©F.=
exist Ξ± i F.β© Ξ² i                         F.β€β)
where open cocart {X} {Y} f


And the Beck-Chevalley condition follows from the observation that a pullback square induces an equivalence between and which sends to so that the joins which define both possibilities for quantification or substitution agree:

  idx .beck-chevalley {A} {B} {C} {D} {f} {g} {h} {k} ispb {Ξ±} =
funext Ξ» i β F.β-apβ± (IsoβEquiv (eqv i))
where
module c X Y = cocart {X} {Y}
module pb = is-pullback ispb
open is-iso

eqv : β i β Iso (c.img D A h (Ξ» x β Ξ± (k x)) i) (c.img B C g Ξ± (f i))
eqv i .fst      (e , p) = e , β‘-map (Ξ» { (d , p , q) β k d , sym (pb.square $β _) β ap f p , q }) p eqv i .snd .inv (e , p) = e , β‘-map (Ξ» { (b , p , q) β let it : β D β it = pb.universal {P' = el! (Lift _ β€)} {pβ' = Ξ» _ β i} {pβ' = Ξ» _ β b} (funext (Ξ» _ β sym p)) (lift tt) in it , (pb.pββuniversal$β lift tt) , ap Ξ± (pb.pββuniversal \$β lift tt) β q }) p
eqv i .snd .rinv (x , _) = refl ,β squash _ _
eqv i .snd .linv (x , _) = refl ,β squash _ _