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

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

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)
  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) β†’
        e            F.=⟨ sym q ⟩F.=
        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)))
      ⟩F.≀
      exist (Ξ» x β†’ Ξ± x F.∩ Ξ² (f x)) i           F.β‰€βˆŽ )
    ( exist (Ξ» x β†’ Ξ± x F.∩ Ξ² (f x)) i           F.β‰€βŸ¨
        F.⋃-universal _ (Ξ» (e , p) β†’ β–‘-rec! (Ξ» { (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.β‰€βˆŽ }) 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 _ _