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

Discussion Tag Cloud

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: axiom K (type theory)

Bottom of Page

1 to 30 of 30

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2012
    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2012

    I suppose the axiom is due to

    • Thomas Streicher, Investigations into intensional type theory Habilitation thesis (1993) (pdf)

    I am adding that to the entry now.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 19th 2015

    added to axiom K the statement that the axiom is incompatible with univalence. Somebody please add a reference for this.

    • CommentRowNumber4.
    • CommentAuthorNikolajK
    • CommentTimeNov 3rd 2016

    The Axiom KK is entirely unrelated to

    K:(α→β)→αK:(\alpha \to \beta)\to \alpha

    right?

    On the Haskell-Curry corresponding page on Wikipedia this is also called Ax K{Ax}_K and this “K”, I assume, should come from “constant”.

    • CommentRowNumber5.
    • CommentAuthorspitters
    • CommentTimeNov 3rd 2016

    There are only 26 letters in the alphabet. It seems like an accidental collision to me.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2016

    Yes, I don’t think there is any relation.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeAug 20th 2018

    Add comments about computational behavior and pattern-matching

    diff, v8, current

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2018
    • (edited Aug 21st 2018)

    A more troubling clash than in #4 is with the Axiom K of modal logic

    □(p→q)→□p→□q\Box(p \to q) \to \Box p \to \Box q.

    I was just thinking about the latter since Bas Spitters has its dependent type theoretic lift as

    Dependent K: □Π y:AB(y)→Π x:□A□B[openx/y]\Box \Pi_{y:A} B(y) \to \Pi_{x: \Box A} \Box B [open x/y].

    Is that talked about elsewhere?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeAug 21st 2018

    I think in BFPRCoHoTT I didn’t consider dependent functoriality of ♭\flat.

    Should we make Axiom K a disambiguation page? Or add hatnotes pointing to the other meanings?

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2018

    Is the choice of K in your case standard now? In modal logic it’s been around for decades, named after Kripke I believe.

    It seems odd just to include mention of the modal case as a side note. We’d better disambiguate.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 21st 2018

    Yeah, this usage is standard in type theory.

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2018

    OK, so I’ll set up a disambiguation page and then create ’Axiom K (type theory)’ and ’Axiom K (modal logic)’.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeAug 22nd 2018

    To preserve history, the current page should really be moved to axiom K (type theory), with the disambiguation page being newly created. But it doesn’t currently seem to be possible to move pages.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeAug 22nd 2018

    Oh, I see maybe that bug is fixed now.

  15. Maybe one could have effectively moved by renaming axiom K to axiom K (type theory)?

  16. Re #14: Yes, the renaming bug should be fixed now.

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2018

    Now a disambiguation page.

    diff, v9, current

  18. I will delete axiom K (type theory) and carry out this renaming.

  19. Thanks David C! To preserve history, I will rollback temporarily. Please nobody edit any of the axiom K pages for a short time!

  20. Renaming old axiom K page to axiom K (type theory).

    diff, v10, current

    • CommentRowNumber21.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 22nd 2018
    • (edited Aug 22nd 2018)

    I have now finished tidying things up. The old axiom K is renamed to axiom K (type theory), and axiom K is now a disambiguation page. Hopefully this is what was intended.

    If you added anything to axiom K (type theory) during creating it David C, it will have been lost when I deleted it; could you check? Perhaps you had a disambiguation note at the top?

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2018

    Yes, it was only the disambiguation note. I can re-add that.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeAug 22nd 2018

    Thanks both!

  24. extensional -> set-level

    Anonymous

    diff, v14, current

  25. adding section about axiom K for individual types

    Anonymous

    diff, v15, current

  26. Edited introduction to distinguish between axiom K for individual types, axiom K for universes, and axiom K for the entire type theory.

    Anonymous

    diff, v15, current

  27. added a section about axiom K applying to the entire type theory

    Anonymous

    diff, v15, current

  28. added section about the definitional K rule

    Anonymous

    diff, v15, current

  29. added section on the relation between axiom K and univalence

    Anonymous

    diff, v15, current

  30. adding foundational axiom contents to sidebar

    Anonymous

    diff, v23, current

1 to 30 of 30

  1.