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?