Is there a reasonable notion of the fixed point of a profunctor? Is there a reasonable notion of the fixed point of a profunctor?
I guess one would want initial/terminal algebras of a endoprofunctor?
I suppose one would impredicatively encode in Set as something like
$$ \mu H (a) = \forall X,  (\forall b, H(X(b), X(b)) \rightarrow X(a) $$
$$ \nu H (a) = \Sigma X, X(a) \times (\forall b, H(X(b), X(b)) $$
I think in a prover like Coq one would want a recursive type like
CoInductive nu H a :=
| nu_map: (forall b, H (nu b) (nu b)) -> nu H a -> nu H a.
Inductive mu H a :=
| mu_map: (forall b, H (mu b) (mu b)) -> mu H a -> mu H a.

But these all seem very strange.
You would intuit the fixed point as repeated product of profunctor compositions but this is strange.
$$ \mu H(a) = \Sigma b, H(a, b) \times \mu H(b)  $$
Inductive mu H a :=
| mu_map:  H (b, a) -> mu H b -> mu H a.

$$ \mu H(a) = H(a, a) $$
Is also really strange.
Is there a rigorous and reasonable idea for this?
I'm most interested in encodings that support dependent induction and not just recursion. So I think some things don't quite work unless you do then "from outside" so to speak.
 A: $\require{AMScd}$I suspect this approach turns out to be too abstract, but it's the best I can come up with.
Caveat emptor: I'll work with coalgebras, one can easily dualise to algebras (although theorems are known and easy for algebras, not for coalgebras).
Fix a 2-category $\cal K$. First, one needs the following definitions/theorems:

*

*the category of coalgebras of an endo-1-cell of $\cal K$

*Lambek lemma: if $(X,a)$ is a terminal coalgebra, then $a : X\to FX$ is an isomorphism.

*Adamek theorem: the terminal coalgebra is obtained from the limit of the opchain
$$ 1 \leftarrow F1 \leftarrow FF1 \leftarrow \dots$$
Now, for what concerns 1:
Definition. Let $F : A \to A$ be a endo-1-cell of $\cal K$. An $F$-coalgebra is a pair $(X,\alpha)$ where $X : B \to A$ and $\alpha$ is a 2-cell $X \Rightarrow FX$. A morphism of coalgebras $(X, \alpha) \to (Y, \beta)$ consists of a 2-cell $\nu : X \Rightarrow Y$ such that the square
$$\begin{CD}
X @>\nu>> Y \\ 
@V\alpha VV @VV\beta V \\ 
FX @>>F\nu> FY
\end{CD}$$ is commutative.
With this definition, one can reproduce the proof of Lambek's lemma, since it remains a tautology that every algebra map $\alpha : X \to FX$ is an algebra morphism between $(X, \alpha)$ and $(FX, F\alpha)$.
The other interesting fact is that one can -at least try to- reproduce the following theorem:

The important fact is that

*

*A 0-cell $X$ of $\cal K$ "has a terminal object" if the terminal arrow $X \to 1$ has a right adjoint.

*such right adjoint is the (absolute) right lifting of the identity of $1$ alont $X\to 1$, thus yielding a unique 2-cell $u : F{\bf 1} \Rightarrow \bf 1$ that we can use to start the opchain:

$$ {\bf 1} \overset{u}\leftarrow F{\bf 1} \overset{Fu}\leftarrow FF{\bf 1} \leftarrow FFF{\bf 1} \leftarrow\dots $$
Now, the terminal $F$-coalgebra should be the limit of this opchain, yielding a(n invertible) 2-cell $\sigma : T \Rightarrow FT$ by universal property.
Now: how does this story specialise to the case of ${\cal K}=$ the bicategory of profunctors?
