fact: Record WFunctor {I O} (S : I ▷ O) (X : I → Type) (o : O) : Type := { op : Operations S o; ar : Arities S op; xx : X (Sorts S ar) }.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple