Lemma on AlgebraEquivs - Githubissues

agda / cubical

An experimental library for Cubical Agda

Other

454 stars 139 forks source link

Closed felixwellen closed 2 years ago

felixwellen commented 2 years ago

Two small things:

inverse of an AlgebraEquiv
precomposition with an AlgebraEquiv, is an equivalence on the hom-types (which are not algebras)