While reading about forcing theory, I came across the concept of Boolean algebra valued models of ZFC. The main idea seems to be: instead of the sheaf/presheaf approach of focusing on a particular location in a hierarchy and asking what objects exist at each level, the Boolean algebra valued models turn that around. They focus on a particular object, and ask at what levels that object exists; and then, it generalizes the "set of levels" to an element of a Boolean algebra.
So, I was wondering whether the same thing could be done to form a topos of Heyting algebra valued models of a type. At a preliminary level, what I'm thinking of could look something like: fix a complete Heyting algebra $H$.
- Objects consist of a type $\operatorname{dom}(X)$; a function $X : \operatorname{dom}(X) \to H$; and a function $\operatorname{dom}(X)^2 \to H$ which we will denote $\lVert \cdot = \cdot \rVert$ which forms an equivalence relation "when restricted to the subset selected by $X$". To wit, $X(t) \le \lVert t = t \rVert$; $X(t) \cdot X(u) \cdot \lVert t = u \rVert \le \lVert u = t \rVert$; and $X(t) \cdot X(u) \cdot X(v) \cdot \lVert t = u \rVert \cdot \lVert u = v \rVert \le \lVert t = v \rVert$. As motivation for definitions and proofs, we will think of this as selecting a subset of $\operatorname{dom}(X)$, and then taking the quotient by the given equivalence relation on the subset.
- Morphisms from $X$ to $Y$ are the functions $f : \operatorname{dom}(X) \to \operatorname{dom}(Y)$ such that $X(t) \le Y(f(t))$ and $X(t) \cdot X(u) \cdot \lVert t = u \rVert \le \lVert f(t) = f(u) \rVert$.
- The identity morphism and composition of morphisms are given by the identity on $\operatorname{dom}(X)$, and composition of the underlying functions, respectively.
Then it looks easy to show that this forms a category. As for showing that it forms a topos:
- Products look easy: set $\operatorname{dom}(\prod_{\alpha \in A} X_\alpha) := \prod_{\alpha \in A} \operatorname{dom}(X_\alpha)$; $\left(\prod_{\alpha\in A} X_\alpha\right) ((t_\alpha)_{\alpha \in A}) := \prod_{\alpha\in A} X_\alpha(t_\alpha)$; and $\lVert (t_\alpha) = (u_\alpha) \rVert := \prod_{\alpha\in A} \lVert t_\alpha = u_\alpha \rVert$. The projections would just be the projections $\prod_{\alpha\in A} \operatorname{dom}(X_\alpha) \to \operatorname{dom}(X_\beta)$. (So in particular, the final object would have domain $\{ * \}$, function $* \mapsto 1$, and equivalence relation $(*, *) \mapsto 1$.)
- Equalizers should be straightforward: given morphisms $f, g : X \to Y$, set $X'$ to have the same domain and equivalence relation as $X$; and $X'(t) := X(t) \cdot \lVert f(t) = g(t) \rVert$. The morphism $X' \to X$ would be the identity on $\operatorname{dom}(X)$.
Where I'm getting tripped up is trying to define a subobject classifier and exponential objects. Possible definitions I'm thinking of:
- $\operatorname{dom}(\Omega) := H$, $\Omega(p) := 1$, and $\lVert p = q \rVert := (p \Leftrightarrow q)$. Here, my conjecture would be that any subobject of $X$ is isomorphic to an object $X'$ with the same domain and equivalence relation as $X$, with $X'(t) \le X(t)$ for all $t$; and then, the characteristic function of $X' \hookrightarrow X$ would be $X'$. (Possible step: if $f : Y \to X$ is a monomorphism, maybe start by defining $X'$ to be the subobject with $X'(t) := \sum_{u \in \operatorname{dom}(Y)} Y(u) \cdot \lVert f(u) = t \rVert$. But then I'm having trouble seeing how to get a morphism from $X'$ to $Y$. Maybe to fix this, I need to allow morphisms to be $H$-valued relations $\operatorname{dom}(X) \times \operatorname{dom}(Y) \to H$ with a further restriction that the relation forms a well-defined function? Or on another tack, maybe restrict objects to be "sheaves" somehow with respect to the covering relation $\sum_{\alpha \in A} p_\alpha = q$?)
- $\operatorname{dom}(Y^X) := \operatorname{dom}(Y)^{\operatorname{dom}(X)}$; $Y^X(f) := \prod_{t\in \operatorname{dom}(X)} (X(t) \Rightarrow Y(f(t))) \cdot \prod_{t,u\in \operatorname{dom}(X)} (X(t) \cdot X(u) \cdot \lVert t = u \rVert \Rightarrow \lVert f(t) = f(u) \rVert)$; and $\lVert f = g \rVert := \prod_{t\in \operatorname{dom}(X)} (X(t) \Rightarrow \lVert f(t) = g(t) \rVert)$. (And again, if morphisms need to be generalized to $H$-valued relations, maybe I would need to change this to $\operatorname{dom}(Y^X) := H^{\operatorname{dom}(X)\times \operatorname{dom}(Y)}$, $Y^X(f)$ is the evaluation of the proposition that $f$ forms a function, and the equivalence relation could be pointwise equivalence of the relations.)
And now, looking back, it's also possible that the definitions could be simplified by consolidating the selection function and equivalence relation into a single partial equivalence relation, i.e. an $H$-valued relation satisfying the symmetry and transitivity conditions, but necessarily reflexivity.
So, my main question is: has some definition along these lines already been worked out? And as a follow-up question: I get the strong feeling that evaluations of propositions in the internal language of a topos, when applied to this topos, should be strongly related to functions to $H$, in some way that I haven't been able to formulate in detail. Is there such a relation, and if so, what would it look like?
Best Answer
Yes, something along these lines has been worked out. The construction is known as the "tripos-to-topos" construction. Your intuition about using partial equivalence relations is spot-on.
Let $Heyt$ be the category of Heyting algebras. We first describe a functor $F : Sets^{op} \to Heyt$. This functor is simply the functor sending $X$ to $H^X$. In fact, $F$ always outputs a complete Heyting algebra since $H$ is complete.
Let us note that for all $f : A \to B$, the map $Ff : FB \to FA$ preserves all meets and all joins. Therefore, $Ff$ has a left adjoint $\exists_f$ and a right adjoint $\forall_f : FA \to FB$. Moreover, these adjoints satisfy the Beck-Chevalley condition. This gives us a "first-order hyperdoctrine with equality".
From here, we can construct the category of partial equivalence relations.
In a bit more generality, consider a category $C$ with finite limits and a functor $F : C^{op} \to Heyt$, where for all $f : A \to B$, $Ff$ has a left and a right adjoint which satisfy the Beck-Chevalley condition. Such a functor is known as a first-order hyperdoctrine with equality. We write $f^{-1}$ instead of $Ff$.
A partial equivalence relation consists of an object $A \in C$, together with some predicate $P \in F(A \times A)$, which satisfies the following conditions:
The arrows from $(A, P)$ to $(B, Q)$ will consist of $f \in F(A \times B)$ which satisfies the following conditions:
Using these tools, we can fairly easily define composition. Given $f : (A, P) \to (B, Q)$ and $g : (B, Q) \to (C, R)$, we can define $g \circ f : (A, P) \to (C, R)$ as follows. We have maps $(p_1, p_2) : A \times B \times C \to A \times B$, $(p_1, p_3) : A \times B \times C \to A \times C$, and $(p_2, p_3) : A \times B \times C \to B \times C$. Then $g \circ f = \exists_{(p_1, p_2)} ((p_1, p_2)^{-1}(f) \land (p_2, p_3)^{-1}(g))$. This corresponds to defining $g \circ f = \{(x, z) \in A \times C \mid \exists y \in B (f(x, y) \land g(y, z))\}$.
One can easily show that this gives us a category. In fact, it gives us a Heyting category - a category in which we can interpret first-order intuitionist logic. This type of category has finite limits, an initial object, Heyting algebra structures for subobjects, and left and right adjoints to pullbacks for monos.
We now add one final condition on $F$. The condition is:
This makes $F$ into a "tripos". In the particular case $FX = H^X$, we see that we can construct $P_x = H^X$ with $in_X : X \times H^X \to H$ being the obvious map.
Using the tripos condition, we can prove that the resulting category of partial equivalence relations is in fact a topos. Finally, we have the following theorem:
So the "correct" way of constructing $H$-valued types just gives us the topos of sheaves on the locale $H$.
There are a few other interesting ways of getting triposes. The first is the "syntactic tripos". Let's say we're working with intuitionist higher-order logic. Then let $C$ be the category of types, where the objects are (products of) types, the arrows are function terms, and $F(T)$ is the Heyting algebra of predicates on $T$. The tripos-to-topos construction then produces a topos where the true statements in the internal logic exactly correspond to provable statements.
The second is, of course, starting with $C$ being the topos and taking the sub-object functor. The tripos-to-topos construction will simply produce a topos which is equivalent to $C$ - this shouldn't be terribly surprising.
The third is using a partial combinatory algebra. This is related to Kleene's realizability models for arithmetic and can be used to construct a topos where, for example, we can show in the internal logic that all functions $\mathbb{N} \to \mathbb{N}$ are computable. It can also be used to model Brouwer's intuitionism.
For more information, see the nLab page.