search

rzk-lang / sHoTT

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

equivalences induced by concatenation #49

Closed emilyriehl closed 1 year ago

emilyriehl commented 1 year ago

I need to use an equivalence between path spaces y = z and x = y induced by preconcatenation with a path p : x = y.

So this has been added to the end of the equivalences file.

I also replaced a proof of equiv (x = y) (y = x) with a better proof of the same fact that appeared later.

emilyriehl commented 1 year ago

@fredrik-bakke done.

emilyriehl commented 1 year ago

Let me know if you approve ;)

emilyriehl commented 1 year ago

@fredrik-bakke could you "approve" rather than just comment. I can't merge until someone approves.

fredrik-bakke commented 1 year ago

@fredrik-bakke could you "approve" rather than just comment. I can't merge until someone approves.

I did! Github just doesn't respect my opinion as much as Jonathan's 😔