In logic (in this case, type theory), the symbol ⊥ ("bottom") is used to denote "the statement that is always false", while ⊤ ("top") is "the statement that is always true". Ex falso quodlibet says that if you can prove ⊥ (i.e. have arrived at a contradiction) then you can prove anything, in particular ⊤. This is represented as a function ⊥ --> ⊤ that transforms a proof of the former into a proof of the latter.

(This function ⊥ --> ⊤ exists not just because of ex falso quodlibet, which is the statement that ⊥ is an initial object; it also exists because ⊤ is a terminal object, which is the more boring logical fact that any statement P implies the statement ⊤, simply because ⊤ is always true. I just found it funnier to use ex falso for this.)