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 $\mathcal{B}$, we can construct a displayed category of βSierpinski conesβ over $\mathcal{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 : \mathcal{B}$ consists of a set $U$, along with a function $U \to B(\top, X)$. If we think about $\mathcal{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 $\mathcal{Sets}$: given a map $f : X \to Y$ in $\mathcal{B}$, a map over $f$ in the category between $(U, su : U \to \mathcal{B}(1, X))$ and $(V, sv : V \to \mathcal{B}(1, Y))$ consists of a function $uv : U \to V$, such that for all $u : U$, we have $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 $\mathcal{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.

private
module Scones = Displayed Scones


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 $\mathcal{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