The branch wildcat-types contains our previous attempts at this, but it causes universe issues elsewhere. Defining things like functor_sum and functor_prod in terms of wildcat functors produces different universe polymorphism: the domains and codomains have to live in the same universe, and there is an extra larger universe parameter. This breaks stuff in Modalities, which are extremely finicky about the number of universe parameters, and also some other places like PropResizing/Nat where universes were carefully tuned for performance.
The branch
wildcat-typescontains our previous attempts at this, but it causes universe issues elsewhere. Defining things likefunctor_sumandfunctor_prodin terms of wildcat functors produces different universe polymorphism: the domains and codomains have to live in the same universe, and there is an extra larger universe parameter. This breaks stuff in Modalities, which are extremely finicky about the number of universe parameters, and also some other places like PropResizing/Nat where universes were carefully tuned for performance.