Types are ∞-groupoids

[markfarrell]

I would imagine it might be a good exercise to try to add to the work done in examples/category-theory/category.jonprl and examples/identity-types.jonprl to show that "types are ∞-groupoids", like in the higher type theory literature.

[jonsterling]

If you can come up with a suitable definition of inf-groupoids, then you could probably prove this—but it is valid in only the trivial sense, since JonPRL types currently have no higher-dimensional structure.

[jozefg]

(to elaborate, all equality witnesses are provably equal to <> so everything just collapses to <> \in =(<>; <> ...))