Questions tagged [homotopy-type-theory]
Homotopy type theory is a flavor of type theory – specifically of intensional (Martin-Löf-) dependent type theory – which takes seriously the natural interpretation of identity types as formalizing path space objects in homotopy theory. (from nLab)
11
questions
1
vote
1
answer
158
views
Formalization of a model of ∞-category in a proof assistant
I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or ...
- 133
9
votes
1
answer
196
views
What is the intuition behind the `Glue` type in Cubical Type Theories
I have some clues regarding Glue based on a paper here and the accepted answer here.
The first resource says that Glue "...
- 345
11
votes
1
answer
225
views
Seven Trees in One, or How to formalize the Semiring of Types?
This is somewhat conceptual beginner's question about proof assistants.
I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary ...
- 213
8
votes
3
answers
240
views
When is hProp equivalent to the subobject classifier?
In the definition of an elementary topos, the "object of propositions" $\Omega$ is axiomatized by the universal property of a subobject classifier.
In homotopy type theory, we instead start ...
- 294
5
votes
1
answer
171
views
In HoTT, what is the hlevel of $S^1$?
I think there's an obvious fact that (base = base) = Z hence isSet (base = base) is inhabited. However, is it also true that <...
- 5,792
3
votes
1
answer
91
views
Can I specify `refl`'s parameter explicitly in Agda?
I'm working on some proofs in Agda that, for educational purposes, explicitly use the path induction principle (which I've defined myself) rather than pattern matching. In the theoretical mathematical ...
- 289
10
votes
1
answer
271
views
How does Prop relate to h-prop and double negation?
I'm referring to these concepts:
Prop in Agda and SProp in Coq, a "sort of definitionally proof-irrelevant propositions", and their squash type (and relatedly, the usual Prop in Coq);
mere ...
- 1,005
17
votes
2
answers
852
views
What are "fibration/cofibration" in type theory and what are their intuitions?
I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
- 181
8
votes
1
answer
204
views
Is there any universe polymorphic version of univalence?
People would say in univalent type theory, anything you defined for types should respect equivalence since univalence told you equivalence equivalent to equality. But that's not correct. Only ...
- 660
5
votes
0
answers
197
views
What would a fully classical and fully univalent ITP and library look like?
Consider two developments in dependent type theory:
Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
- 6,713
9
votes
1
answer
423
views
What is the state of the art in proof automation in HoTT/CuTT?
One of the frequent criticisms of HoTT is that it requires a lot of lemmata keeping track of which types are sets/propositions etc. And a frequent counterpoint is "It can be automated."
...
- 3,678