Contravariant sort parameters

Uses Character strings.

The sort
 ⇅(𝕊)
is equal to its argument sort except for an inversion of its subsort relations.

See Functions for an example and an explanation.

Implementation detail

The sort of sort operators with contravariant parameters is 𝕊(String). These are subsorts of the standard sort sort 𝕊: 𝕊(s:String) ⊆ 𝕊. The string parameter is a bit string (containing only the characters 0 and 1), with each bit containing the contravariance flag of one parameter.