MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to first-order predicate logic too).

In the category $\mathbb{P}$ of propositions-in-dependent-type-contexts, an object is a well formed proposition $\Gamma \vdash \varphi:Prop$ and a morphism $(\Gamma \vdash \varphi:Prop) \rightarrow (\Delta \vdash \psi : Prop)$ consists of a context morphism $\vec{M} : \Gamma \rightarrow \Delta$ such that $\Gamma | \varphi \vdash \phi(\vec{M})$ is derivable. This category $\mathbb{P}$ is fibred over the category of dependent type contexts $\mathbb{C}$ via $(\Gamma \vdash \varphi:Prop) \mapsto \Gamma$.

Consider the "contradictory proposition" object, $A$, in $\mathbb{P}$ which I define as $\emptyset \vdash \perp : Prop$ and the "inconsistent context" object, $B$, which I define as $x : 0 \vdash \top:Prop$ (where $0$ is the empty type).

I would expect $A$ and $B$ to be isomorphic in $\mathbb{P}$ since both objects seems equally void to me in the sense that neither appear to have any models, i.e. there are no morphisms from the terminal object, $1 := \emptyset \vdash \top : Prop$, to either $A$ or $B$. But, of course, $A$ and $B$ cannot be isomorphic since a morphism from $A$ to $B$ entails the existence of a context morphism $M : \emptyset \rightarrow x : 0$ which would imply that the void type is inhabited.

Can someone assuage my concerns about $A$ and $B$ being equally void yet not isomorphic?

share|cite|improve this question
up vote 6 down vote accepted

My understanding of the situation is that you have to correctly understand what the morphisms do. A geometric picture might be helpful.

Let us interpret a context $\Gamma = x_1 : A_1, \ldots, x_n : A_n$ as a cartesian product $|\Gamma|$ of topological spaces. A proposition in a context $\Gamma \vdash \phi$ is interpreted as a subspace of a cartesian product $|\phi| \subseteq |\Gamma|$. I think the confusion arises if you think of a morphism $M : (\Gamma \vdash \phi) \to (\Delta \vdash \psi)$ as a continuous map $|\phi| \to |\psi|$, which it is not. It is an ambient map, i.e, a continuous map $|\Gamma| \to |\Delta|$ which also happens to map $|\phi| \to |\psi|$. Now it is clear that even though $|\phi|$ and $|\psi|$ may be homeomorphic as spaces, the may be embedded in $|\Gamma|$ and $|\Delta|$ in wildly different way (the wild Cantor sets come to mind), so it won't be possible to extend a homeomorphism between them to an ambient map.

In your example, we are comparing $\emptyset$ as a subspace of $\emptyset$ versus $\emptyset$ as a subspace of $1$. Even though the two empty subspaces are homeomorphic, there is no ambient map taking the latter to the former.

share|cite|improve this answer

I'm not sure what you mean by the individual propositional objects having models or not.

In any case, as you said, as morphism in $\mathbb P$ simply is a context morphism compatible with the preordering. So $A$ and $B$ are definitely not isomorphic in $\mathbb P$. In a model, $A$ is the initial subobject of the terminal object, while $B$ is the terminal subobject of the initial object (taking models in subobject fibrations for simplicity), and an isomorphism of these subobjects would restrict to an isomorphism of the initial object with the terminal object.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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