hott zulip

Stream: general

[Johan Commelin]

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]

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]

You should ask over there (-;

[Kevin Buzzard]

@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]

Thanks for the heads-up; I've joined.