This is only somewhat related to the talk on category theory in Agda but sometimes I get the impression that there's a lot of proofs where people will be like "oh this relies on axiom K and proof irrelevance and blah blah blah" as an argument for why the proof is ungood but to me this feels more like an argument for why more type theories *should* have such axioms etc. (or at least the possibility to enable them)

There was probably a design decision somewhere to use those axioms because it simplified proofs etc. which means they were helpful in making proofs easier to write and understand

There's a lot of the "what's the smallest set of axioms we can work off of" that I feel like comes from set theory and it's a valid desire but adding justifiable, intuitive, and consistent (ofc) axioms should be just as valid for practical purposes

jonoodle@ionchy@types.plre: CPP 2021

How strange, there doesn't seem to be any cubical talks in CPP this year

No tori as the product of two circles this year, alas