3
$\begingroup$

In Bart Jacobs. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, 1999. isbn: 9780444508539, the author writes, p. 326:

enter image description here

Sometimes, for instance in Bart Jacobs' Thesis, Definition 1.2.9, the unicity in (ii) is dropped, so that generic object are identified with weak generic objects.

However, later on, on p. 473, Definition 8.4.3, he writes

A polymorphic fibration with $\Omega$ in the base as generic object

(my emphasis), which implies that $\Omega \in |\mathbb{B}|$ according to the notation of the definition 5.2.8.

I scanned

  • Saunders Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer New York, 1971. isbn: 978-1-4757-4721-8. doi: 10.1007/978-1-4757-4721-8.
  • Joachim Lambek and Philip Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics 7. Cambridge University Press, 1986. isbn: 0521246652.

and other lectures notes without finding any other definition of what a generic object is, and where it lives.

Am I missing some obvious equivalence, or has that object a more common synonym? I know it is sometimes called "distinguished object", for instance in those notes by Thomas Streicher, but I could'nt find any appropriate definition for that object.

$\endgroup$
  • 3
    $\begingroup$ I think he means there is some unnamed object in $\mathbb{E}$ such that $p$ of that object is $\Omega$. $\endgroup$ – Mike Shulman Nov 18 '15 at 19:50
  • $\begingroup$ Let $\mathbb{E}_X$ be the fibre over the object $X\in \mathbb{B}$, i.e. the subcategory of $\mathbb{E}$ whose objects have for image through $p$ the object $X$, and whose morphism have for image through $p$ the identity over $X$. And let $T \in \mathbb{E}$ be that object $pT = \Omega$. Do we have that $\mathbb{E}_{\Omega} = T$? I would understand this shortcut in the notation if that equality was true, but I don't think this is true in general. $\endgroup$ – Clément Nov 18 '15 at 20:02
  • 4
    $\begingroup$ No, $T$ is certainly not the only object in the fiber over $\Omega$. It's a sloppy abuse of notation, but it's common enough in this sort of situation. It's analogous to saying "let $F$ be a left adjoint of $G$" without giving a name to the adjunction: in general there might be more than one adjunction relating two given functors, but when we say "let $F$ be a left adjoint of $G$" we generally mean that we've specified a particular such adjunction, but without giving it a name. $\endgroup$ – Mike Shulman Nov 18 '15 at 23:45
  • 2
    $\begingroup$ Please do not post pictures of mathematics. It is not that hard to copy the relevant definition. $\endgroup$ – Andrej Bauer Nov 30 '15 at 18:30
8
$\begingroup$

I don't have Bart Jacobs' book so I don't know for sure what the context is for this extract from it, but I suspect that it is the categorical semantics of a type of types or universe such as in Martin-Löf Type Theory. This is not treated by Mac Lane or Lambek and Scott but my own book Practical Foundations of Mathematics considers related material, though not Martin-Löf Type Theory.

A fibration is a way of presenting the manner in which a mathematical structure varies according to a certain parameter. The parameter is represented by the base category $\mathbb B$ and for each value $X\in\mathbb B$ the corresponding structure is the category ${\mathbb E}_X$, which is called the fibre over $X$. As $X$ "varies" along a morphism $f:Y\to X$, this structure is related by a functor $f^*:{\mathbb E}_X\to{\mathbb E}_Y$. In a fibration, all of these categories and functors are collected together into a single category $\mathbb E$ together with a functor $p:{\mathbb E}\to{\mathbb B}$ with certain properties. In this, the fibre ${\mathbb E}_X\subset{\mathbb E}$ consists of the objects and morphisms that $p$ takes to $X$ and ${\mathsf{id}}_X$. We say informally that these objects and morphisms live over $X$.

The clearest paradigm of the use of fibrations in categorical type theory is that of types and predicates. Then the base category consists of types and terms (more precisely, its objects are contexts, ie lists of typed variables, and its morphisms are lists of terms whose types correspond to the target context and whose free variables correspond to the source). The fibre over a particular context consists of the predicates in its variables. The horizontal or prone or cartesian lifting of a base morphism at a predicate has as source the substituted form of the predicate using the terms that make up the morphism.

What is a generic predicate? Since any predicate on any type can be a substituted form of it, the free variable of the generic predicate cannot be any ordinary type but must somehow say what it is to be a predicate. If you follow through the definition, you will see that, for a strong generic predicate, this type has to be the subobject classifier $\Omega$ of a topos, whilst a weak generic predicate is the type or kind $\mathbf{Prop}$ of propositions.

We can handle universes or types of types in a similar way. Now the variables in the base category denote type-unknowns and the fibre over a particular context (list of type variables) consists of the type-expressions and terms that are definable using that list of type variables. The generic type is a single type variable qua type-expression in the fibre over the context that consists of that single type vaiable. Analogously to the previous case, its type is $\mathbf{Type}$, the type of all types. However, this can only give a weak generic type.

In fact, $\mathbf{Type}$ cannot itself be a type if you want the terms to do ordinary mathematics, with equality and functions, although it can be if you're doing domain theory with fixed points. In the former setting, such as in Martin-Löf Type Theory or Homotopy Type Theory, a hierarchy of universes is introduced; this has a corresponding hierarchy of generic types.

Personally, I feel that fibrations obfuscate categorical type theory.

The naive way of doing this would be to use indexed categories, which are functors ${\mathbb B}\to{\mathbf{Cat}}^{\mathsf{op}}$. In the applications in pure mathematics, we get pseudofunctors instead, where we have to take account of isomorphisms and coherence thereof; this was the reason for using fibrations instead, as explained in a paper of Bénabou that is notorious for its personal language. In the applications to type theory, on the other hand, these isomorphisms are unnecessary because the syntax ensures functoriality.

A deeper objection to indexed categories is that the functors mix up internal and external notions and making sense of them in the usual foundational setting (sets or toposes) requires the axiom-scheme of replacement. Using fibrations avoids this and potentially allows us to understand replacement in the context of a topos (see the final pages of my book).

The categorical technology that I prefer to fibrations is that of a category with a class of display maps, which is set out in Chapter VIII of my book.

In the applications of fibrations to type theory, each fibre usually has a terminal object, with which we can identify the objects of the base category, and we just work in the total category of the fibration (its source qua functor). The display maps are the terminal projections in each fibre, from which we recover the fibration as the codomain.

In the paradigm of types and propositions above, an object of the total category is a list of types together with a predicate on them. We may think of this as a subset of a product of sets, or just a mono. A morphism is a commutative square, which is a pullback iff the morphism is prone (horizonatal, cartesian). A base object (context) consists of a list of types together with the true predicate, or a set considered as the entire subset of itself. The display map corresponding to a particular object (mono) is the square consisting of this mono on the vertical sides and identities on the horizontal sides, though more briefly we take it to be the mono.

We can think of the display map in terms of its fibres. In the case of a predicate on a single type (or subset of a set), the fibre over an element is the truth-value of the predicate at that element, where we think of a truth value as a subset of the singleton. The mono displays these truth values over the set in that the source of the display map is the disjoint union of these sub-singletons.

I leave it as an exercise to see why the map $\top:{\mathbf 1}\to\Omega$ in a topos is the display of all possible truth values over their names.

We can now understand a generic type in the same way. The target of the display map is the type $\mathbf{Type}$ of all types. The fibre over each element of $\mathbf{Type}$ (the name of a type) is the extent of that type, so the source of the display map is the disjoint union of all types.

I leave it as another exercise to see that, for a model $M$ of set theory, this display map is the global mebership relation, $\{(x,y):M^2|x\in y\}\to M$ by $(x,y)\mapsto y$.

I proposed the word prone in this subject because the notion has nothing to do with Descartes and the word cartesian, like regular and normal, is grossly over-used in mathematics. Morphisms of the total category that the fibration takes to identities have been called vertical. However, there are two ways in which morphisms can be orthogonal to vertical morphisms, whilst the English language conveniently provides two words for horizontal, namely prone (face up) and supine (face down).

$\endgroup$
  • $\begingroup$ Thanks for your answer that is enlightening and shed new perspectives on my research. However I cannot accept it as an answer to my question, since you are in fact answering another (way more interesting, I admit) question. I scanned your book and will again, thanks for that detailed introduction to its concepts. $\endgroup$ – Clément Nov 30 '15 at 17:15
3
$\begingroup$

On the very same page (p. 326), Bart Jacobs writes, in the proof of a proposition:

Assume $p$ has a generic object $T \in \mathbb{E}$, say with $\Omega = pT \in \mathbb{B},$

So even if that convention is never explicitly written, it is reasonnable to assume that Mike Shulman is right when he writes as a comment

I think he means there is some unnamed object in $\mathbb{E}$ such that $p$ of that object is $\Omega$.

In short: $\Omega \in |\mathbb{B}|$ is the image of the generic object.

$\endgroup$
  • 1
    $\begingroup$ "$p$ of that object is $\Omega$" is the same as saying that the object is in the fibre over $\Omega$, as you remarked in your comment of 18 November, although I would use $\Omega$ for the fibre containing the generic predicate, not the generic object. I fail to see what you consider wrong with my explanation and how yours is somehow the correct one. $\endgroup$ – Paul Taylor Dec 1 '15 at 10:50
  • 3
    $\begingroup$ (BTW, thanks for editing my question) Nothing is wrong with your explanation; on the contrary, it is way more interesting than mine. I just thought that someone who looks at this question would expect a simple answer regarding where $\Omega$ lives, and what it is. $\endgroup$ – Clément Dec 1 '15 at 16:34

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.