Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Curious that you don’t list the initiality-issue. (Not that I think you should, but curious that you don’t.) By the way, we have a page on that: initiality conjecture, but entirely written by me. Some TT might want to look over it.
In the section “In cohesive homotopy type theory” (here) I have:
added a pointer to cohesive homotopy type theory
removed the last two items, as they were too far-out (“formalize -Chern-Weil theory”, and “formalize 3+1 d electromagnetism”)
instead I added pointer to the original:
defining higher inductive types in higher observational type theory is an open problem
Anonymous
@Urs I think all the the main hold-outs who believed initiality to remain unresolved have been all convinced by Taichi Uemura’s doctoral thesis, which gives a more detailed and mathematically satisfactory alternative to Cartmell’s 1978 proof for a broader class of theories — a class that includes homotopy type theory, cubical type theory, and many other type theories.
All right, thanks! I have added these references and your comment at initiality conjecture: here. Please feel invited to adjust.
Could you say which page/Proposition number in Cartmell 1978 you are referring to? I see him discuss categorical semantics of ML type theory in Chapter 3, but I have trouble identifying something like the initiality statement. Or is it left implicit in the statement that the semantics is algebraic?
a more detailed and mathematically satisfactory alternative to Cartmell’s 1978 proof for a broader class of theories
Could you clarify what you mean by “mathematically satisfactory”? While inelegant, Cartmell’s work certainly seems sound and expressive, so for that reason it seems entirely satisfactory. The proofs are also very detailed. I think it would be better simply to say that Uemura’s work is more elegant and/or categorical.
What evidence is there that Uemura’s framework captures theories that GATs do not?
Re. #9. Cartmell never states an “initiality theorem” of the kind described in initiality conjecture, but it is fairly straightforward to see how specific type theories may be encoded as GATs. The equivalence between GATs and contextual categories thereby provides an initiality theorem (§2.4 of Cartmell’s thesis).
Thanks! That’s what I figured: I had added Cartmell’s thesis to the references here, with a brief comment in this direction. But experts should please feel invited to expand.
@varkor I didn’t mean anything too harsh, I just felt that Cartmell’s proofs were a bit breezy and low-abstraction. But I have been fully satisfied with the correctness of Cartmell’s results for as long as I have been aware of them.
Re: the question of whether Uemura’s framework captures theories that GATs don’t, it’s a bit more complicated than that as one is comparing to very different ways to formalize a given type theory. In one case, you use the framework to handle binding (which Uemura’s framework has and GATs don’t). But note that Uemura’s framework is itself (roughly) a GAT, so you can always formalize a type theory as a GAT by first formalizing it in the Uemura framework. That is very similar, in fact, to how all formalizations of type theories as GATs work: you formalize the data of a category of contexts, and the data of a cwf on top of that. In the Uemura framework, the category of context is derived from the signature rather than being part of the signature.
I hope that clarifies the relationship between the two frameworks.
To give another analogy, elementary topoi are generalized algebraic; thus the “theory of a topos equipped with constants drawn from the higher-order signature Sigma” is also generalized algebraic. Nonetheless, the signature Sigma is not presenting a generalized algebraic theory.
Some open problems listed in the article
Anonymous
Moving problem
- Does having an interval type with only typal beta conversion rules and function types with only typal eta conversion rules imply function extensionality?
from objective type theory section to metatheory section, since iirc this problem is still unresolved even in the context of Martin-Löf type theory.
Anonymous
specified that the type theory in the problem
Define semi-simplicial types in type theory, or show that this is not possible. Define Segal space complete Segal space.
is single-level non-modal dependent type theory. Otherwise, one already has two-level type theory, simplicial type theory, displayed type theory for which one can construct semi-simplicial types or Segal spaces and complete Segal spaces.
Anonymouse
If we were to have a section on linear homotopy type theory, which open problems could we include? Presumably many results on linear representations.
Defining spectra and -rings, and results from spectral algebraic geometry.
The linear types of LHoTT already “are” spectra (synthetic spectra: they behave like spectra). One problem is to construct such linear types from a sequential spectrum of ordinary types.
Defining -ring structure on linear types will currently run into the same unresolved coherence issues that defining -structure on ordinary types ran into.
1 to 26 of 26