Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I suppose the axiom is due to
I am adding that to the entry now.
added to axiom K the statement that the axiom is incompatible with univalence. Somebody please add a reference for this.
The Axiom $K$ is entirely unrelated to
$K:(\alpha \to \beta)\to \alpha$
right?
On the Haskell-Curry corresponding page on Wikipedia this is also called ${Ax}_K$ and this “K”, I assume, should come from “constant”.
There are only 26 letters in the alphabet. It seems like an accidental collision to me.
Yes, I don’t think there is any relation.
A more troubling clash than in #4 is with the Axiom K of modal logic
$\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: $\Box \Pi_{y:A} B(y) \to \Pi_{x: \Box A} \Box B [open x/y]$.
Is that talked about elsewhere?
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?
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.
Yeah, this usage is standard in type theory.
OK, so I’ll set up a disambiguation page and then create ’Axiom K (type theory)’ and ’Axiom K (modal logic)’.
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.
Oh, I see maybe that bug is fixed now.
Maybe one could have effectively moved by renaming axiom K to axiom K (type theory)?
Re #14: Yes, the renaming bug should be fixed now.
I will delete axiom K (type theory) and carry out this renaming.
Thanks David C! To preserve history, I will rollback temporarily. Please nobody edit any of the axiom K pages for a short time!
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?
Yes, it was only the disambiguation note. I can re-add that.
Thanks both!
Following the discussion here, I have rolled back this entry to revision 11, the last one before a flood of edits signed by “Anonymous”
Judging by the unique writing style, the Anonymous author whose edits are now rolled back seems to be the one now signing as “Anonymouse”, after we blocked the plain “Anonymous” for their flood of low-quality edits, and for never replying and reacting to comments.
1 to 31 of 31