search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

transport along a path is an equivalence #77

Closed TashiWalde closed 1 year ago

TashiWalde commented 1 year ago

Add two minor utilities which I couldn't find.

1) The identity function is an equivalence.

2) Transport along a path is an equivalence.