pub fn dimap_ty() -> Expr
Dimap : ∀ (P : Type → Type → Type) (A B C D : Type), Prop
The dimap law: functorial mapping in both contravariant and covariant positions.