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

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.