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

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).
    • 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


    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

    (pq)pq\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:AB[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.

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

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

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2018

    Now a disambiguation page.

    diff, v9, current

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

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

  5. 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!

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)