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-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry goodwillie-calculus graph graphs gravity grothendieck group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal-logic model model-category-theory monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory 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-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topological 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).
    • CommentRowNumber1.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    For now, a place to try putting some typing rules for proto CLF.

    v1, current

    • CommentRowNumber2.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Shoot. Bad itex command guessing. Do not read this revision.

    diff, v3, current

    • CommentRowNumber3.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Hope this makes things readable.

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    have equipped a bunch of keywords with hyperlinks

    diff, v4, current

    • CommentRowNumber5.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019
    Thanks!
    • CommentRowNumber6.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    type checking is currently a redirect to decidability, so I merged those links. I also added my name, since this is my work.

    diff, v5, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    Okay, good.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    have added a table of contents and a floating context menu

    diff, v6, current

    • CommentRowNumber9.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Why are these rules appearing in such a small font? And how do I make a line break? (Am trying to look into this; just recording my problem.)

    diff, v7, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    You make a line break by typing

      \linebreak
    

    Regarding typesetting the deduction rules: I seem to remember that Todd had looked into this at some point and found a good solution. But I forget where and how. (Once we remember, we should record this at HowTo…)

    • CommentRowNumber11.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    Using double-dollar-sign itex blocks. Fixes the font size of the rules. Probably shoulda known.

    diff, v9, current

    • CommentRowNumber12.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019
    Oops. But then consecutive rules don’t have enough space between them.
    • CommentRowNumber13.
    • CommentAuthoratmacen
    • CommentTimeMay 14th 2019

    \linebreak works to put space between rules, but it’s too much space. Better than too little.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 14th 2019

    I do believe there was a decent solution, but I didn’t pay attention back then. Maybe open a thread with the question, so that people see it.

    • CommentRowNumber15.
    • CommentAuthoratmacen
    • CommentTimeMay 15th 2019

    Fixed references for equality formation and PER comprehension.

    diff, v11, current

    • CommentRowNumber16.
    • CommentAuthoratmacen
    • CommentTimeMay 15th 2019

    I think that does it for the rules!

    diff, v14, current

    • CommentRowNumber17.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    Whoops, forgot the variable rule! (Because I was copying from HOAS rules.)

    diff, v17, current

    • CommentRowNumber18.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    From another thread, which changed subject to conservativity of Nuprl-style systems:

    Can you save me some time by pointing out exactly how the inductive definition of A.3 differs from, say, MLTT+UIP, or whatever intrinsically typed system it is easiest to compare it to?

    Looking at A.3 more closely now (it’s been a while since I read it carefully), I’m remembering how weird those rules are. What I call reflexivity is (usually?) admissible, not a rule. On A.3.16, introduction is like the CLF “selectivity” rules. because is obviously unsound; it’s like Coq’s Admitted. Elimination rules tend to be sequent-style “left rules”, rather than the usual MLTT style. Universes and inductive types (rectype) won’t work; ignore. Atoms and integers should be sufficiently similar to natural numbers.

    I guess the first thing to compare it to would be ETT (or MLTT+UIP) with Pi, funext, Sigma, empty type, natural numbers, lists, regular propositional truncation, and quotients. Actually, I guess regular propositional truncation is definable from the other stuff.

    In your prototype CLF, to start with I have no idea what “CompComp” would mean in categorical semantics.

    My question is not about finding categorical characterizations of all the type constructors, but whether it’s a conservative extension of ETT. The CompComp type is not in ETT, so conservativity doesn’t say anything about that. (I think the other CLF type constructors have order theoretic characterizations relative to CompComp. Like a function type is the greatest type of apply-able computations.)

    For a possible analogy, material and structural set theories have different styles, but if you translate propositions from structural to material set theory, is there a difference in provability?

    • CommentRowNumber19.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    Discussion of admissible rules, and a bunch of empty sections I ought to fill.

    diff, v18, current

    • CommentRowNumber20.
    • CommentAuthoratmacen
    • CommentTime7 days ago

    Five-hash subheadings make the text too small. :(

    diff, v18, current

    • CommentRowNumber21.
    • CommentAuthoratmacen
    • CommentTime6 days ago

    Removed the “Discussion” section, hoisting out the subsections, because most of the sections are discussion, and they were too deeply nested.

    diff, v21, current

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTime4 days ago

    Ok, well, in the other thread you said

    it’s not clear to me that Nuprl isn’t already a conservative extension. Do you know some incompatibility besides unusual types and funky type equality?

    I guess my answer is that the entire frameworks are prima facie incompatible. If you think there should be a conservativity result, the onus is on you to prove it.

    • CommentRowNumber23.
    • CommentAuthoratmacen
    • CommentTime4 days ago

    Clarification of “not all functions are lambdas”: proto CLF does satisfy an eta rule for function types.

    diff, v26, current

    • CommentRowNumber24.
    • CommentAuthoratmacen
    • CommentTime3 days ago

    If you think there should be a conservativity result, the onus is on you to prove it.

    Of course. I was wondering two things:

    • If you could spot any counterexamples. (I can’t.)
    • If conservativity would remove the problem of it being based on a particular semantics.
    • CommentRowNumber25.
    • CommentAuthoratmacen
    • CommentTime2 days ago

    It occurred to me that curly braces was an awful choice of notation for squash, since set theory uses that for singleton sets. BTW, singleton types are ambiguous: you also need to specify equality. But still.

    diff, v27, current

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTime2 days ago

    I don’t immediately see any counterexamples, but I haven’t really looked. A conservativity result might resolve the semantic problem, though it might depend on the precise form of the result.

    • CommentRowNumber27.
    • CommentAuthoratmacen
    • CommentTime2 days ago

    I’ve been too vague about what I want the result to actually say. I don’t want to commit to a precise formulation because I don’t know what features are needed from ETT to get anywhere.

    I think a way to say the gist of what I expect is that the full subcategory corresponding to the small types, of the syntactic category of ETT embeds into the syntactic category of an appropriate Nuprl-style system. The small types are the ETT types in the bottom universe, if the ETT has universes, otherwise it’s all of them.

    So there’s a syntactic translation from ETT terms to Nuprl-style terms. That part is clear once all the required type constructors are available on the Nuprl side. (Although it’s not shown (yet?), you can construct sigmas and coproducts in CLF.) So I think the translation, along with a proof that it preserves typing, is a functor, and the conservativity result makes it full and faithful.

    • CommentRowNumber28.
    • CommentAuthoratmacen
    • CommentTime2 days ago
    So I figure you could pick whatever semantics you like for the relevant ETT, and use the Nuprl-style system to reason about the elements of small types. But you can't use an axiom that uses a universe. (Since discharging the assumption makes the type large.)
    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTime2 days ago

    I’m not sure what you mean when talking about universes, but aside from that, yes I think if the syntactic category of one theory embeds full-faithfully in another one then that would be sufficient.

    • CommentRowNumber30.
    • CommentAuthoratmacen
    • CommentTime2 days ago

    Maybe my grammar was too weird. There are generally three categories involved: the syntactic category of an ETT, the syntactic category of a Nuprl-style system, and a full subcategory of small ETT types. The translation functor I have in mind is only an embedding of the small types.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTime2 days ago

    Hmm. One does generally want to prove things about large types too.

    • CommentRowNumber32.
    • CommentAuthoratmacen
    • CommentTime2 days ago

    The problem with large types (if my expectations are correct) is the universes. Nuprl-style universes are different from ETT universes. I’m wondering if that’s really a problem though, since neither kind of universe is univalent. They’re both arbitrary ways of coding for the “real” types, from a univalent perspective. Are ETT universes somehow preferable anyway?

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTime1 day ago

    Probably depends on what you’re trying to do.

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)