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 with the property that for any we have a (not necessarily unique) cartesian map 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 has a generic object, then every object of arises as a reindexing of along some morphism in the base.

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

The size-based perspective on generic objects hinges on the fact that the family fibration on has a generic object if and only if is equivalent to a small, strict category. Fibred structure in the family fibration corresponds to structure in 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 such that, for every there is a map exhibiting β€” then 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 is skeletal if the classifying map in the base category is unique: if underlies a Cartesian map then it must be the map coming from the generic object structure of

This condition is quite strong: for instance, the family fibration of a strict category has a skeletal generic object if and only if 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 is a Cartesian map into the generic object then not only must be generated by the structure we have equipped with, but must, as well.

We can also expand on what this means for the family fibration: has a gaunt generic object if and only if 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.