the cubical agda library (has some pointers...)
The goal of my talk is to introduce you to homotopy type theory, which is a reletatively recent area of pure mathematics and computer science. The talk is not about using homotopy type theory in programming, but introducing it in a way geared towards everyone with some background in programming.
I will show some data types in the dependently typed language agda, explaing how they relate to corresponding things in more mainstream languages. Agda is a language with nice notation for both, programming and math. It is certainly helpful if you know the material covered in the formalization workshop at 11:00 am (same day), but my aim is to make a stand alone presentation.
From there, I will move to more exotic things which are the first steps into the world of homotopy type theory, still using agda as a language. You can try agda on your on device during the talk if you like - even in your browser!
🧮