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}\text{,}$ we can construct a displayed category of “Sierpinski cones” over $\mathcal{B}\text{,}$ 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\text{,}$ along with a function $U\to B(\top ,X)\text{.}$ 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\text{)}$ to $X\text{,}$ such that we can recover closed terms of $X$ from elements of $U\text{.}$

Morphisms behave like they do in an arrow category of $\mathcal{S}ets\text{:}$ given a map $f:X\to Y$ in $\mathcal{B}\text{,}$ 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\text{,}$ such that for all $u:U\text{,}$ we have $f\circ su(u)=sv(uvu)\text{.}$

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