search

agda / cubical

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

Dependent Version of Bi-Invertible Equivalences #1062

Closed kangrongji closed 9 months ago

kangrongji commented 11 months ago

Some facts about dependent bi-invertible maps. They are useful to deal with HITs with bi-invertible maps constructors, for example, the BiInvInt.