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

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!

\ Warning

The terminology surrounding generic objects is a bit of a disaster. What we refer to as a generic object is referred to as a weak generic object in (Jacobs 2001). However, we follow the terminology set out in (Sterling 2023), as generic objects in the sense of Jacobs are quite rare.

With that caveat out of the way, we define a generic object to be some object T:EUT : \mathcal{E}_{U} with the property that for any X′:EXX' : \mathcal{E}_{X}, we have a (not necessarily unique) cartesian map X′→TX' \to T. 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 E\mathcal{E} has a generic object, then every object of E\mathcal{E} arises as a reindexing of TT along some morphism in the base.

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

The size-based perspective on generic objects hinges on the fact that the family fibration on C\mathcal{C} has a generic object if and only if C\mathcal{C} is equivalent to a small, strict category. Fibred structure in the family fibration corresponds to structure in C\mathcal{C}, 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

We can also prove the aforementioned characterisation in terms of base changes: If there exists an object t′tt' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} t, such that, for every x′xx' \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} x, there is a map u:x→tu : x \to t exhibiting x′≅u∗(t′)x' \cong u^*(t') — then t′t' 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′t' is skeletal if the classifying map in the base category is unique: if u:x→tu : x \to t underlies a Cartesian map x′→ut′x' \to_u t', then it must be the map coming from the generic object structure of t′t'.

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

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
\ Warning

(Jacobs 2001) refers to “skeletal generic objects” as simply “generic objects”.

Gaunt Generic Objects🔗

A generic object is gaunt if the classifying maps themselves are unique. This condition expands on that of skeletality: if u′:x′→ut′u' : x' \to_u t' is a Cartesian map into the generic object t′t', then not only must uu be generated by the structure we have equipped t′t' with, but u′u' must, as well.

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

  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′
\ Warning

(Jacobs 2001) refers to “gaunt generic objects” as “strong generic objects”.


  1. See here for a proof.↩︎


References

  • Jacobs, Bart. 2001. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. Elsevier.
  • Sterling, Jonathan. 2023. “What Should a Generic Object Be?” arXiv. http://arxiv.org/abs/2210.04202.