Zulip Chat Archive

Stream: general

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: Dec 20 2023 at 11:08 UTC