Univalence only needing ua and ua𝛽

vikraman / 2DTypes

Collaborative work on reversible computing

17 stars 1 forks source link

Univalence only needing ua and ua𝛽 #144

Closed inexxt closed 2 years ago

inexxt commented 3 years ago

Yes, surprisingly, ua and ua𝛽 give full univalence, and ua𝜂 is derivable. This is a folklore result known in the HoTT community. We will make sure to add a footnote.