search

agda / cubical

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

Simplify proof that cong ⟨_⟩ is injective on groups #1134

Closed ecavallo closed 3 weeks ago

ecavallo commented 3 weeks ago

We can use declareRecordIsoΣ for this.

felixwellen commented 3 weeks ago

Thanks @ecavallo ! I'll merge it....