Fixtype of Syntheto type sums.
This is a product type introduced by fty::defprod.
This is like a disjoint sum of types, where each summand has a name. Each summand also has fields an an optional invariant, i.e. it has a type product.
So a type sum is a sum of product types, specifically i.e. not a sum of arbitrary types. This is not a limitation of course, because one can have a singleton product type. This ``asymmetry'' between product and sum types is typical of this kind of type systems, including ACL2's FTY library, which Syntheto provides a wrapper for.