Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. copied from HoTT wiki

    Anonymous

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJun 6th 2022

    The first problem in the list has been solved!

    diff, v3, current

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

    diff, v3, current

    • 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:

    diff, v5, current

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

    Anonymous

    diff, v8, current

    • 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

    All right, thanks! I have added these references and your comment at initiality conjecture: here. Please feel invited to adjust.

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

  3. adding a few open questions about cubical type theory

    Stefani Germanotta

    diff, v9, current

  4. Some open problems listed in the article

    Anonymous

    diff, v10, current

  5. Moving problem

    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

    diff, v13, current

  6. The problem mentioned in last edit could also have definitional eta rule for function types, and it would still be unsolved.

    Anonymous

    diff, v13, current

  7. What was posed of the interval type with typal computation rules also applies to the propositional truncation of the booleans with typal computation rules

    Anonymous

    diff, v14, current

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

    diff, v26, current

    • CommentRowNumber21.
    • CommentAuthorAli Caglayan
    • CommentTimeFeb 21st 2024

    Hurewicz theorem in HoTT is solved

    diff, v27, current

    • CommentRowNumber22.
    • CommentAuthorAli Caglayan
    • CommentTimeFeb 21st 2024

    Add the loop space of a hset indexed wedge of circles to solved problems list.

    diff, v27, current

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 21st 2024

    If we were to have a section on linear homotopy type theory, which open problems could we include? Presumably many results on linear representations.

  9. Defining spectra and E E_\infty-rings, and results from spectral algebraic geometry.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeFeb 21st 2024

    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 E E_\infty-ring structure on linear types will currently run into the same unresolved coherence issues that defining A A_\infty-structure on ordinary types ran into.