Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

update reference to first path induction #1676

Closed
louisGarde opened this issue Oct 31, 2022 · 3 comments
Closed

update reference to first path induction #1676

louisGarde opened this issue Oct 31, 2022 · 3 comments

Comments

@louisGarde
Copy link

louisGarde commented Oct 31, 2022 •
edited
Loading

The last paragraph in the Notes of chapter 1 states:
The path induction principle for identity types was formulated by Martin-Löf [ML98]
However it seems that the paper [ML98] does not mention identity types.
According to Evan Cavallo, the identity type first appears in Martin-Löf's similarly-named 1975 paper, section 1.7.
@mikeshulman
Copy link
Contributor

This is the Coq repository, not the book repository. See HoTT/book#1129.

@Alizter
Copy link
Collaborator

Alizter commented Oct 31, 2022

Maybe it would be a good idea to rename the repo to say coq-hott? Given that is how we distribute the opam package and it is much clearer than HoTT/HoTT. GitHub let's you do this and also redirect links to HoTT/HoTT to the new name.

@Alizter
Copy link
Collaborator

Alizter commented Oct 31, 2022

AFAIK nobody would have to do anything in their local repos.

@mikeshulman mikeshulman mentioned this issue Oct 31, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@mikeshulman @Alizter @louisGarde