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,$ we can construct a displayed category of βSierpinski conesβ over $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:B$ consists of a set $U,$ along with a function $UβB(β€,X).$ If we think about $B$ as some sort of category of contexts, then a scone over some context $X$ is some means of attaching semantic information (the set $U)$ to $X,$ such that we can recover closed terms of $X$ from elements of $U.$

Morphisms behave like they do in an arrow category of $Sets:$ given a map $f:XβY$ in $B,$ a map over $f$ in the category between $(U,su:UβB(1,X))$ and $(V,sv:VβB(1,Y))$ consists of a function $uv:UβV,$ such that for all $u:U,$ we have $fβsu(u)=sv(uvu).$

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

Scones : Displayed B (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$ 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