You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
OTT makes equality compute on the type, so that we get stuff like “equality of functions is pointwise equality” by definition. This seems like what we want, for convenience of matching on constructors in particular (e.g. finsets for constructor names like #{ .zero, .succ }).
OTT would restrict the models we have, in particular it rules out Univalence, and the question is do we care?
No description provided.
The text was updated successfully, but these errors were encountered: