2 spelling

1

# Why no morphisms from the contradictory proposotion to the inconsistent context?

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?