3
$\begingroup$

In Martin-Löf type theory, the elimination form for identity types seems to always be called J. Is this short for something? Is it just because it's the letter after I? I can't find anything explaining why.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Yes, that is the most likely explanation (in fact the only one I'm aware of). See also Remark 4.2.3 in Principles of Dependent Type Theory.

Axiom K was then named for the next letter after J, and axiom L... you get the picture.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.