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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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).

nLab > Latest Changes: function application to identifications

Bottom of Page

1 to 10 of 10

  1.  

  1. Page created, but author did not leave any comments.

    Anonymous

    v1, current

  2. adding section on binary actions on identifications and the reference

    Anonymous

    diff, v6, current

  3. renaming page to make it more in line with the common terminology “identity” and “identity type”

    Anonymous

    diff, v8, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2023

    added a little bit of whitespace to this equation, in order to make the syntax binding more evident to the eye:

    a:A,b:A,p:a= Ab⊢ap f(a,b)(p):f(a)= Bf(b) a \colon A \,, b\colon A \,, p \colon a =_A b \;\;\vdash\;\; \mathrm{ap}_f(a, b)(p) \,\colon\, f(a) =_B f(b)

    This applies to other formulas, too, but I’ll leave it at that.

    diff, v9, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2023
    • (edited Jan 19th 2023)

    I have added more explicit pointers to section numbers in the references.

    The current title (“action on identities”) of this entry seems bad: I don’t think “action” is a good word for “application”, but certainly “identities” is misleading. And that’s also not what the cited literature says (the cited literature says “paths” or “identifications”).

    I vote for naming this entry “function application to identifications”.

    Or if “action” must be in the title, then “action on identifications”.

    diff, v11, current

  6. renamed it from “action” to “function application”, especially since notation used is ap f\mathrm{ap}_f given a function ff which makes more sense if the notation is “function application” rather than “action”.

    Anonymous

    diff, v12, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2023

    Thanks!

    So am taking the liberty then to also replace, in the title, the previous “identities” by “identifications”.

    (An “identity” is either an identity morphism which here would be refl, or else is a proposition asserting equality. In either case this is not what this entry is about.)

    diff, v15, current

  8. (An “identity” is either an identity morphism which here would be refl, or else is a proposition asserting equality. In either case this is not what this entry is about.)

    And for that reason I don’t like the name “identity type”, since it implies that its terms are called “identities”, similar to how terms of function types are functions, and terms of natural number types are natural numbers.

    I’d rather use “path type” or “identification type”. The word “identification” is used throughout the type theory literature but I have never seen “identification type” used in the type theory literature before. On the other hand, “path type” has been used in the literature, and makes sense as well since since every element of an identity type is given by a function from the interval type, but then in the context of cubical type theory one has to make the distinction between different notions of path type.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2023

    Very good. I am all for saying “Identification type”, as it’s clearly the right term: It is the data type of identification certificates.

    And while we are at it, am for:

    • writing “Id D(d 1,d 2)Id_{D}(d_1, \, d_2)” instead of “d 1= Dd 2d_1 =_D d_2”

      as this is suggestive notation, avoids the weird clash with equality, and is still readable when the nesting level increases,

    • writing “id did_d” instead of “refl drefl_d” and call it the self-identification

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 19th 2023

    I have added brief mentioning of the (∞\infty-)functoriality of ap fap_f and added an illustrating graphics of the 0th and first stage: here

    (This might want to go to a Properties-section, eventually, but given the structure of the entry at the moment, it seems most useful right here after the basic definition.)

    My graphics uses somewhat different notational conventions than this (or other) entries. If this is found confusing and people insist, I can adjust this, but maybe I can alternatively nudge “us” into adopting this convention.

    diff, v15, current

1 to 10 of 10

  1.