$\require{AMScd}$The following question is somewhat technical, and since I firmly believe this has a small hope to be true only using *all* the assumptions, I am forced to introduce them all: I don't want to say "I have a bicategory"; probably if this works, it does just because the bicategory is $\sf Span$, and so on...

- I have defined a monoidal category $F$, and endowed it with a functor $N^\sharp : F \to {\sf Span}$; $F$ is moreover a free monoidal category.
- this functor is
*almost*a pseudofunctor, meaning that it preserves the composition of morphisms, but not the identity map: there's only a noninvertible unitor $1_{Na} \to N^\sharp(1_a)$ if the domain "1" is the identity span. - Moreover, $N^\sharp$ is constant on objects, meaning that for every $a\in F$, $N^\sharp(a)$ is the same set $S$
- $N^\sharp$ is also lax monoidal.

Now, mimicking a "category of elements" construction, I have built the following "pullback", where $\sf Span_*$ is the category of spans between pointed sets:

$$\begin{CD}
\textstyle\int N^\sharp @>>> {\sf Span}_* \\
@VVV@VVUV \\
F @>>N^\sharp> {\sf Span}
\end{CD}$$
The functor $U$ just forgets that a span is a span of pointed sets. Thus it is as strong as it can possibly be. The square in question commutes *strictly*.

The category $\int N^\sharp$ can be described as follows: its objects are pairs $(a, x\in S)$ (remember that $N^\sharp$ is constant on objects), and a morphism $(a,x)\to (b,y)$ is a pair $(f,e)$ of a morphism $f : a\to b$ in $F$ and an element $e$ in the summit of the span $N^\sharp f : E \to S\times S$, with the property that $N^\sharp f$ sends $e$ to $(x,y)$.

So far, so good!

My aim now is to prove that $\int N^\sharp$ is just a different name for another (free monoidal) category $F_B$, obtained from a completely different construction, and yet equivalent to $\int N^\sharp$. As always when working with lax functors, this opens a bag of snakes, because I have no idea what universal property I'm really after, and where exactly to instantiate it.

I will be more specific: I was able to prove what follows: for the category $F_B$, defined via some very different construction,

There exists a square $$\begin{CD} F_B @>K>> {\sf Span}_* \\ @VHVV@VVUV \\ F @>>N^\sharp> {\sf Span}\end{CD}$$ filled by lax functors, or more precisely $$\begin{CD} @>\text{lax on id}>> \\ @V\text{lax}VV@VV\text{pseudo}V \\ @>>\text{lax on id}> \end{CD}$$

This square is strictly commutative;

It enjoys the following property: for every arrangement of

*bicategories*and*lax functors*(solid arrows) like inthere exists a unique strict functor $G$ ($F_B$ is a category!), making everything commute.

I have, oh, so many questions now! Am I done, is this enough to deduce that there is an equivalence of categories $F_B\cong \int N^\sharp$? What did I build? A bilimit, and if yes, where (=in what category/n-category)? And more in particular:

- The theory of bilimits is still elusive to me; I know that when pulling back along a functor that is an isofibration, the result is also a bipullback (in the sense of bilimits). Now, $U$ here is clearly an isofibration: can I still deduce that performing a pseudopullback yields a bipullback, or the laxity of $N^\sharp$ gets in the way?
- Even if the former question has negative answer, is it the case that the universal property of $\int N^\sharp$ can be checked on less, or on stricter, structure, and still obtain a bilimit?
- Every 2-dimensional universal property has a 2-dimensional part; what about here, where the laxity of functors prevents them to be whiskered with transformations of any sort?

RE the last point, if lax transformations were whiskerable, I would say that the following 2-dimensional UP has to hold: every pair of 2-cells $\lambda : L\Rightarrow L' : \mathcal C \to {\sf Span}_*$ and $\rho : R \Rightarrow R' : \mathcal C \to F$ with the property that $U * \lambda = N^\sharp * \rho$, must induce a unique $\langle\lambda,\rho\rangle : G\Rightarrow G'$ between the $G$'s induced by the pairs $(L,R)$ and $(L',R')$.