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!

🧮