<p>If you're going to work <em>only</em> in the internal language then you can just use a proof assistant. There is a minor technicality of having or not having powersets, since proof assistants are typically type theories, but Coq's <code>Prop</code> is consistent with an interpretation of Coq in a topos.</p>

<p>You're suggesting however to use the machine as a sort of translation tool that would get you from the internal language to the interpretation in a model. This is a fine idea, except I think it would not be as useful as one might expect. It is true that the translation from the internal language to the model is mechanical, but unfortunately it produces convoluted translations that need a lot of massaging before they're useful. (If you ever tried to use the Lawvere-Tierney interpretation of topos logic in a sheaf topos you'll know.)</p>

<p>There is one more problem, namely the <em>reverse</em> translation. We often start with a known concept or object in the model, and would like a good description or axomatization of it in the internal language. This is typically hard work and real math. I do not see how current proof assistants could help.</p>

<p>On the technical side of things one would have to worry about formalizing:</p>

<ul>
<li>the syntax and the rules of the internal language</li>
<li>the model</li>
<li>the interpretation</li>
</ul>

<p>That is a lot of work, too. Some projects along these lines have been done (for instance the interpretation of $\lambda$-calculus in a cartesian closed category). I am not aware of anyone formalizing toposes, for instance.</p>

<p>In summary, using a proof assistant to help check that you're not doing anything wrong in the internal language is a good idea (in fact, it is a <em>very</em> good idea, as attested by homotopy type theory, where we used Coq and Agda to develop new theorems which were only later unformalized into English), but using it to get statements about models is unlikely to work without a lot of extra work. Which is not to say that you shouldn't try!</p>

CC BY-SA 3.0
2016-04-09T21:17:49.680Z
Do you have a reference for Type Theory + Prop ~~ topos? This was my intuition but I haven't seen anyone else say it until now.
Max New
CC BY-SA 3.0
2016-04-09T21:22:13.953Z
Also, for model-specific logics, specific *axioms* will be specific to the models but the structure of the logic overall is still just higher-order logic, right? I'm imagining that you would externally characterize features of your model (like the Next-time functor in the step-indexing paper) and then just reflect them as axioms in your internal language. Coming up with **nice** and **complete** axiomatizations would still be hard math but my hope is that the machine can automate some of the plumbing.
Max New
CC BY-SA 3.0
2016-04-10T00:04:41.153Z
For step-indexing in particular it would make sense to extend the topos logic with a modal operator. This will in general be a feature of any situation in which you care about a subtopos, or you have a (co)monad that you want to study, etc.
Andrej Bauer
CC BY-SA 3.0
2016-04-10T00:05:37.393Z
For the Type theory + Prop, you just stare at every rule and see that if you interpret Prop as the subobject classifier, it's all valid in a topos.
Andrej Bauer
CC BY-SA 4.0
2021-05-21T16:58:41.620Z
The problem with this approach is that adding new axioms doesn't compute well. This mostly works for classical math but it's not so helpful for constructive math. I guess rewrite rules could help. Another problem is that topos is a rather strong construction. It would be nice to figure out internal languages of more limited categories. Also just adding axioms isn't so great for reflection. Would be nice to work some of this stuff into compilers and interpreters.
Ms. Molly Stewart-Gallus
CC BY-SA 4.0
2021-05-22T10:43:54.393Z
@MolossusSpondee: What does "this approach" refer to? I never mentioned any axioms, and if you're referring to Max New's comment, I think you misunderstood the meaning of "axioms" there. We're not talking about the addition of uninterpreted constants in type theory, although even that can be quite useful. Computation and constructivity aren't dogmas.
Andrej Bauer
CC BY-SA 4.0
2024-08-22T22:46:22.273Z
Could you elaborate a bit about the issues with the Lawvere-Tierney interpretation in a sheaf topos? With my current knowledge, this seems analogous to doing topology using Kuratowski closures instead of the standard approach with open subsets. but even if that's true I still don't appreciate the difficulties.
Somatic Custard
CC BY-SA 4.0
2024-08-23T13:04:08.763Z
@SomaticCustard: It's just a fact that unfolding the Lawvere-Tierney interpretation in a sheaf topos quickly leads to very uwieldy formulas. I should however point out that since I wrote the answer in 2016 there have been some cool developments, both in terms of proof assistants supporting sheaf semantics (Coq in particular), and people actually coding up models (the HoTT0 project in Lean). And also, one can probably go some distance by using the j-operators as modal operators and do modal logic.
Andrej Bauer
CC BY-SA 4.0
2024-08-24T03:38:14.780Z
@AndrejBauer Ok, thank you! My mind certainly goes toward modal operators (and I've seen recommendation to call it LT modality instead of topology), but I have little experience with modal logic anyhow.
Would Agda be unsuitable for this stuff? I settled on it having the least drawbacks of all proof assistants, but I keep seeing counterpoints. This deserves its own question...but you would probably be my top choice of answerer anyway!
Somatic Custard
CC BY-SA 3.0
2016-04-09T20:30:19.667Z
2016-04-09T20:30:19.667Z
Andrej Bauer
<p>In <a href="https://hal.inria.fr/hal-00685150">Extending Type Theory with Forcing</a> by  Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, <a href="https://github.com/mattam82/Forcing">implemented</a> as a type-preserving translation in the style of Bernardy and Lasson's <a href="https://who.rocq.inria.fr/Marc.Lasson/articles/RealParam/RealParam.pdf">parametricity translation</a>.</p>

<p>This means that you can define terms in your usual type theory, and then "translate them" into a "forcing layer" where they are interpreted as translations at a different translation type. For example, the translation induced by indexing over decreasing natural numbers lets you use your usual terms in a post-translation theory where a <code>later</code> modality is definable. This sounds rather close to your idea of working internally in the topos of trees.</p>

<p>It seems that they have a new, simpler Coq plugin implementing these ideas at <a href="https://github.com/CoqHott/coq-forcing/">CoqHott/coq-forcing</a>, and in particular <a href="https://github.com/CoqHott/coq-forcing/blob/master/theories/SI.v">SI.v</a> builds this forcing translation for step-indexing. Unfortunately, while it does the work of building the model, there is no example of using it for step-indexed definitions in practice (the only thing translated instead of defined in the forcing layer is <code>Forcing Translate eq</code>, which isn't terribly informative). You could try to experiment to see how (in)convenient this is to use.</p>

CC BY-SA 3.0
2016-04-14T15:29:03.147Z
2016-04-14T15:29:03.147Z
gasche
<p>One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured category.</p>

<p>For instance, Synthetic Differential Geometry has models in topoi that contain and embedding of the category of smooth manifolds, so you can use higher-order logic to construct smooth functions and solve differential equations.</p>

<p>As another example, in <a href="http://arxiv.org/abs/1208.3596" rel="noreferrer">this paper</a>, they notice that "step-indexing" is really just working with presheaves over the naturals (another topos), so you can use the syntax of higher order logic to define step-indexed logical relations without the tedious manipulation of steps.</p>

<p>Finally, Andrej Bauer shows in <a href="https://mathoverflow.net/questions/124991/what-can-be-expressed-in-and-proved-with-the-internal-logic-of-a-topos/126492#126492">this MO question</a> that you can do a lot with the "internal language" of the topos of graphs.</p>

<p>My question is, <strong>has anyone realized this vision literally in a theorem prover</strong>?
For instance, if I show that a category I care about is Cartesian Closed, I could then move to "internal mode" where I write lambda-calculus syntax (with some model-specific axioms) and then can move back to "external mode" and manipulate them as objects in my model?</p>

<p>In the extreme I would even want topos theory and higher-order logic, so I could write my step-indexed logical relations without steps, or teach classical mechanics with a theorem prover using SDG. This seems to me to be a very powerful idea as someone could implement extensional dependent type theory once and provide nice tooling and then use it with wildly different applications as described above.</p>

CC BY-SA 3.0
2016-04-10T15:05:55.127Z
Just for the sake of clarity: are you asking whether anyone has ever rewritten a mathematical theory in the internal language of the underlying category  (for using theorem prover to prove stuff on such math-theories)? Or are you interested in knowing if anyone have done *model theory* in the type theory  (of some kind of category) ?
Giorgio Mossa
CC BY-SA 3.0
2016-04-11T15:22:19.990Z
I'm not asking about work people have done in a particular internal language in a theorem prover (though references for that would be welcome). I'm asking if someone has done the work of implementing "Internal Languages" as essentially DSLs in a theorem prover so I can use the internal language for *any* particular model that I'm interested in and get all the benefits of a nice syntax. For CCCs this seems easy since the syntax can be easily expressed in Coq/Agda etc but Topoi seems more difficult.
Max New
CC BY-SA 4.0
2021-01-25T23:22:21.960Z
It has been four years since this question was asked... Recently I started thinking about this as well, and it seems like the internal-external translation is quite analogous to metaprogramming by reflection (the "external" form is a deep embedding, and the internal form is a shallow embedding). I wonder if work in the spirit of MetaCoq can make this easier.
xrq
<reference-request><pl.programming-languages><type-theory><ct.category-theory><constructive-mathematics>
Implementing "Internal" Languages
Max New
# Implementing "Internal" Languages

(Asked by: username_0 on 2016-04-09)

One of the most practical consequences of the "Curry-Howard-Lambek" correspondence is that the syntax of many lambda-calucli/logics can be used to perform constructions in a sufficiently structured category.

For instance, Synthetic Differential Geometry has models in topoi that contain and embedding of the category of smooth manifolds, so you can use higher-order logic to construct smooth functions and solve differential equations.

As another example, in [this paper](http://arxiv.org/abs/1208.3596), they notice that "step-indexing" is really just working with presheaves over the naturals (another topos), so you can use the syntax of higher order logic to define step-indexed logical relations without the tedious manipulation of steps.

Finally, Andrej Bauer shows in [this MO question](https://mathoverflow.net/questions/124991/what-can-be-expressed-in-and-proved-with-the-internal-logic-of-a-topos/126492#126492) that you can do a lot with the "internal language" of the topos of graphs.

My question is, **has anyone realized this vision literally in a theorem prover**?
For instance, if I show that a category I care about is Cartesian Closed, I could then move to "internal mode" where I write lambda-calculus syntax (with some model-specific axioms) and then can move back to "external mode" and manipulate them as objects in my model?

In the extreme I would even want topos theory and higher-order logic, so I could write my step-indexed logical relations without steps, or teach classical mechanics with a theorem prover using SDG. This seems to me to be a very powerful idea as someone could implement extensional dependent type theory once and provide nice tooling and then use it with wildly different applications as described above.

**Tags:** reference-request, pl.programming-languages, type-theory, ct.category-theory, constructive-mathematics
> **Comments:**
> **username_1**: Just for the sake of clarity: are you asking whether anyone has ever rewritten a mathematical theory in the internal language of the underlying category  (for using theorem prover to prove stuff on such math-theories)? Or are you interested in knowing if anyone have done *model theory* in the type theory  (of some kind of category) ?  
> **username_0**: I'm not asking about work people have done in a particular internal language in a theorem prover (though references for that would be welcome). I'm asking if someone has done the work of implementing "Internal Languages" as essentially DSLs in a theorem prover so I can use the internal language for *any* particular model that I'm interested in and get all the benefits of a nice syntax. For CCCs this seems easy since the syntax can be easily expressed in Coq/Agda etc but Topoi seems more difficult.  
> **username_2**: It has been four years since this question was asked... Recently I started thinking about this as well, and it seems like the internal-external translation is quite analogous to metaprogramming by reflection (the "external" form is a deep embedding, and the internal form is a shallow embedding). I wonder if work in the spirit of MetaCoq can make this easier.  

---

## 2 answers

### Answer by username_6 on 2016-04-14. Score: 7 | Accepted answer

In [Extending Type Theory with Forcing](https://hal.inria.fr/hal-00685150) by Guilhem Jaber, Nicolas Tabareau and Matthieu Sozeau, 2012, intuitionistic forcing is presented as an internalization of the presheaf construction, [implemented](https://github.com/mattam82/Forcing) as a type-preserving translation in the style of Bernardy and Lasson's [parametricity translation](https://who.rocq.inria.fr/Marc.Lasson/articles/RealParam/RealParam.pdf).

This means that you can define terms in your usual type theory, and then "translate them" into a "forcing layer" where they are interpreted as translations at a different translation type. For example, the translation induced by indexing over decreasing natural numbers lets you use your usual terms in a post-translation theory where a `later` modality is definable. This sounds rather close to your idea of working internally in the topos of trees.

It seems that they have a new, simpler Coq plugin implementing these ideas at [CoqHott/coq-forcing](https://github.com/CoqHott/coq-forcing/), and in particular [SI.v](https://github.com/CoqHott/coq-forcing/blob/master/theories/SI.v) builds this forcing translation for step-indexing. Unfortunately, while it does the work of building the model, there is no example of using it for step-indexed definitions in practice (the only thing translated instead of defined in the forcing layer is `Forcing Translate eq`, which isn't terribly informative). You could try to experiment to see how (in)convenient this is to use.


---

### Answer by username_3 on 2016-04-09. Score: 5

If you're going to work *only* in the internal language then you can just use a proof assistant. There is a minor technicality of having or not having powersets, since proof assistants are typically type theories, but Coq's `Prop` is consistent with an interpretation of Coq in a topos.

You're suggesting however to use the machine as a sort of translation tool that would get you from the internal language to the interpretation in a model. This is a fine idea, except I think it would not be as useful as one might expect. It is true that the translation from the internal language to the model is mechanical, but unfortunately it produces convoluted translations that need a lot of massaging before they're useful. (If you ever tried to use the Lawvere-Tierney interpretation of topos logic in a sheaf topos you'll know.)

There is one more problem, namely the *reverse* translation. We often start with a known concept or object in the model, and would like a good description or axomatization of it in the internal language. This is typically hard work and real math. I do not see how current proof assistants could help.

On the technical side of things one would have to worry about formalizing:

* the syntax and the rules of the internal language
* the model
* the interpretation

That is a lot of work, too. Some projects along these lines have been done (for instance the interpretation of $\lambda$-calculus in a cartesian closed category). I am not aware of anyone formalizing toposes, for instance.

In summary, using a proof assistant to help check that you're not doing anything wrong in the internal language is a good idea (in fact, it is a *very* good idea, as attested by homotopy type theory, where we used Coq and Agda to develop new theorems which were only later unformalized into English), but using it to get statements about models is unlikely to work without a lot of extra work. Which is not to say that you shouldn't try!

> **Comments:**
> **username_0**: Do you have a reference for Type Theory + Prop ~~ topos? This was my intuition but I haven't seen anyone else say it until now.  
> **username_0**: Also, for model-specific logics, specific *axioms* will be specific to the models but the structure of the logic overall is still just higher-order logic, right? I'm imagining that you would externally characterize features of your model (like the Next-time functor in the step-indexing paper) and then just reflect them as axioms in your internal language. Coming up with **nice** and **complete** axiomatizations would still be hard math but my hope is that the machine can automate some of the plumbing.  
> **username_3**: For step-indexing in particular it would make sense to extend the topos logic with a modal operator. This will in general be a feature of any situation in which you care about a subtopos, or you have a (co)monad that you want to study, etc.  
> **username_3**: For the Type theory + Prop, you just stare at every rule and see that if you interpret Prop as the subobject classifier, it's all valid in a topos.  
> **username_4**: The problem with this approach is that adding new axioms doesn't compute well. This mostly works for classical math but it's not so helpful for constructive math. I guess rewrite rules could help. Another problem is that topos is a rather strong construction. It would be nice to figure out internal languages of more limited categories. Also just adding axioms isn't so great for reflection. Would be nice to work some of this stuff into compilers and interpreters.  
> **username_3**: @MolossusSpondee: What does "this approach" refer to? I never mentioned any axioms, and if you're referring to Max New's comment, I think you misunderstood the meaning of "axioms" there. We're not talking about the addition of uninterpreted constants in type theory, although even that can be quite useful. Computation and constructivity aren't dogmas.  
> **username_5**: Could you elaborate a bit about the issues with the Lawvere-Tierney interpretation in a sheaf topos? With my current knowledge, this seems analogous to doing topology using Kuratowski closures instead of the standard approach with open subsets. but even if that's true I still don't appreciate the difficulties.  
> **username_3**: @SomaticCustard: It's just a fact that unfolding the Lawvere-Tierney interpretation in a sheaf topos quickly leads to very uwieldy formulas. I should however point out that since I wrote the answer in 2016 there have been some cool developments, both in terms of proof assistants supporting sheaf semantics (Coq in particular), and people actually coding up models (the HoTT0 project in Lean). And also, one can probably go some distance by using the j-operators as modal operators and do modal logic.  
> **username_5**: @AndrejBauer Ok, thank you! My mind certainly goes toward modal operators (and I've seen recommendation to call it LT modality instead of topology), but I have little experience with modal logic anyhow. Would Agda be unsuitable for this stuff? I settled on it having the least drawbacks of all proof assistants, but I keep seeing counterpoints. This deserves its own question...but you would probably be my top choice of answerer anyway!  

---

