cubical
cubical copied to clipboard
Heap
I defined heaps (aka grouds) and did the SIP boilerplate. I defined the structure group of a heap, and proved that a group is equivalently a pointed heap. I didn't try to prove that a heap is equivalently a group equipped with a torsor, we will need a definition of group actions first. (I could use the EM delooping of the group in place of the type of torsors, but i feel like it would be simpler to use torsors).