[creata]

Do you have any introductory material on cubical type theory, suitable for the average mathematician? The type theory in Lean feels dead simple to me, but all the online resources on cubical type theory feel impenetrable.

[tlringer]

I like these lecture notes: https://staff.math.su.se/anders.mortberg/papers/cubicalmetho...

But if that is too hard to read, I recommend telling Anders directly when you get confused. He is open to improving the notes.

[octoberfranklin]

> all the online resources on cubical type theory feel impenetrable.

Same here.