search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

elimProp for the FreeCommAlgebra HIT #1035

Closed MatthiasHu closed 1 year ago

MatthiasHu commented 1 year ago

This PR replaces the huge repetitive proveEq lemma in FreeCommAlgebra.Properties by a simpler, more general and somewhat shorter (but also repetitive) elimProp eliminator.

felixwellen commented 1 year ago

Thanks! I wanted to have/do this for a long time...