Not signed in (Sign In)

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

  • 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 beauty bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics 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 foundation foundations functional-analysis functor galois-theory 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 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 sheaves simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)