# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. copied from HoTT wiki

Anonymous

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJun 6th 2022

The first problem in the list has been solved!

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJun 6th 2022
• (edited Jun 6th 2022)

The first problem in the list has been solved! Even with strict universes. This and related pages need some updating.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJun 6th 2022

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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeJun 6th 2022
• (edited Jun 6th 2022)

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 $\infty$-Chern-Weil theory”, and “formalize 3+1 d electromagnetism”)

2. defining higher inductive types in higher observational type theory is an open problem

Anonymous

• CommentRowNumber7.
• CommentAuthorjonsterling
• CommentTimeJul 20th 2022
• (edited Jul 20th 2022)

@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.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeJul 20th 2022

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeJul 20th 2022

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?

• CommentRowNumber10.
• CommentAuthorvarkor
• CommentTimeJul 20th 2022
• (edited Jul 20th 2022)

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?

• CommentRowNumber11.
• CommentAuthorvarkor
• CommentTimeJul 20th 2022

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).

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeJul 20th 2022

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.

• CommentRowNumber13.
• CommentAuthorjonsterling
• CommentTimeJul 21st 2022

@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.

• CommentRowNumber14.
• CommentAuthorjonsterling
• CommentTimeJul 21st 2022
• (edited Jul 21st 2022)

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.