Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes? First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is expected to work. Shulman has shown that type theory with W-types can be interpreted in higher Grothendieck toposes. Inductive families 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 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 can be interpreted in HoTT, but I am not aware of a reduction of Coq's co-inductive types to M-types.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.