# What is a bipullback of lax functors?

$$\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...

1. 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.
2. 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.
3. Moreover, $$N^\sharp$$ is constant on objects, meaning that for every $$a\in F$$, $$N^\sharp(a)$$ is the same set $$S$$
4. $$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,

1. 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}$$

2. This square is strictly commutative;

3. It enjoys the following property: for every arrangement of bicategories and lax functors (solid arrows) like in

there 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:

1. 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?
2. 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?
3. 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')$$.

Since your $$N^\sharp$$ is almost a pseudofunctor not much can go wrong, in particular lax functors that are lax just on identities are pullback stable, as well as isofibrations ($$U$$ is an isofibration).