Repository logo
 

What should a generic object be?

Published version
Peer-reviewed

Repository DOI


Type

Article

Change log

Abstract

jats:titleAbstract</jats:title>jats:pJacobs 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 jats:italichigher order fibrations</jats:italic>, jats:italicpolymorphic fibrations</jats:italic>, jats:inline-formulajats:alternatives<jats:inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" mime-subtype="png" xlink:href="S0960129523000117_inline1.png" />jats:tex-math λ2 </jats:tex-math></jats:alternatives></jats:inline-formula>-jats:italicfibrations</jats:italic>, jats:italictriposes</jats:italic>, 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, jats:italicetc.</jats:italic> 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, jats:italici.e.</jats:italic> in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of jats:underlineacyclic</jats:underline> generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the jats:italicrealignment</jats:italic> property of universes to the setting of an arbitrary fibration.</jats:p>

Description

Keywords

4904 Pure Mathematics, 49 Mathematical Sciences

Journal Title

Mathematical Structures in Computer Science

Conference Name

Journal ISSN

0960-1295
1469-8072

Volume Title

33

Publisher

Cambridge University Press (CUP)