5 votes

How to state and prove the associativity of append of sized vectors with homogeneous equality?

The equality has to be a "dependent equality" over the associativity of natural numbers n + (m + o) = (n + m) + o. Some libraries for univalent ...
Mike Shulman's user avatar
  • 3,040

Only top scored, non community-wiki answers of a minimum length are eligible