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 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 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 nforum 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 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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 20th 2011

    created types and logic - table and all the entries to complete it.

    Currently I am using this to include inside type theory - contents, which I keep reorganizing.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014
    • (edited Jan 20th 2014)

    have added two more lines related to linear logic to the “trinitarianism dictionary” types and logic - table

    Looking at this again now, I see that I have a complaint about one line in the table, I forget where this originates from, but the 5th line reads:

    logic category theory type theory
    classical type theory internal logic classical type theory, logic programming

    That doesn’t make sense to me. What’s the interntion here? Could we clarify this?

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeJan 20th 2014

    “Classical” in the first column probably means “extensional”.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014

    Okay, maybe that was the intention. In this case however I vote for removing that line, because this seems to make a distinction too fine-grained for the table. Later the table talks about object classifiers, after all.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 20th 2014

    I support removing that line entirely.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 20th 2014

    Thanks for the feedback, Todd! I am removing it now. We still can (and probably should) add more of what seems missing.

    By the way, there is another line which I don’t understand (or not anymore, I forget what happens. I believe that I created the bulk of this table, but others edited it, too):

    namely the line which under “logic” has “cut elimination” under “category theory” says “counit”. This at least needs more qualification, I’d think: counit of what?

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 20th 2014

    Actually, I’m not too keen on that line either, but it refers to a specific instance of cut-elimination that is related to the counit (AB)AB(A \multimap B) \otimes A \to B of the hom-tensor adjunction. In terms of terms, it refers to the reduction (λx.τ[x])(a)τ[x/a](\lambda x. \tau[x])(a) \rightsquigarrow \tau [ x/a ].

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 20th 2014

    Okay, I edited in what I said in #7, and filled in for a question mark. Having done that, I think these would probably read a little more nicely if instead of having the left-hand column written in the language of sequent calculus, we write it instead in the language of natural deduction (with introduction and elimination rules). But I’m not very fussed about it.

    I don’t really like the line with proof net in it – it seems slightly confused to me, or needs qualification of some kind or another. Let me think on it.

    • CommentRowNumber9.
    • CommentAuthorAli Caglayan
    • CommentTimeAug 11th 2018
    The table is broken at the moment. I tried a few trivial edits to format it like the other tables but it hasn't seemed to fix it. You can roll back all my edits. This table is used by other articles so it would be good if it can be fixed.
  1. Thanks for letting us know, I’ll take a look when I get the chance.

  2. Fixed table.

    diff, v32, current

    • CommentRowNumber12.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 12th 2018
    • (edited Aug 12th 2018)

    I also tweaked the file instiki.css to add a bit of padding to table cells and headings (for all tables in the nLab).

  3. I think general consensus amongst type theorists are that setoids/Bishop sets aren’t actually internal 0-groupoids; only the setoids/Bishop sets whose “relations” are (-1)-truncated are internal 0-groupoids. Also “type of type” -> “type universe”


    diff, v40, current

    • CommentRowNumber14.
    • CommentAuthormaxsnew
    • CommentTimeSep 29th 2022

    I think there are some rows in this table that are fundamentally wrong. For instance “cut elimination for implication” in logic is identified with the counit of the hom-tensor adjunction, but the counit instead corresponds most closely to the left rule for implication (even more directly the elimination rule in natural deduction). The third thing, beta-reduction does roughly correspond to the cut elimination for implication.

    Then in the next line, it identifies the introduction rule for implication with the unit of the hom-tensor adjunction, which is arguably correct but then this is identified with eta-conversion which doesn’t really make any sense.

    I think the right analogy would be

    intro rule for implication : counit : lambda elim rule for implication : unit : application cut elimination for implication : one of the zigzag identities : beta reduction identity elimination for implication : the other zigzag identity : eta conversion

    Where identity elimination is the less well known procedure where you show that the identity rule A |- A is admissible if you only assume it for base types. For instance A -> B |- A -> B is admissible by the term f : A -> B |- lambda x. f x : A -> B and the fact that this is an identity is the eta rule.

  4. changed rows regarding various rules for logical implication to the suggested changes by maxsnow in the nForum


    diff, v51, current