In topology, the notion of "lifting" has a quite a long history, starting with the theory of covering spaces, where the classic example is that if you take an outdoor spiral staircase, $S$ and look at its shadow at noontime, you see a circle, $C$. "Casting a shadow" gives a map $p : S\to C$ with lots of nice properties, and we say that $S$ is a covering of $C$. $C$ is the base space, $S$ is the covering space, and $p$ is the projection.
A typical problem we consider is this: suppose we have a point $c \in C$ and a point $s \in S$ with $p(s) = c$. If we have a path in $C$ starting at $c$ (i.e., a function $u: [0, 1] \to C$ with $u(0) = c$), is there a path $\hat{u}$ in $S$ that "covers" $u$, i.e., a function $$ \hat{u}:[0, 1] \to S,\\ \hat{u}(0) = s \\ p(\hat{u}(t)) = u(t) \text{ for $0 \le t \le 1$ }. $$
In humbler terms, if Ann takes a walk on the circle starting at $c$, can Robin take a walk on the staircase starting at $s$ in such a way that Robin's shadow falls on Ann at all times?
The answer (at least in this example) is evidently "yes", and that's called the "path lifting theorem" --- the path $\hat{u}$ is a "lift" of the path $u$. That gets generalized to the homotopy lifting theorem, etc.
It's pretty clear that on $S$, there's an equivalence relation defined by $p$: points $s_1$ and $s_2$ are declared equivalent when $p(s_1) = p(s_2)$. Under this equivalence relation, the set $C$ is the quotient of $S$ by this relation.
So we have a set $S$, a relation $\sim$ on $S$, and a quotient $C = S/\sim$. A function $u$ to the set $C$ is said to "lift" to a function $\hat{u}$ to $S$.
This is exactly the opposite of the use of "lift" in both Lean and Isabelle, as far as I can tell. In those, we start with a function to $S$ and "lift" it to a function to $C$ (if certain conditions hold). A topologist would describe this second one by saying "we have a function going to $S$; is it the lift of a function to $C$?
There's a kind of "dual" notion: perhaps we have a function $f$ from $S$ to some space $X$. If $f(x) = f(y)$ whenever $p(x) = p(y)$, then topologists would say that $f$ "passes to (or even "projects to") a function on the quotient", while proof-assistant folks seem to say that $f$ lifts to a function on $C$.
Can anyone explain how this exactly-opposite notion of "lift" arose for proof-assistants? I know that lots of words in mathematics get used differently in different context, but I can't think of many instances where the meanings are exact opposites (except for some confusion over co-variant and contra-variant).
