search

agda / cubical

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

Fin (suc n) ≡ Maybe (Fin n) #880

Closed MatthiasHu closed 2 years ago

MatthiasHu commented 2 years ago

This PR proves a small property of the Fin datatype in Cubical.Data.FinData:

finSuc≡Maybe : Fin (ℕ.suc n) ≡ Maybe (Fin n)

and also a pointed variant of that.