search

HoTT / Coq-HoTT

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

finite sums and modules #1975

Closed Alizter closed 4 months ago

Alizter commented 4 months ago

Some lemmas about finite sums of scalars and module elements and how the left action interacts with them.