What is predicate lifting?

I understand the constructions involved in this sort of thing best by way of induction rather than coinduction; the differences aren't huge, but examples of induction come to mind more easily. Perhaps the easiest way to see what predicate lifting is doing there is to look at the usual induction over the natural numbers.

So let's say we have a fibration $p:\mathcal{E}\to\mathcal{B}$, which has finite products, coproducts, and a natural numbers object $N$ in $\mathcal B$; fibred finite products and coproducts; and adjunctions $p\dashv \top_{(-)}\dashv C$. I'll also assume that it's a preorder fibration for simplicity, though it need not be. Say we have some predicate $P$ over $N$, and we want to know that $P$ holds of all $n\in N$; that is, our goal is to show that $\top_N\leqslant P$, where $\top_N$ is the uniformly true predicate on $N$.

To make use of induction we need to show that $\top_1\leqslant P(0)$ and that $P(-)\leqslant P(s(-))$, where $0,s$ are the zero and successor of $\mathcal B$'s NNO. Notice that, fibrationally speaking, this is the same as an arrow $\top_1\to P$ in the total category that sits over $0:1\to N$, and an arrow $P\to P$ that sits over $s:N\to N$. So in some sense, it looks a lot like the induction hypotheses also have their own algebraic form, following the form of the algebra in the base category. And this turns out to be just what's happening.

Really, what Jacobs calls "predicate lifting" is lifting a functor on the base category to the total category of predicates; under the above assumptions, the inductive hypotheses for induction can be packaged as an algebra for an endofuctor $\hat{(-)}:\mathcal{E}\to\mathcal{E}$. In this particular instance, the new predicate produced by the lifted functor has the following behavior: $\hat P(*)$ is true, while $\hat P(n)\Leftrightarrow P(n)$. Its not hard to see that the induction hypothesis is true exactly when $\hat P(-) \leqslant P([0,s](-))$ (i.e. when there's an arrow $\hat P\to P$ over $[0,s]$).

The validity of induction in a fibration with the properties described above comes from there being an initial algebra for $\hat{(-)}$ lying over $[0,s]:1+N\to N$. In particular, there will be a functor $G:\mathbf{Alg}(1+-)\to\mathbf{Alg}(F)$, and this functor will have a right adjoint. (And between Jacobs' full result, and those of Neil Ghani, we can generalize this well beyond the case of induction on $N$.)

So "all" that's going on with predicate lifting is that it's a nice way to explain, by way of various adjunctions, why the (co)algebra structure in the base category has anything to do with the structure of the predicates.

Hopefully this sheds some small amount of light on the idea. Let me know if there's any way I can clarify things.