2
$\begingroup$

Given an arbitrary topos $\mathscr{T}$ and objects $X, Y$ of $\mathscr{T}$, are the interpretations of the following terms equal to $\top : \mathrm{Hom}(1, \Omega)$?

  1. $\forall p, q : \Omega, (p \rightarrow q) \rightarrow (q \rightarrow p) \rightarrow p = q$.

  2. $\forall f, g : {}^X Y, (\forall x : X, f(x) = g(x)) \rightarrow f = g$.

  3. $\forall S_1, S_2 : P(X), S_1 \subseteq S_2 \rightarrow S_2 \subseteq S_1 \rightarrow S_1 = S_2$.

My attempt at 2, for example, would be: suppose we use a test object $U$, and we have $f, g : \mathrm{Hom}(U \times X, Y)$. The interpretation of the term in parentheses would suggest for any morphism $\phi : \mathrm{Hom}(V, U)$ and term $x : \mathrm{Hom}(V, X)$, then $f \circ (\phi, x) = g \circ (\phi, x)$. (More precisely, the pullback of $f$ to $\mathrm{Hom}(V \times X, Y)$ would be $f \circ (\phi \circ \pi_1, \pi_2)$, and then evaluation at $x$ corresponds to composing on the right with $(\mathrm{id}_V, x)$; so the result is $f \circ (\phi \circ \pi_1, \pi_2) \circ (\mathrm{id}_V, x) = f \circ (\phi, x)$, and similarly for $g$.) But then, by simply choosing $V := U \times X$, $\phi := \pi_1$, and $x := \pi_2$, we get $(\phi, x) = \mathrm{id}_{U \times X}$ so $f = g$.

And for 1, suppose we use a test object $U$, and we have $p, q : \mathrm{Sub}(U)$. Then $p \rightarrow q$ would be interpreted as $p$ factors through $q$, and $q \rightarrow p$ would be interpreted as $q$ factors through $p$. Therefore, $p \simeq q$, and by the definition of equality in $\mathrm{Sub}(U)$ this implies $p = q$. And 3 I think would be similar, except that $S_1, S_2 : \mathrm{Sub}(U \times X)$.

So, does this make any sense, or is it complete nonsense? I haven't actually seen a detailed treatment of the internal language, so I've been attempting to reconstruct what it might look like. My interpretation seems to largely make sense to me though I tend to get bogged down in the details if I try to formalize it generally - but also as far as I know, my interpretation might be completely off-base compared to the "official" one, and maybe even the question doesn't make sense.

As an optional follow-on question: is there a version of the internal language of a topos which allows for "proof terms" as in the Curry-Howard correspondence and if so, does it satisfy proof irrelevance: $\forall p : \Omega, \forall \alpha, \beta : p, \alpha = \beta$? What about definite description: is there a way to interpret something similar to $(\exists! x:X, \phi) \to \{ x:X | \phi \}$ in a topos where $\phi$ is a term of type $\Omega$ with a free variable $x : X$?

(Basically, I'm going through the classical axioms which aren't automatic in Coq's logic - though there are things there like the Type(n) hierarchy which have no interpretation in an arbitrary topos. Obviously, excluded middle and axiom of choice are not valid even in general algebraic-geometric sites. And "indefinite description" $(\exists x:X, \phi) \to \{ x:X | \phi \}$ isn't accepted even by most classical mathematicians as a valid way of giving a "definition", even if it's a consistent axiom.)

$\endgroup$
2
$\begingroup$

are the interpretations of the following terms equal to $\top : \mathrm{Hom}(1,\Omega)$?

Yes, the three principles you state are valid in the internal language of any topos, and the proofs you provide are correct.

In general, the internal language of a topos is an extensional dependent type theory supplemented with further rules governing power types. If you can read German, then you might enjoy this list (page 14) and the remark on page 16.

is there a version of the internal language of a topos which allows for "proof terms" as in the Curry-Howard correspondence

I don't think so. However, you might want to look at homotopy type theory, which is the internal language of $(\infty,1)$-toposes. Most propositions in HoTT do not satisfy proof irrelevance (this is seen as a feature, not a bug), but the "mere propositions" do.

What about definite description

Yes, definitely! You can add that to the internal language.

Proposition 2.6 of these notes of mine lists a simplification rule for the interpretation of "$\exists!$" using the Kripke–Joyal semantics (this is not quite what you're asking, but it's related, since one gives meaning to the definite description by exploiting this simplification rule).

$\endgroup$
  • $\begingroup$ Hmm, interesting... my version of the internal language was a more conservative extension of the internal language of a cartesian closed category, with types $\Omega$, $P(\cdot)$, sigma-types $\{\{ x:X | \cdot \}\}$; terms from the Heyting-algebra-object structure of $\Omega$, $=$, $\in$, subset comprehension $\{ x:X | \cdot \} : P(X)$; and then convenience notations such as $\forall x:X, \phi := \{ x:X | \phi \} = \{ x:X | \top \}$, $\exists x:X, \phi := \forall q:\Omega, (\forall x:X, \phi \to q) \to q$, etc. $\endgroup$ – Daniel Schepler Apr 30 '17 at 15:15
  • $\begingroup$ But then my definition of quotient by an equivalence relation (transliterating the usual classical definition as the sigma-type of equivalence classes) would have required definite description to work. And if you don't have proof terms in the internal language, I'm not sure exactly what type the definite description map would inhabit. $\endgroup$ – Daniel Schepler Apr 30 '17 at 15:20
  • $\begingroup$ I also wasn't sure what relations you have to add to the formal logic, in order to get it to be complete, i.e. the category with objects given by formal type expressions in the internal language, and morphisms given by formal expressions modulo formally provable equality, should be a topos. I would guess it would need to include these extensionality rules, along with more basic things like $\{ x:X | x \in S \} = S$, $(y \in \{ x:X | \phi \}) = \phi[x := y]$. $\endgroup$ – Daniel Schepler Apr 30 '17 at 15:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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