<p>Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes?
First of all, even the <a href="https://hal.inria.fr/hal-01952037/document" rel="noreferrer">set theoretical model</a> is not complete (e.g. inductive types in Prop). Although, this is expected to work.
<a href="https://arxiv.org/abs/1904.07004" rel="noreferrer">Shulman</a> has shown that type theory with W-types can be interpreted in higher Grothendieck toposes. <a href="https://ncatlab.org/nlab/show/inductive+family" rel="noreferrer">Inductive families</a> can be reduced to W-types. These are claimed to be similar to the inductive families of Coq. However, I am not sure I’ve ever seen a precise result along these lines.
<a href="https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf" rel="noreferrer">Voevodsky</a> has made a similar reduction for Coq’s inductive types, but I am not sure it’s entirely up to date, or complete. The note was never published. Moreover, it was written before pCuIC came out.
Finally, Coq also has co-inductive types. Again, <a href="https://ncatlab.org/nlab/show/M-type" rel="noreferrer">M-types</a> can be interpreted in HoTT, but I am not aware of a reduction of Coq's co-inductive types to M-types.</p>

CC BY-SA 4.0
2019-08-16T00:56:16.623Z
I guess pCuIC as in [Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)](https://arxiv.org/abs/1710.03912)?
David Roberts
CC BY-SA 4.0
2019-08-16T07:16:09.837Z
Ah, I see that looks to be a different version of the same paper.
David Roberts
<type-theory><coq><homotopy-type-theory>
Model of Coq (pCuIC) in higher toposes?
Bas Spitters
# Model of Coq (pCuIC) in higher toposes?

(Asked by: username_0 on 2019-08-13)

Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes?
First of all, even the [set theoretical model](https://hal.inria.fr/hal-01952037/document) is not complete (e.g. inductive types in Prop). Although, this is expected to work.
[Shulman](https://arxiv.org/abs/1904.07004) has shown that type theory with W-types can be interpreted in higher Grothendieck toposes. [Inductive families](https://ncatlab.org/nlab/show/inductive+family) can be reduced to W-types. These are claimed to be similar to the inductive families of Coq. However, I am not sure I’ve ever seen a precise result along these lines.
[Voevodsky](https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf) has made a similar reduction for Coq’s inductive types, but I am not sure it’s entirely up to date, or complete. The note was never published. Moreover, it was written before pCuIC came out.
Finally, Coq also has co-inductive types. Again, [M-types](https://ncatlab.org/nlab/show/M-type) can be interpreted in HoTT, but I am not aware of a reduction of Coq's co-inductive types to M-types.

**Tags:** type-theory, coq, homotopy-type-theory

> **Comments:**
> **username_1**: I guess pCuIC as in [Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)](https://arxiv.org/abs/1710.03912)?  
> **username_1**: Ah, I see that looks to be a different version of the same paper.  

---

## 0 answers

