Event

talk notes as agda file

talk notes as html

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!

🧮