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)

Filter by
Sorted by
Tagged with
5 votes
1 answer
387 views

Unnecessary premises in a congruence rule of homotopy type theory?

In the HOTT book, p. 433 (Appendix A.2.2), we have a congruence rule with the three following premises: $\Gamma \vdash A : \mathcal{U}_i$ $\Gamma, x : A \vdash B : \mathcal{U}_i$ $\Gamma, x : A \...
Bruno's user avatar
  • 195
2 votes
2 answers
134 views

Can Hyperreal exist a axiom-free implementation in HoTT?

The main current implementations of hyperreal numbers are model-theoretic and set-theoretic approaches. Most of these implementations are strongly non-constructive, and many require a very deep ...
Ember Edison's user avatar
7 votes
1 answer
524 views

Benefits of HoTT compared with dependent type theory like what Lean does?

I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would ...
ch271828n's user avatar
  • 171
2 votes
1 answer
187 views

Higher Observational Type Theory: variables becoming free in reduction rules

This question is based on the talks given by Mike Shulman on higher observational type theory (part 1, part 2, part 3). In trying to understand the reduction rules of the calculus, I tried to work ...
idka's user avatar
  • 73
1 vote
2 answers
271 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 ...
TomR's user avatar
  • 133
9 votes
1 answer
272 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 "...
Russoul's user avatar
  • 345
11 votes
1 answer
276 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 ...
Dario's user avatar
  • 213
8 votes
3 answers
265 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 ...
Max New's user avatar
  • 304
5 votes
1 answer
189 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 <...
ice1000's user avatar
  • 6,144
3 votes
1 answer
124 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 ...
aradarbel10's user avatar
10 votes
1 answer
369 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 ...
James Martin's user avatar
  • 1,015
18 votes
2 answers
1k 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/...
Anqur's user avatar
  • 191
8 votes
1 answer
223 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 ...
KANG Rongji's user avatar
8 votes
0 answers
270 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 ...
Jason Rute's user avatar
  • 8,535
9 votes
2 answers
578 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." ...
Trebor's user avatar
  • 3,867