# How did the meaning of "lifting" in proof assistants arise?

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).

I totally agree that Lean's quotient.lift is disastrously-named as far as mathematicians are concerned. After discussion with the Lean devs it seems that it came about because to a computer scientist, quotienting out something by an equivalence relation is "making it more complex" (because as a type the quotient involves more stuff than the original type), whereas for mathematicians it's "making it smaller and hence simpler".