Questions tagged [homotopy-type-theory]

For questions about the field of study known as homotopy type theory.

6 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
9
votes
0answers
237 views

Model of Coq (pCuIC) in higher toposes?

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 ...
6
votes
0answers
109 views

Programmatic higher inductive/inductive-inductive types with equalities between equalities

I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and ...
4
votes
0answers
149 views

Model of homotopy type theory where propositional & judgmental equality coincide for closed terms

In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal. Is there a non-empty model of homotopy type theory ...
4
votes
0answers
321 views

Category theory in plain MLTT

I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of: a type of objects with equivalence relation (Obj : Set) a type of arrows ...
3
votes
0answers
115 views

Abstract stone duality and cohesive homotopy type theory

I have been reading the real-cohesive homotopy type theory paper and one of the remarks has sparked an interest. In this paper a string of monadic and comonadic modalities is introduced together with ...
3
votes
0answers
90 views

Request for an update on a discussion about coinductive types in HoTT (or anywhere else)

Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...