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!
1 to 30 of 30