search

agda / cubical

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

A small lemma on equivalences #897

Closed felixwellen closed 2 years ago

felixwellen commented 2 years ago

Just one proof, that a retract of an equivalence is itself an equivalence.

felixwellen commented 2 years ago

I added the symmetric statement. Because I messed up and that was what I actually needed - but I guess its better to have both anyway.