Compute sym on all types

[mikeshulman]

• [ ] Unit type
• [ ] Sigma-types
• [ ] Pi-types
• [ ] Copy-types
• [ ] The universe
• [ ] Sum-types
• [ ] Natural numbers
• [ ] Integers

[mikeshulman]

Computing sym on the universe is somewhat fraught: it seems that even the underlying double-correspondence can't be computed on an arbitrary square in the universe, without knowing the structure of that square. (The obvious definition, transposing the double correspondence, yields bizarre definitional equalities when combined with the naturality rules for sym; instead it should be only isomorphic to this transpose, by an isomorphism that is essentially an instance of sym.)

It seems that the double-correspondence resulting from sym on the universe should be treated like a new type former, say Sym, analogous to Id, which computes on its input type argument. Then Sym is related to sym (which computes on its type -- not identification -- argument) similarly to how Id is related to ap (which computes on its term -- not identification -- argument).