Replies: 2 comments
-
|
https://hal.inria.fr/hal-03367052v4/document This is a very good summary of the OTT research, with a predicative universe of strict proposition. |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Learn about observational equality by McBride or cubical extension type (either cartesian or de morgan)
Beta Was this translation helpful? Give feedback.
All reactions