Topic: hott zulip
Johan Commelin (Mar 21 2020 at 10:45):
I wanna dive a bit more into HoTT. See whether the benefits of univalence such as transfer are as cool as I think they are. And also check whether it doesn't create nuisances in practice when formalising ordinary non-homotopy maths. Since Zulip is awesome, I've created: https://hott.zulipchat.com/#
You're heartily invited to join, if you are interested in HoTT.
@Bas Spitters has already publicised the chatroom on the HoTT github page. I'm looking forward to some fruitful and engaging discussions!
Yury G. Kudryashov (Mar 21 2020 at 11:03):
Is there a simple explanation of what is easier/harder in HoTT from the point of view of a person who writes proofs and doesn't care about logic / type theory foundations?
Johan Commelin (Mar 21 2020 at 11:07):
You should ask over there (-;
Kevin Buzzard (Mar 21 2020 at 16:39):
@Ulrik Buchholtz I had a couple of really interesting conversations with you about HoTT in Pittsburgh and perhaps this Zulip chat would be a great place to have more. I still am confused about whether HoTT is actually what I as a mathematician want, and Mario's remarks on another thread here are exactly the kind of things which make me worry.
Ulrik Buchholtz (Mar 21 2020 at 16:57):
Thanks for the heads-up; I've joined.
Last updated: Aug 03 2023 at 10:10 UTC