search

rzk-lang / sHoTT

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

FunExt implies WeakFunExt #74

Closed MatthiasHu closed 1 year ago

MatthiasHu commented 1 year ago

Part of https://github.com/rzk-lang/sHoTT/issues/73.

MatthiasHu commented 1 year ago

This is only a draft pull request for now. I am grateful for any comments/corrections of course!

MatthiasHu commented 1 year ago

This is ready now.

Is the name map-for-weakfunext ok?

jonweinb commented 1 year ago

This is ready now.

Is the name map-for-weakfunext ok?

I'd go for map-for-weakfunext according to previous conventions. Otherwise, I can merge.

MatthiasHu commented 1 year ago

Sorry -- are you saying the name should be changed, or are you saying it can stay as it is?

jonweinb commented 1 year ago

Oops, sorry for the typo. I think map-weakfunext is more in line with preexisting conventions than map-for-weakfunext, so arguing for a change.

MatthiasHu commented 1 year ago

Thanks, I changed it.