I don't like how symmetrical the type theoretical colon denotation is, compared to the regular "element" notation. (They are more or less the same.) If instead of

    F : A -> B

we wrote

    F ∈ A -> B

(or any other not symmetrical character) then we could flip it, and use

   A -> B ϶ F, and
   B <- A ϶ F too.