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
I did find it neat how you can prove that a donut can be broken up into two circles and vice versa just using pattern matching, but unsure if this is what you had in mind: