Return to Answer

It'll be a little nicer to work with the category $$\mathcal{C} = \mathsf{Pos}^{|P|} \times_{\mathsf{Pos}/|P|} \mathsf{Pos}/P$$ (we mean the strict pullback, but this is equivalent to the weak one because the forgetful functor $\iota_{!} : \mathsf{Pos}/|P| \to \mathsf{Pos}/P$ is an isofibration by general nonsense). The base change of $E$ gives an equivalence $E' : \mathcal{C} \to \mathsf{Pos}/P$ and the base change $F : \mathcal{C} \to \mathsf{Pos}^{|P|}$ of $\iota^*$ satisfies $\iota^* \cong E \circ F \circ (E')^{-1}$. Neglecting some redundant data (or replacing $\mathcal{C}$ by an isomorphic category) the objects of $\mathcal{C}$ are pairs $(\{Q_x\}_{x \in P}, \leq)$ where $\{Q_x\}_{x \in P}$ is a family of posets and $\leq$ is a partial order on $\sum_{x \in P} Q_x$ which (i) restricts to the given order on each cross section $\{x\} \times Q_x \cong Q_x$ and (ii) makes the set-theoretic projection $\sum_{x\in P} Q_x \to P$ monotone. We can restate (ii) as saying whenever $(x, y) \leq (x', y')$ also $x\leq x'$. Morphisms in $\mathcal{C}$ are the obvious thing: morphisms of families as in $\mathsf{Pos}^{|P|}$ such that the induced morphism on $\Sigma$'s is monotone with respect to the chosen orders.

It'll be a little nicer to work with the category $$\mathcal{C} = \mathsf{Pos}^{|P|} \times_{\mathsf{Pos}/|P|} \mathsf{Pos}/P$$ (we mean the strict pullback, but this is equivalent to the weak one because $\iota^* : \mathsf{Pos}/P \to \mathsf{Pos}/|P|$ is an isofibration). The base change of $E$ gives an equivalence $E' : \mathcal{C} \to \mathsf{Pos}/P$ and the base change $F : \mathcal{C} \to \mathsf{Pos}^{|P|}$ of $\iota^*$ satisfies $\iota^* \cong E \circ F \circ (E')^{-1}$. Neglecting some redundant data (or replacing $\mathcal{C}$ by an isomorphic category) the objects of $\mathcal{C}$ are pairs $(\{Q_x\}_{x \in P}, \leq)$ where $\{Q_x\}_{x \in P}$ is a family of posets and $\leq$ is a partial order on $\sum_{x \in P} Q_x$ which (i) restricts to the given order on each cross section $\{x\} \times Q_x \cong Q_x$ and (ii) makes the set-theoretic projection $\sum_{x\in P} Q_x \to P$ monotone. We can restate (ii) as saying whenever $(x, y) \leq (x', y')$ also $x\leq x'$. Morphisms in $\mathcal{C}$ are the obvious thing: morphisms of families as in $\mathsf{Pos}^{|P|}$ such that the induced morphism on $\Sigma$'s is monotone with respect to the chosen orders.

Here are some other thoughts: the fact that $\iota^*$ is a left adjoint actually doesn't require us to construct $\iota_*$, it follows from the fact that $\iota$ is a Conduché fibration (this is a condition about lifting factorizations in $P$ to factorizations in $|P|$, and in this case it's the fact that $x \leq y \leq z$ and $x = z$ implies $x = y$ and $y = z$). We can very explicitly check that the left adjoint $\iota_! \dashv \iota^*$ is fully faithful (it's immediate from injectivity of $\iota$) and since we have an adjoint triple $\iota_! \dashv \iota^* \dashv \iota_*$ this implies $\iota_*$ is fully faithful as well. And then $\iota_! \circ \iota^*$, $\iota_* \circ \iota^*$ are the coreflection and reflection of $\mathsf{Pos}/P$ at the class $W$ of morphisms which restrict to bijections on fibers. So given a poset $Q$ over $P$ the coproduct of the fibers of $Q$, i.e. $\iota_!(\iota^*(Q))$, is characterized by being $W$-colocal and mapping into $Q$ via an element of $W$ while the lexicographic order on $Q$, i.e. $\iota_*(\iota^*(Q))$, is characterized by being $W$-local and mapping into $Q$ via an element of $W$. A decategorification of this is that if we fix a family $\{Q_x\}_{x \in P}$ of posets then the coproduct order on $\sum_{x \in P} Q_x$ is the minimum order satisfying (i) and (ii) while the lexicographic order on $\sum_{x \in P} Q_x$ is the maximum order satisfying (i) and (ii). I'm sure you could rephrase what I did above in terms of this. This description in terms of slices also sort of clarifies why the lexicographic order isn't a grothendieck construction. In a topos or locally cartesian closed category the left adjoint to pullback is dependent sum, which the grothendieck construction is like a higher dimensional version of, while the right adjoint is dependent product. But this is still strange: why does the lexicographic order on the dependent sum arise as a sort of dependent product? Maybe the answer lies in the semantics of directed type theory (which I know nothing about). I also wonder if there's any cohesion stuff happening here since it's all about slices and discreteness (although again this isn't something I understand). The fact that we get a "dependent product" maybe suggests that the lexicographic order is a lax limit, but I didn't work that part out.

Here are some other thoughts: the fact that $\iota^*$ is a left adjoint actually doesn't require us to construct $\iota_*$, it follows from the fact that $\iota$ is a Conduché fibration (this is a condition about lifting factorizations in $P$ to factorizations in $|P|$, and in this case it's the fact that $x \leq y \leq z$ and $x = z$ implies $x = y$ and $y = z$). We can very explicitly check that the left adjoint $\iota_! \dashv \iota^*$ is fully faithful (it's immediate from injectivity of $\iota$) and since we have an adjoint triple $\iota_! \dashv \iota^* \dashv \iota_*$ this implies $\iota_*$ is fully faithful as well. And then $\iota_! \circ \iota^*$, $\iota_* \circ \iota^*$ are the coreflection and reflection of $\mathsf{Pos}/P$ at the class $W$ of morphisms which restrict to order isomorphisms on fibers. So given a poset $Q$ over $P$ the coproduct of the fibers of $Q$, i.e. $\iota_!(\iota^*(Q))$, is characterized by being $W$-colocal and mapping into $Q$ via an element of $W$ while the lexicographic order on $Q$, i.e. $\iota_*(\iota^*(Q))$, is characterized by being $W$-local and mapping into $Q$ via an element of $W$. A decategorification of this is that if we fix a family $\{Q_x\}_{x \in P}$ of posets then the coproduct order on $\sum_{x \in P} Q_x$ is the minimum order satisfying (i) and (ii) while the lexicographic order on $\sum_{x \in P} Q_x$ is the maximum order satisfying (i) and (ii). I'm sure you could rephrase what I did above in terms of this. This description in terms of slices also sort of clarifies why the lexicographic order isn't a grothendieck construction. In a topos or locally cartesian closed category the left adjoint to pullback is dependent sum, which the grothendieck construction is like a higher dimensional version of, while the right adjoint is dependent product. But this is still strange: why does the lexicographic order on the dependent sum arise as a sort of dependent product? Maybe the answer lies in the semantics of directed type theory (which I know nothing about). I also wonder if there's any cohesion stuff happening here since it's all about slices and discreteness (although again this isn't something I understand). The fact that we get a "dependent product" maybe suggests that the lexicographic order is a lax limit, but I didn't work that part out.

For an object $Q = (\{Q_x\}_{x \in P}, \leq)$ of $\mathcal{C}$ define $\varepsilon_Q : Q \to L(F(Q))$ to be the family of identity maps $Q_x \to Q_x$. For this to be a well defined morphism in $\mathcal{C}$ we need the induced map $\Sigma_{x \in P} Q_x \to \Sigma_{x \in P} Q_x$, again the identity, to be monotone with respect to $\leq$ on the domain and $\leq^{\ell}$ on the codomain. This is immediate from conditions (i), (ii) and the definition of $\leq^{\ell}$. Finally the triangle identities are trivial to check because $F, L$ don't change the underlying families of set-functions at all and the underlying families of $\eta, \varepsilon$ are the identities.

For an object $Q = (\{Q_x\}_{x \in P}, \leq)$ of $\mathcal{C}$ define $\eta_Q : Q \to L(F(Q))$ to be the family of identity maps $Q_x \to Q_x$. For this to be a well defined morphism in $\mathcal{C}$ we need the induced map $\Sigma_{x \in P} Q_x \to \Sigma_{x \in P} Q_x$, again the identity, to be monotone with respect to $\leq$ on the domain and $\leq^{\ell}$ on the codomain. This is immediate from conditions (i), (ii) and the definition of $\leq^{\ell}$. Finally the triangle identities are trivial to check because $F, L$ don't change the underlying families of set-functions at all and the underlying families of $\eta, \varepsilon$ are the identities.