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

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• 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 $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”.

• 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

• 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

$\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]$.

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

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

• 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!