I've been trying to figure out some homotopy stuff with regards to categories.
A lot of theorem provers have good support for integers. Not so many have good support for quotient types. Setoids help but they're still a massive pain. The fundamental group of the circle is equivalent to addition of integers. So the circle can be defined directly in terms of integers.
How much homotopy theory can I bootstrap from the circle/integers in preference to fiddling with setoids and quotients?
I'm wondering if I can get away without any setoids/quoitents at all just by using integers/circles.
I know a functor out of the circle is a loop and you can take the product of circles to obtain toroids. But the suspension seems to require the smash product.
I have a feeling like maybe what I want is something to do with stabilization and spectrum objects but I don't understand those. Maybe homology? Every Abelian group can be represented by a Z-Module so maybe this is what I want. I don't really get it though.
In pseudocoq.
Instance Circle: Groupoid := {
object := unit ;
mor _ _ := Z ;
id _ := 0 ;
compose _ _ _ f g := f + g ;
invert _ _ x := -x ;
}.
I'm exploring Cubical Agda right now but this style still looks sort of interesting.