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)


## 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 = hlevel 2

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

  disp .idr' f'         = prop!
disp .idl' f'         = prop!
disp .assoc' f' g' h' = prop!


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 .Οβββ¨β©      = prop!
prod f g .has-is-product .Οβββ¨β©      = prop!
prod f g .has-is-product .unique _ _ = prop!

  term : β S β Terminal (Fibre disp S)
term S .top  _ = F.top
term S .hasβ€ f = is-propββis-contr (hlevel 1) (Ξ» 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'  β prop!
; unique    = Ξ» m p   β prop!
}


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 _ $elim! Ξ» e x p q β e F.=Λβ¨ q β©F.=Λ g x F.β€β¨ h' x β©F.β€ u' (m (f x)) F.=β¨ ap u' (ap m p) β©F.= u' (m i) F.β€β lifted .cocartesian .commutes m h = prop! lifted .cocartesian .unique m x = prop!  ## 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 = hlevel 1 idx .has-univalence S = set-identity-system (Ξ» _ _ _ _ β Cat.β -path (Fibre disp _) prop!) Ξ» 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))) β©F.β€ exist (Ξ» x β Ξ± x F.β© Ξ² (f x)) i F.β€β ) ( exist (Ξ» x β Ξ± x F.β© Ξ² (f x)) i F.β€β¨ F.β-universal _ (elim! Ξ» e x p q β e F.=β¨ sym q β© Ξ± x F.β© Ξ² (f x) F.=β¨ ap (Ξ± x F.β©_) (ap Ξ² p) β© Ξ± x F.β© Ξ² i F.β€β¨ F.β-inj (Ξ± x , inc (x , p , refl)) β©F.β€ F.β {I = img Ξ± i} (Ξ» (x , _) β x F.β© Ξ² i) F.β€β) β© 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 _ _