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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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