What should a generic object be?

TL;DR

This paper critically examines existing definitions of generic objects in fibrational categories, identifies limitations, and proposes new terminology and classes of generic objects inspired by higher category theory and homotopy type theory.

Contribution

It introduces a new alignment of terminology for generic objects and proposes a novel class of acyclic generic objects inspired by recent developments in higher category theory.

Findings

Existing definitions exclude some fundamental examples.

New terminology emphasizes common forms of generic objects.

Proposes a new class of acyclic generic objects.

Abstract

Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations, polymorphic fibrations, ${\lambda}2$-fibrations, triposes, and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.