Question

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?

Answer 1

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.

Answer 2

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.