Thanks Anders. To be clear, I don’t think we have any schemas or semantics of HITs that accept this definition of S^n (with an n-loop for an internally-specified n) in any non-cubical settings either; at the time, I was thinking of it more as exploring what you can do with the definition. Proving the two definitions equivalent should be the same (modulo which definitional equalities you get) as implementing the one-n-loop rules in terms of suspensions, so that would be one way to justify these rules.
Also, the proof of pi_n(S^n) = Z that Guillaume mentioned, which predated Freudenthal, is a lot more work than the one that you get from Freudenthal, so I’m not sure we have any motivating examples for why the one-n-loop definition is better than the suspension definition for arbitrary n.
-Dan
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to
HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit
https://groups.google.com/d/msgid/HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%40googlegroups.com.