search

rzk-lang / sHoTT

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

Weak FunExt implies FunExt #145

Closed thchatzidiamantis closed 4 months ago

thchatzidiamantis commented 4 months ago

Converse direction for #73. Also added a naive-funext axiom.

emilyriehl commented 4 months ago

The code looks good but the exposition could be improved. Start the new section with some text that explains what you are planning to do and how the proof will go. The citation to Rijke doesn't appear to be in the right place. If you are formalizing a specific result in that book, then you can use the title="blah" tag immediately before the definition that corresponds to that result. Here it appears you are citing an entire section, so I would do this in the body of the comment and not with a title.

Can we come up with a better name for "WeirdFunExt". Similarly how should I interpret the name of the first term you define? Feel free to ask questions about this on the zulip.

thchatzidiamantis commented 4 months ago

Changes to the exposition. I did not make any name changes on my own, I would be happy to discuss and rename as appropriate.