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 categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology 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 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 infinity integration-theory internal-categories k-theory kan lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology nonassociative 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 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.
    • CommentAuthorUrs
    • CommentTimeNov 18th 2011

    added to identity type a mentioning of the alternative definition in terms of inductive types (paths).

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 18th 2011

    Thanks! It’s not really an alternative definition, though, just an encompassing of the other definition into a general framework. Also, it predates HoTT by a lot. I edited the page some trying to clarify.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 18th 2011

    Ah, okay. That wasn’t clear to me. Thanks.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 13th 2011

    I have added to identity type some discussion of the stability/coherence obstacles to interpreting identity types categorically in a WFS, along with some more references.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    I added to identity type a discussion of how the definitional eta-conversion rule for identity types forces us into extensional type theory.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2012

    I wonder: is there a negative presentation of identity types?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2012

    at identity type in the section on categorical semantics I have added some actual details on how that proceeds. (to the existing discussion of what conditions on the ambient category we need for this.)

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 30th 2014

    For fun, I have given identity type a lead-in quote

    everything is identitcal with itself (WdL §863)

    no two things are like each other (WdL §903)

    Beyond being fun, it is reminiscent of how there is no way to prove equality than by reducing to reflection.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2014

    In a similar vein, I have been amused to notice that as Arthur grows up, one of the more difficult things for him to learn is that two things can be isomorphic without being identical (e.g. the beans on his plate and the beans on Dad’s plate).

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 30th 2014

    You do realise that you and Urs now have the perfect opportunity to see how children brought up in the HoTT spirit will think mathematically.

    Think how much harder at a later stage to work out how money works. Not only do they go through the stage of worrying about which particular coin they have, but that it’s treated as the same as combinations of coins.

    • CommentRowNumber11.
    • CommentAuthorNikolajK
    • CommentTimeDec 1st 2014

    David,

    Even in my daily life, I’m often confronted with how plain bijections are not good isomorphisms in the category of coins, closed under addition. If it were, it would spare me some NP-complete problems.

    Sure, everything I can buy with a 5er, I can also by with five 1’s. But if some machine takes two 1’s, I can’t use my 5er to get gum out of a machine. Its curious how money is partitioned into 1’s, 2’s, 5’s and 10-multiples of it. When I’m waiting in a cue, I always compute if I can generate all composites to pay “right”: With {1,2,2,5} you can pay 1,2,3,4,5,6,7,8,9. Funny how changing a 2 with a 1 only changes the upper bound, but not e.g your ability to produce 4. With more money, {1,5,5} say, you have far less options :) Having 11 units of money really isn’t just having 11 units of it. I was in Russia last month and when I ran out of money for some days, the boss of the firm we worked in said he’d help me out with some cash - of course I’d give him back whatever I didn’t need. Well, this guy then gave me a note worth a huge amount. I assume he meant the best, but to me it was an ass move as I just couldn’t break the note and give him back some small ones. He gave me too much and so he gave me nothing.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2014

    On my end, the Proceß has not expressed the moment of quantity yet, it still needs to sublate becoming into a more determinate being first. Also, I am still worried not so much about the identity type of beans as about it being inhabited at all.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2018

    Some of the βs and ηs had become \infty in links, so I fixed this.

    I guess we just live with using η-reduction, -conversion, -expansion interchangeably.

    diff, v40, current

  1. Thanks David! This one was my fault, sorry, again it’s related to the unicode issues. When I get the time to try to fix things once and for all, I’ll look out for occurrences of this one.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 2nd 2018

    As explained at the page eta-conversion, η\eta-reduction, η\eta-conversion, and η\eta-expansion are technically all slightly different things, though of course very closely related. η\eta-conversion is an undirected equivalence relation; η\eta-reduction and η\eta-expansion are the two opposite ways to “direct” this relation. Would it be useful to mention this point on the page identity type?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 2nd 2018

    I wonder if we use these consistently, e.g., at Extensionality and η-conversion.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018

    also pointer to Licata 11. Is that where the observation originates?

    diff, v41, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeAug 5th 2018
    • (edited Aug 5th 2018)

    Hm, it seems that my first edit-message did not get through:

    I had added pointer to Shulman 12 and was asking: Where is the origin of the observation that identity types are simply indctive type families generated by reflection?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2018

    Oh, way earlier than that. For instance, identity types are defined that way in Coq and have been since ever that I know of.

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)