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 beauty bundles calculus categories category category-theory chern-weil-theory cohesion 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 education elliptic-cohomology enriched fibration foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry 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 homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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 subobject 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).
    • 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
    • CommentTimeMay 16th 2019

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

    diff, v17, current

    • CommentRowNumber18.
    • CommentAuthoratmacen
    • CommentTimeMay 16th 2019

    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
    • CommentTimeMay 16th 2019

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

    diff, v18, current

    • CommentRowNumber20.
    • CommentAuthoratmacen
    • CommentTimeMay 16th 2019

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

    diff, v18, current

    • CommentRowNumber21.
    • CommentAuthoratmacen
    • CommentTimeMay 17th 2019

    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
    • CommentTimeMay 19th 2019

    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
    • CommentTimeMay 19th 2019

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

    diff, v26, current

    • CommentRowNumber24.
    • CommentAuthoratmacen
    • CommentTimeMay 19th 2019

    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
    • CommentTimeMay 20th 2019

    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
    • CommentTimeMay 20th 2019

    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
    • CommentTimeMay 20th 2019

    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
    • CommentTimeMay 20th 2019
    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
    • CommentTimeMay 20th 2019

    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
    • CommentTimeMay 20th 2019

    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
    • CommentTimeMay 20th 2019

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

    • CommentRowNumber32.
    • CommentAuthoratmacen
    • CommentTimeMay 21st 2019

    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
    • CommentTimeMay 21st 2019

    Probably depends on what you’re trying to do.

    • CommentRowNumber34.
    • CommentAuthoratmacen
    • CommentTimeMay 28th 2019

    Greatly expanded “Idea” section, with more discussion about the “why” and “how” of CLF, gist of the expected proof system, and connection to Cedille. Also, an extra reference, about proof checking.

    diff, v31, current

    • CommentRowNumber35.
    • CommentAuthoratmacen
    • CommentTimeMay 30th 2019

    Noting that on-the-fly realizer extraction, aka dependent proof refinement, is also implemented in RedPRL, and is apparently a style of elaboration.

    diff, v37, current

    • CommentRowNumber36.
    • CommentAuthoratmacen
    • CommentTimeMay 31st 2019

    Expanded the “Idea/Method” subsection with explanation of how checking proof terms relates to tactic engines.

    diff, v38, current

    • CommentRowNumber37.
    • CommentAuthoratmacen
    • CommentTimeJun 1st 2019

    Added section about how “constructive”, “intuitionistic”, and classical propositions are represented in CLF (and also Nuprl), along with discussion of the difference between constructive and intuitionistic in this sense.

    diff, v40, current

    • CommentRowNumber38.
    • CommentAuthoratmacen
    • CommentTimeJun 8th 2019

    Cleaned up and slightly expanded the explanation about nonadmissibility of strengthening.

    diff, v43, current

    • CommentRowNumber39.
    • CommentAuthoratmacen
    • CommentTimeJun 9th 2019

    Finally started adding stuff about logical frameworks.

    diff, v44, current

    • CommentRowNumber40.
    • CommentAuthoratmacen
    • CommentTimeJun 9th 2019

    I probably ought to split this page up. Also, a lot of the stuff on logical frameworks should probably be on logical framework.

    • CommentRowNumber41.
    • CommentAuthoratmacen
    • CommentTimeJun 12th 2019

    Finally put stuff in “PER theory”, although it’s not the material I was originally planning to put there. For now, it explains refinement-style quotients.

    diff, v50, current

    • CommentRowNumber42.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 12th 2019

    atmacen, are you Matt Oliveri?

    • CommentRowNumber43.
    • CommentAuthoratmacen
    • CommentTimeJun 12th 2019
    Yes.
    • CommentRowNumber44.
    • CommentAuthoratmacen
    • CommentTimeJun 23rd 2019

    Filled in the LF= section. Improved the reference to Andromeda. (There’s now also an arXiv link.)

    diff, v53, current

    • CommentRowNumber45.
    • CommentAuthoratmacen
    • CommentTimeJul 4th 2019

    Finished filling in the sections on logical frameworks.

    diff, v56, 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)