I must confess, I understand higher inductive types syntactically, but semantically I still don't understand what they mean. Like, what does it really mean to have a higher inductive type that represents a circle?
Conversation
What does reasoning about a circle as a higher inductive type really look like?
1
5
What theorems can one prove about the circle type? What functions can one write? What do those proofs and functions look like?
4
5
I wanna know what cool programs I can write using klein bottles muahaha
2
Möbius for loop?
1
Now I'm wondering if you could somehow make a game of asteroids or snake on different HITs somehow - perhaps this is overly optimistic/silly though