search

agda / cubical

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

Add `Π-contractDom` #1132

Closed ncfavier closed 5 months ago

ncfavier commented 6 months ago

Analogous to Σ-contractFst. Not sure where this should live; can't go in Cubical.Foundations.Function because of cyclic imports.