Exercise 4.6: qinv-univalence #10

Open
opened 2023-05-18 08:27:33 +00:00 by michael · 0 comments
Owner

I was reading the HoTT book and noticed that this exercise helps walk through why not use qinv to define the equivalence used in univalence.

This may be good to look at in particular in the future

I was reading the HoTT book and noticed that this exercise helps walk through why not use `qinv` to define the equivalence used in univalence. This may be good to look at in particular in the future
michael added the
exercise
label 2023-05-18 08:27:33 +00:00
michael added this to the (deleted) project 2023-05-18 08:27:33 +00:00
michael modified the project from (deleted) to research 2024-05-24 01:34:36 +00:00
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: michael/type-theory#10
No description provided.