open import Cat.Displayed.Instances.Pullback
open import Cat.Displayed.Instances.Slice
open import Cat.Instances.Sets.Complete
open import Cat.Displayed.Cartesian
open import Cat.Diagram.Terminal
open import Cat.Instances.Slice
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Functor.Hom as Hom

module Cat.Displayed.Instances.Scone
  {o β„“} (B : Precategory o β„“)
  (terminal : Terminal B)
  where

open Precategory B
open Terminal terminal
open Hom B
open /-Obj

Sierpinski conesπŸ”—

Given a category B\ca{B}, we can construct a displayed category of β€œSierpinski cones” over B\ca{B}, or β€œscones” for short. Scones provide a powerful set of tools for proving various properties of categories that we want to think of as somehow β€œsyntactic”.

A scone over some object X:BX : \ca{B} consists of a set UU, along with a function Uβ†’B(⊀,X)U \to B(\top, X). If we think about B\ca{B} as some sort of category of contexts, then a scone over some context XX is some means of attatching semantic information (the set UU) to XX, such that we can recover closed terms of XX from elements of UU.

Morphisms behave like they do in an arrow category of Sets\ca{Sets}: given a map f:Xβ†’Yf : X \to Y in B\ca{B}, a map over ff in the category between (U,su:Uβ†’B(1,X))(U, su : U \to \ca{B}(1, X)) and (V,sv:Vβ†’B(1,Y))(V, sv : V \to \ca{B}(1, Y)) consists of a function uv:Uβ†’Vuv : U \to V, such that for all u:Uu : U, we have f∘su(u)=sv(uvu)f \circ su(u) = sv (uv u).

With the exposition out of the way, we can now define the category of scones by abstract nonsense: the category of scones over B\ca{B} is the pullback of the fundamental fibration along the global sections functor.

Scones : Displayed B (lsuc β„“) (lsuc β„“)
Scones = Change-of-base Hom[ top ,-] (Slices (Sets β„“))

We can unfold the abstract definition to see that we obtain the same objects and morphisms described above.

scone : βˆ€ {X} β†’ (U : Set β„“) β†’ (∣ U ∣ β†’ Hom top X) β†’ Scones.Ob[ X ]
scone U s = cut {domain = U} s

scone-hom : βˆ€ {X Y} {f : Hom X Y} {U V : Set β„“}
          β†’ {su : ∣ U ∣ β†’ Hom top X} {sv : ∣ V ∣ β†’ Hom top Y}
          β†’ (uv : ∣ U ∣ β†’ ∣ V ∣)
          β†’ (βˆ€ u β†’ f ∘ (su u) ≑ sv (uv u))
          β†’ Scones.Hom[ f ] (scone U su) (scone V sv)
scone-hom uv p = slice-hom uv (funext p)

As a fibrationπŸ”—

The category of scones over B\ca{B} is always a fibration. This is where our definition by abstract nonsense begins to shine: base change preserves fibrations, and the codomain fibration is a fibration whenever the base category has pullbacks, which sets has!

Scones-fibration : Cartesian-fibration Scones
Scones-fibration =
  Change-of-base-fibration _ _ $
  Codomain-fibration _ $
  Sets-pullbacks