search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

fix universes in vector #1988

Closed Alizter closed 3 months ago

Alizter commented 3 months ago

With a little bit of help, we can get Coq to minimize the number of universes it uses for Vector.v.