open import Cat.Displayed.Cartesian.Indexing
open import Cat.Displayed.Cartesian
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning
import Cat.Displayed.Morphism

module Cat.Displayed.GenericObject
  {o ℓ o' ℓ'} {B : Precategory o ℓ}
  (E : Displayed B o' ℓ')
  where

open Precategory B
open Cat.Displayed.Morphism E
open Cat.Displayed.Reasoning E
open Displayed E
open Functor

Generic objects🔗

There are 2 perspectives one can take on generic objects. The first is a purely logical one: generic objects provide us a tool for giving categorical models of higher order logics. The second perspective is that generic objects are a categorical way of describing the size of fibrations, and their ability to be internalized in the base category. We shall use both perspectives interchangeably!

With that caveat out of the way, we define a generic object to be some object $T:{\mathcal{E}}_U$ with the property that for any $X^{\prime }:{\mathcal{E}}_X\text{,}$ we have a (not necessarily unique) cartesian map $X^{\prime }\to T\text{.}$ Note that this means that generic objects are a structure in a fibration!

record Generic-object {t} (t' : Ob[ t ]) : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
  no-eta-equality
  field
    classify  : ∀ {x} → (x' : Ob[ x ]) → Hom x t
    classify' : ∀ {x} → (x' : Ob[ x ]) → Hom[ classify x' ] x' t'
    classify-cartesian : ∀ {x} (x' : Ob[ x ])
                       → is-cartesian E (classify x') (classify' x')

  module classify-cartesian {x} (x' : Ob[ x ]) = is-cartesian (classify-cartesian x')

The intuition for this definition is that if $\mathcal{E}$ has a generic object, then every object of $\mathcal{E}$ arises as a reindexing of $T$ along some morphism in the base.

If we think of $\mathcal{E}$ as some sort of logic over some syntactic category, then a generic object behaves like $\mathrm{Prop}\text{,}$ the type of propositions. To see why, recall that an object ${\mathcal{E}}_{\Gamma }$ over a classifying category is a proposition in ranging over some free variables of type $\Gamma \text{.}$ The classifying map in the base yields a substitution $\Gamma \to \mathrm{Prop}\text{,}$ or in other words, a term of type $\mathrm{Prop}$ in context $\Gamma \text{.}$ Furthermore, the classifying map upstairs gives an implication between the original proposition in ${\mathcal{E}}_{\Gamma }$ and a proof of the corresponding element of $\mathrm{Prop}\text{.}$

The size-based perspective on generic objects hinges on the fact that the family fibration on $\mathcal{C}$ has a generic object if and only if $\mathcal{C}$ is equivalent to a small, strict category. Fibred structure in the family fibration corresponds to structure in $\mathcal{C}\text{,}$ so we can see the generic objects as a generalization of both a strictness and size condition.

With this size-based perspective in mind, we say that a displayed category is globally small if it has a generic object.

record Globally-small : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
  no-eta-equality
  field
    {U} : Ob
    Gen : Ob[ U ]
    has-generic-ob : Generic-object Gen

  open Generic-object has-generic-ob public

module _ (fib : Cartesian-fibration E) where
  open Cartesian-fibration fib

We can also prove the aforementioned characterisation in terms of base changes: If there exists an object $t^{\prime }t\text{,}$ such that, for every $x^{\prime }x\text{,}$ there is a map $u:x\to t$ exhibiting $x^{\prime }\cong u^{\ast }(t^{\prime })$ — then $t^{\prime }$ is a generic object. The quantifier complexity of this sentence is a bit high, so please refer to the code:

  vertical-iso→Generic-object
    : ∀ {t} (t' : Ob[ t ])
    → (∀ {x} (x' : Ob[ x ])
      → Σ[ u ∈ Hom x t ]
         (base-change E fib u .F₀ t' ≅↓ x'))
    → Generic-object t'

  vertical-iso→Generic-object {t} t' viso = gobj where
    open Generic-object
    open has-lift

    module viso {x} (x' : Ob[ x ]) = _≅[_]_ (viso x' .snd)

    gobj : Generic-object t'
    gobj .classify x' = viso x' .fst
    gobj .classify' x' =
      hom[ idr _ ] (has-lift.lifting _ t' ∘' viso.from' x')
    gobj .classify-cartesian x' .is-cartesian.universal m h' =
      hom[ idl _ ] (viso.to' x' ∘' universal (viso x' .fst) t' m h')
    gobj .classify-cartesian x' .is-cartesian.commutes m h' =
      hom[] (lifting _ _ ∘' viso.from' x') ∘' hom[] (viso.to' x' ∘' universal _ _ _ _) ≡˘⟨ split _ _ ⟩≡˘
      hom[] ((lifting _ _ ∘' viso.from' x') ∘' (viso.to' x' ∘' universal _ _ _ _))     ≡⟨ weave _ _ refl (cancel-inner[] _ (viso.invr' x')) ⟩≡
      hom[] (lifting _ _ ∘' universal _ _ _ _)                                         ≡⟨ shiftl _ (has-lift.commutes _ _ _ _) ⟩≡
      h' ∎
    gobj .classify-cartesian x' .is-cartesian.unique {m = m} {h' = h'} m' p =
      m'                                                            ≡⟨ shiftr (sym (idl _) ∙ sym (idl _)) (insertl' _ (viso.invl' x')) ⟩≡
      hom[] (viso.to' x' ∘' viso.from' x' ∘' m')                    ≡⟨ reindex _ _ ∙ sym (hom[]-∙ (idl _) (idl _))  ∙ ap hom[] (unwhisker-r (idl _) (idl _)) ⟩≡
      hom[] (viso.to' x' ∘' ⌜ hom[ idl _ ] (viso.from' x' ∘' m') ⌝) ≡⟨ ap! (unique _ _ _ (whisker-r _ ∙ assoc[] ∙ unwhisker-l (ap (_∘ m) (idr _)) _ ∙ p)) ⟩≡
      hom[] (viso.to' x' ∘' universal _ _ _ h') ∎

Skeletal generic objects🔗

We say that a generic object $t^{\prime }$ is skeletal if the classifying map in the base category is unique: if $u:x\to t$ underlies a Cartesian map $x^{\prime }{\to }_u{t}^{\prime }\text{,}$ then it must be the map coming from the generic object structure of $t^{\prime }\text{.}$

This condition is quite strong: for instance, the family fibration of a strict category $\mathcal{C}$ has a skeletal generic object if and only if $\mathcal{C}$ is skeletal.¹

is-skeletal-generic-object : ∀ {t} {t' : Ob[ t ]} → Generic-object t' → Type _
is-skeletal-generic-object {t} {t'} gobj =
  ∀ {x} {x' : Ob[ x ]} {u : Hom x t} {f' : Hom[ u ] x' t'}
  → is-cartesian E u f' → u ≡ classify x'
  where open Generic-object gobj

is-skeletal-generic-object-is-prop
  : ∀ {t} {t' : Ob[ t ]} {gobj : Generic-object t'}
  → is-prop (is-skeletal-generic-object gobj)
is-skeletal-generic-object-is-prop = hlevel 

Gaunt generic objects🔗

A generic object is gaunt if the classifying maps themselves are unique. This condition expands on that of skeletality: if $u^{\prime }:x^{\prime }{\to }_u{t}^{\prime }$ is a Cartesian map into the generic object $t^{\prime }\text{,}$ then not only must $u$ be generated by the structure we have equipped $t^{\prime }$ with, but $u^{\prime }$ must, as well.

We can also expand on what this means for the family fibration: $\mathrm{Fam}(\mathcal{C})$ has a gaunt generic object if and only if $\mathcal{C}$ is itself gaunt (See here for the proof).

record is-gaunt-generic-object
  {t} {t' : Ob[ t ]}
  (gobj : Generic-object t')
  : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where
  no-eta-equality
  open Generic-object gobj

  field
    classify-unique : is-skeletal-generic-object gobj
    classify-unique'
      : ∀ {x} {x' : Ob[ x ]} {u : Hom x t} {f' : Hom[ u ] x' t'}
      → (cart : is-cartesian E u f')
      →  f' ≡[ classify-unique cart ] classify' x'

gaunt-generic-object→skeletal-generic-object
  : ∀ {t} {t' : Ob[ t ]} {gobj : Generic-object t'}
  → is-gaunt-generic-object gobj → is-skeletal-generic-object gobj
gaunt-generic-object→skeletal-generic-object =
  is-gaunt-generic-object.classify-unique

unquoteDecl H-Level-is-gaunt-generic-object = declare-record-hlevel  H-Level-is-gaunt-generic-object (quote is-gaunt-generic-object)