Two-sided cartesian fibrations of synthetic (∞,1)-categories

Jonathan Weinberger]Jonathan Weinberger
Dept. of Mathematics, Krieger School of Arts & Sciences, Johns Hopkins University, 3400 N Charles St, Baltimore, MD 21218, USA

Within the framework of Riehl–Shulman's synthetic $(\infty,1)$-category theory, we present a theory of two-sided cartesian fibrations. Central results are several characterizations of the two-sidedness condition à la Chevalley, Gray, Street, and Riehl–Verity, a two-sided Yoneda Lemma, as well as the proof of several closure properties.

Along the way, we also define and investigate a notion of fibered or sliced fibration which is used later to develop the two-sided case in a modular fashion. We also briefly discuss discrete two-sided cartesian fibrations in this setting, corresponding to $(\infty,1)$-distributors.

The systematics of our definitions and results closely follows Riehl–Verity's $\infty$-cosmos theory, but formulated internally to Riehl–Shulman's simplicial extension of homotopy type theory. All the constructions and proofs in this framework are by design invariant under homotopy equivalence. Semantically, the synthetic $(\infty,1)$-categories correspond to internal $(\infty,1)$-categories implemented as Rezk objects in an arbitrary given $(\infty,1)$-topos.

MSC2020: 18N60, 03B38, 18D30, 18N45, 55U35, 18N50

Keywords: $(\infty,1)$-categories, two-sided cartesian fibrations, Segal spaces, Rezk spaces, fibered Yoneda Lemma, homotopy type theory, simplicial type theory

§ INTRODUCTION

§.§ Synthetic higher category theory

§.§.§ $\infty$-Cosmos theory

In recent years, there have been ongoing investigations into higher category theory using synthetic approaches where the basic objects already have intrinsic homotopical meaning. The program of Riehl–Verity <cit.> develops $(\infty,n)$-category theory, for $0 \le n \le \infty$, using the notion of $\infty$-cosmos[The terminology has been suggested by Peter May <cit.>, after <cit.>.] which provides a semi-strict way to present $(\infty,2)$-categorical universes of a wide range of notions of higher categories ( quasi-categories, Rezk spaces/objects, $n$-complicial sets, $\Theta_n$-spaces, …)—as well as derived notions thereof such as slices, discrete objects, fibrations, . This has sparked a very powerful program to establish $\infty$-category theory in model-independent way. Intriguingly, they demonstrate how parts of the theory can even be reduced essentially to (strict) $2$-categorical arguments <cit.> which makes precise a range of very helpful intuitions that previously had lacked justification at this level of conceptionality, rigor, and comprehensiveness. Indeed, $\infty$-cosmos theory systematically employs techniques from Australian or formal category theory to work internal to sufficiently complete $(\infty,2)$-categories that are thought of as universes for different notions of higher categories.

§.§.§ Simplicial type theory

While $\infty$-cosmos theory is based on traditional set theory, there also have been approaches to higher category theory within various type theories. A type theory is a formal system that allows for doing mathematics in a more structuralist way, as opposed to the materialist nature of set theory. The advent of homotopy type theory and univalent foundations (HoTT/UF) due to Voevodsky <cit.>, Awodey–Warren <cit.>, et al. has led to a new area of research yielding synthetic accounts to homotopy theory. This provides a significant generalization of the pioneering earlier work by Hofmann–Streicher <cit.> on the ($1$-)groupoid interpretation of Martin–Löf type theory. Roughly, the basic objects in HoTT are homotopy types,  spaces up to homotopy  weak $\infty$-groupoids,  <cit.>. In fact, after various works towards extending the class of models such as <cit.> Shulman was able in 2019 to prove Awodey's conjecture that any $\inftyone$-topos (in the sense of Grothendieck–Rezk–Lurie <cit.>) admits a model-categorical presentation that supports a full model of HoTT.

This does not yield an account to synthetic higher categories right away. Indeed, defining a notion of $(\infty,1)$-category in plain HoTT has been a long standing open problem.

Thus, variations of HoTT have been proposed that indeed make it possible to reason about higher categories using (complete) Segal-type formalisms such as two-level type theory <cit.> based on Voevodsky's homotopy type system (HTS) <cit.>. Another such approach is simplicial (homotopy) type theory, introduced in <cit.>.[ <cit.> for a high-level overview.] There, one adds another layer of strict simplicial shapes, containing  the directed cubes $\I^n$, standard $n$-simplices $\Delta^n$, the $(n,k)$-horns $\Lambda_k^n$, . Type families can then also depend on shapes. Another feature is the notion of extension type: given a shape inclusion (“cofibration”) $\Phi \subseteq \Psi$, a type family $A: \Psi \to \UU$, and a partial section $a: \prod_\Phi \Phi^*A$, there exists the type

\[ \exten{\Phi}{A}{\Psi}{a}\]

of sections $b: \prod_\Psi A$ satisfying $a(t) \jdeq b(t)$ for all $t:\Phi$.

Together with the given shapes, this induces a sensible notion of (dependent) hom-type $\hom_A:A \to A \to \UU$, as well as synthetic versions of the Segal and Rezk conditions. Riehl–Shulman's work on discrete fibrations in this setting was later generalized to the case of co-/cartesian fibrations <cit.> and lextensive  <cit.>. The text at hand presents a further generalization of the one-sided (co-/)cartesian case to the two-sided cartesian case.

§.§ Co-/cartesian families

Let $\UU$ be a universe type,  <cit.>. A cocartesian family $P:B \to \UU$ over a Rezk type $B$ ( a synthetic $\inftyone$-category) precisely captures the idea of a functorial type family valued in ($\UU$-small) synthetic $\inftyone$-categories: an arrow $u:a \to_B b$ in the type $B$ induces covariantly a functor $u_!^P \jdeq : u_! : P\,a \to P\,b$ between the fibers:

\[\begin{tikzcd}
a & b && {P\,a} & {P\,b}
\arrow["u", from=1-1, to=1-2]
\arrow["\leadsto"{description}, draw=none, from=1-2, to=1-4]
\arrow["{u_!}", from=1-4, to=1-5]
\end{tikzcd}\]

Dually, a cartesian family $P:B \to \UU$ transforms contravariantly functorially,  an arrow $u:b \to_B a$ induces a functor $u_P^* \jdeq : u^*: P\,a \to P\,b$:

\[\begin{tikzcd}
b & a && {P\,b} & {P\,a}
\arrow["u", from=1-1, to=1-2]
\arrow["{u^*}"', from=1-5, to=1-4]
\arrow["\rightsquigarrow"{description}, draw=none, from=1-2, to=1-4]
\end{tikzcd}\]

These notions generalize the familiar $1$-categorical concepts of a Grothendieck op-/fibration <cit.> to the synthetic higher setting. Fibrations of $\inftyone$-categories have initally been studied by Joyal <cit.> and Lurie <cit.> for quasi-categories, and consecutively very notably by Ayala–Francis <cit.>, Barwick–Shah <cit.>, Barwick–Dotto–Glasman–Nardin–Shah <cit.>, Rezk <cit.>, Cisinski <cit.>, Nguyen <cit.>, Cisinski–Nguyen <cit.>, as well as other authors. Particularly crucial for our approach are the treatments by Rasekh <cit.> for Rezk spaces, and Riehl–Verity's $\infty$-cosmos theory <cit.> which generalizes concepts and results due to Street <cit.> and Gray <cit.> to a rigorous and powerful framework of model-independent higher category theory.

In the context of simplicial type theory, Riehl–Shulman have considered covariant families <cit.>, functioning as a synthetic variant of (discrete) left fibrations <cit.>.

§.§ Two-sided cartesian families

Two-sided cartesian families are type families $P:A \to B \to \UU$ which fibrationally are presented by spans

\[\begin{tikzcd}
& E \\
A && B
\arrow["\xi"', two heads, from=1-2, to=2-1]
\arrow["\pi", two heads, from=1-2, to=2-3]
\end{tikzcd}\]

where $\xi$ is cocartesian, $\pi$ is cartesian, and some compatibility conditions between the two respective liftings are satisfied. An instructive example is given by the “hom span” $\partial_1: A \leftarrow A^{\Delta^1} \to A:\partial_0$ of a Rezk type $A$, and from ensuing properties one also obtains comma spans $\partial_1 : C \leftarrow \comma{f}{g} \rightarrow B : \partial_0$ induced by a span $g:C \leftarrow A \to B:f$ of functors.[In fact, these are even discrete two-sided fibrations,  <cit.>, <cit.>, <cit.>.] Originally, this notion goes back to Street <cit.>, and it has been generalized and thoroughly investigated for $\infty$-cosmoses <cit.>. Semantically, two-sided families correspond to categorical $\inftyone$-distributors,  bifunctors $A^{\Op} \times B \to \Cat$ into the $\inftyone$-category of small $\inftyone$-categories.[Even though this cannot be expressed in our theory yet,  <cit.>.] The significance for $\infty$-cosmos theory is that the discrete variant,  the $\inftyone$-distributors or modules, form a virtual equipment <cit.>, a rich double-categorical structure that presents the formal $\infty$-category theory of an $\infty$-cosmos. The Model Independence Theorem states that a biequivalence between $\infty$-cosmoses lifts to a biequivalence of the associated virtual equipments.[Note the parallel to axiomatic homotopy theory where a Quillen equivalence between “homotopy theories” presented through model categories lifts to an equivalence of their associated homotopy categories.] Here, however, we will deal with the categorical two-sided case. Namely, we will provide a structured analysis, leading up to characterizations and closure properties generalizing the one-sided case. This follows the thread of of <cit.>, but with a more explicit account of various (auxiliary) notions of fibered (or sliced) fibrations, owed to the lack of categorical universes in the present theory. Our treatise nevertheless often times make use of techniques from “formal” category theory, by reasoning about the various conditions in terms of statements about (fibered) adjunctions, and their closure properties. We view this as a fruitful pratical effect of the $\infty$-cosmological philosophy on the synthetic theory formulated in simplicial type theory.

Our treatise ends with a two-sided Yoneda Lemma, and a (very brief) note on discrete two-sided families.

§.§ Structure of the paper

A two-sided cartesian family $P: A \to B \to \UU$ corresponds to a span $\xi: A \leftarrow E \rightarrow B : \pi$ with $\xi$ a cocartesian and $\pi$ a cartesian fibration such that the lifts are compatbile in a certain sense. But such a family or span, resp., can also be understood as a cartesian functor

\[\begin{tikzcd}
E && {A \times B} \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\pi"', two heads, from=1-1, to=2-2]
\arrow["q", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

between cartesian fibrations that in addition is a fibered or sliced cocartesian fibration over $B$. By duality and the Chevalley criteria for (ordinary) co-/cartesian fibrations and functors, resp., there are several equivalent way to express this fact,  <Ref>, after <cit.>.

Semantically, the condition is that $\varphi: \pi \to_B q$ is an object of the $\infty$-cosmos $\mathrm{co}{\mathcal C}\mathrm{art}(\mathcal{C}\mathrm{art}(\mathcal K))$ for the ambient $\infty$-cosmos $\mathcal K$ (which is of the form $\mathcal K=\mathscr{R}ezk_\mathscr E$,  <cit.> for an $\infty$-cosmos $\mathscr E$ presenting an $\inftyone$-topos.).

<Ref> is a technical introduction and a recap of the basic fibrational theory set up in <cit.>. We then work towards two-sided cartesian families by first discussing sliced cocartesian families in <Ref>, in particular their characterizations à la Chevalley and their closure properties,  <Ref>. Next, we specialize to the case of cocartesian families in cartesian families,  <Ref>.

<Ref> then introduces and the notion and establishes basic properties of two-sided cartesian families and fibrations, resp. In <Ref> we provide the basic formalism of two-variable families and bifibers. Finally, in <Ref> we define two-sided cartesian families and prove a number of Chevalley-like characterization criteria.

In <Ref> we introduce two-sided cartesian functors and prove several closure properties (a subset of which corresponds to the $\infty$-cosmological closure properties,  <cit.>).

We proceed by proving a two-sided cartesian Yoneda Lemma in <Ref> and conclude by briefly discussing discrete two-sided cartesian families in <Ref>, namely how they can be understood as discrete objects in the $\infty$-cosmos of two-sided cartesian fibrations.

Helpful technical results about several fibered constructions and notions are provided in the Appendix. We treat fibered equivalences in <Ref> and fibered (LARI) adjunctions in <Ref>. In <Ref> we conclude with preservation properties for sliced commas and products.

§.§ Contribution

We develop a theory of two-sided cartesian fibrations <cit.> of synthetic $\inftyone$-category theory in simplicial homotopy type theory <cit.>. The central results are a characterization theorem (<Ref>), a Yoneda Lemma (<Ref>), and several closure properties (<Ref>). Along the way, we also investigate other notions like sliced co-/cartesian families or cocartesian-on-the-left families.

In doing so we work completely internally in simplicial HoTT, so all the results externalize to theorems about internal $\inftyone$-categories in an arbitrary given Grothendieck–Rezk–Lurie $\inftyone$-topos.

Specifically, our work in this type-theoretic setting generalizes previous developments from <cit.> and <cit.> following ideas, concepts, and techniques from <cit.> and translating into the type theory at hand.

The work presented here appears as <cit.>. This PhD thesis was written at TU Darmstadt under the supervision of Thomas Streicher.

§.§ Related work

Two-sided cartesian fibrations internal to $2$- and bicategories have been introduced by Street <cit.>,  also the review in <cit.>. They have been later generalized to the $\infty$-cosmological setting by Riehl–Verity <cit.>. Our work is an adaption of the latter, in particular <cit.>, to the setting of simplicial homotopy type theory <cit.>. This generalizes previous work on (one-sided) co-/cartesian fibrations <cit.> in this setting. Moreover, there exist treatments of lextensive <cit.> and exponentiable  Conduché  flat fibrations <cit.> in this setting.

Recently, large parts of Riehl–Shulman's initial paper <cit.>, including the $\infty$-categorical Yoneda Lemma <cit.> have been formalized <cit.> in Kudasov's new proof assistant Rzk <cit.>. There have been various follow-up formalizations in Rzk <cit.>. These currently do not include the work at hand about two-sided cartesian (non-discrete) families but we this development to be possible depending some more groundwork formalizations.

By the semantics of simplicial HoTT <cit.> in $\inftyone$-toposes of the form $\mathscr E^{{\Simplex}^{\Op}}$ for an $\inftyone$-topos $\mathscr E$, the synthetic $\inftyone$-categories in our theory are interpreted as internal $\inftyone$-categories in $\mathscr E$,  Rezk objects. Those have been investigated in various works and semantic settings, notably <cit.>.

Directed univalence for a universe of synthetic left fibrations has been shown by <cit.>. In a (bi-)cubical analogue to sHoTT, there is work by Weaver–Licata <cit.> on directed univalence for covariant discrete fibrations. There is also recent work on co-/limits <cit.> for (complete) Segal types in simplicial HoTT by Bardomiano Martínez.

In HoTT, univalent categories and the Rezk completion have been considered in <cit.> and <cit.>. In two-level type theory (complete) (semi-)Segal types have been treated in <cit.>. Directed homotopy type theory with semantics in  categories has been discussed by North <cit.>, and bicategorical directed type theory has been introduced by Ahrens–North–van der Weide <cit.>. Earlier, directed variants of type theories have been considered by Warren <cit.> and Licata–Harper <cit.>. Synthetic notions of variance has been studied by Nuyts <cit.>.

Perspectives on directed type theories in connections with synthetic higher categories and/or fibrations are given in <cit.>.

§ SYNTHETIC FIBERED (∞,1)-CATEGORY THEORY: A QUICK STARTING GUIDE

§.§ Homotopy type theory

The basic objects in dependent type theory are families $A$ of types, depending on contexts $\Gamma$, indicated by the judgment $\Gamma \vdash A$. A context $\Gamma$ is a finite list of variable declarations. So if $\Gamma \jdeq [x_1 : A_1, \ldots, x_n : A_n]$, then $\Gamma \vdash A$ means that $A \defeq A(x_1, \ldots, x_n)$ is a family of types depending on the free variables $x_1 : A_1, \ldots, x_n : A_n$.

If $\Gamma \jdeq [ \, \, \,]$ is the empty context then a dependent type $\Gamma \vdash A$ is just a single, constant type $A$. A type $A$ is inhabited by terms or elements $a : A$.

If $\Gamma \vdash A$, we can consider the extended context

\[ \Gamma.A \jdeq [x_1 : A_1, \ldots, x_n : A_n, y : A(x_1,\ldots,x_n)].\]

Given families $\Gamma \vdash A$ and $\Gamma.A \vdash B$, there are two important new constructions. We can form $\Sigma$-types or dependent sum types $\Gamma \vdash \sum_{a:A} B(a)$ whose elements are pairs $\pair{a}{b}$ with $a:A$ and $b:B(a)$. If $A$ is a constant dependent type, then $\sum_{a:A} B(a)$ coincides with the cartesian product type $A \times B$.

Again, given dependent types $\Gamma \vdash A$ and $\Gamma.A \vdash B$, we can form the $\Pi$-type or dependent function type $\Gamma \vdash \prod_{a:A} B(a)$. The elements are given by dependent functions, or sections, $x : \Gamma.A \vdash f(x) : B(x)$, which can be thought of functions with “varying codomain.” In case $\Gamma$ is the empty context, the $\Pi$-type $\prod_{a:A} B(a)$ coincides with the ordinary function type $A \to B$.

Given a dependent term $x : \Gamma.A \vdash f(x) : B(x)$ we denote the corresponding dependent function via the $\lambda$-constructor $\Gamma \vdash \lambda x.f(x) : \prod_{a:A} B(a)$.

A crucial ingredient for homotopy type theory are Martin-Löf's identity types: given a type $A$ and terms $x,y:A$ one can consider the identity type or path type $(x=_Ay)$ (often just abbreviated as $(x=y)$) whose terms are witnesses or paths identifying the points $x$ and $y$. There always exists the canonical reflexivity path $\refl_x : (x=_A x)$ for $x:A$, and the identity types satisfy an induction principle (akin to the Yoneda Lemma) stating that the reflexivity terms inductively generate the family $x : A, y : A \vdash (x=_A y)$.

Two terms $x,y : A$ being judgmentally equal, $x \jdeq y$, entails that there exists an identification $p : (x=_A y)$, but in an intensional type theory (such as HoTT) the converse is not true.

We want to assume a (hierarchy of) universe(s) $\UU$ of all small types, implementing the idea of Grothendieck universes, well-known from category theory inside set theory. Though not material for most of our work, it is convenient to assume Voevodsky's univalence axiom stating that in a canonical way the paths of the universes, as captured by its identity type, coincide with the weak equivalences, , bi-invertible functions between types.

Univalence yields a straightening-unstraightening construction on the level of types, see <Ref>. Namely, we can understand a dependent type $\Gamma \vdash A$ either as family $A : \Gamma \to \UU$, where $\Gamma \jdeq A_1 \times \ldots \times A_n$ or as a “fibration” $\sum_{a:A} B(a) \to A$.

Indeed, by path induction, one can show that any type family $P : A \to \UU$ behaves like a fibration in the topological sense in that it supports a path transport operation $(-)_!^P : \prod_{a,b:A} \prod_{u:(a=_Ab)} P(a) \to P(b)$. For a path $u : (a=_A b)$ and points $x : P(a)$, $y : P(b)$, the path type $(u_!^P(x) =_{P(b)} y)$ gets identified with the type $(x =^P_u y)$ (short: $(x=_uy)$) of paths over $u$, , paths $\varphi : (\pair{a}{x} =_{\sum_{x:A} B(x)} \pair{b}{y})$ such that $\pr_1(\varphi) = u$. In this way, we can think of type families also supporting path lifting, in line with the topological intution.

In this sense the family $x,y :A \vdash (x=_A y)$ can be identified with a path space fibration $\mathrm{Path}(A) \to A \times A$ in a model category <cit.>.

More background on homotopy type theory can be found in  <cit.>.

§.§ Simplicial homotopy type theory

Simplicial (homotopy) type theory (s(Ho)TT) has been introduced by Riehl–Shulman <cit.> as an extension of Martin–Löf type theory (MLTT) or homotopy type theory (HoTT), resp., to reason synthetically about $\inftyone$-categories. Building on this, there has been further work on directed univalence <cit.>, fibered $\inftyone$-category theory <cit.>, and co-/limits <cit.>.

We give a short overview on how sHoTT can be presented, and on the basic concepts we will need in this theory. For a longer exposition of the basics of this theory we refer to the original paper <cit.>, and for a detailed discussion of the fibrational prerequisites we refer to <cit.>.

§.§.§ Strict shapes

In usual dependent type theories, a type family $A$ depends on a context

\[ \Gamma \defeq [x_1 : A_1, \ldots, x_n : A_n] \vdash A.\]

This gets extended in simplicial type theory <cit.> where now types can depend on shapes that are defined as sub-polytopes of finite-dimensional cubes. One writes

\[ \Xi \; | \; \Phi \; | \; \Gamma \vdash A \]

where $\Xi$ denotes a cube, and $\Phi$ a (sub-)shape of $\Xi$.

A general cube is of the form $\I^n$, where $\I^1 \jdeq \I$ denotes the directed bipointed linear order

\[ (0 \le 1).\]

From this, one can define common shapes in the expected way, such as :

\begin{align*}
& \partial \Delta^1 \defeq \{ t:\I \; | \;  t \jdeq 0 \lor t \jdeq 1\}, \quad \Lambda_1^2 \defeq \{ \pair{t}{s} : \I \times \I  \; | \;  s \jdeq 0 \lor t \jdeq 1\}, \\
& \partial \Delta^2 \defeq \{ \pair{t}{s} : \I \times \I  \; | \;  s \jdeq t \lor s \jdeq 0 \lor t \jdeq 1\}.
\end{align*}

Strictness of the cube and shape layer refers to the fact emethat equality of shape terms $\Phi \vdash s \jdeq t$ is reflected as definitional equality in the type level.
As explained in <cit.> we also coerce the shapes to be types.

§.§.§ Extension types

Let be a shape inclusion $\Phi \subseteq \Psi$ (in some common cube context $\Xi$). We consider a family $P:\Psi \to \UU$ and a partial section $a:\prod_{t:\Phi} P(t)$. Then we can form the extension type

\[ \exten{\Psi}{P}{\Phi}{a}\]

consisting of all total sections $b:\prod_{t:\Psi} P(t)$ such that $t: \Phi \vdash a(t) \jdeq b(t)$:

\[\begin{tikzcd}
&& P \\
\Phi && \Psi
\arrow[hook, from=2-1, to=2-3]
\arrow[two heads, from=1-3, to=2-3]
\arrow["a", dotted, from=2-1, to=1-3]
\arrow["b"', curve={height=12pt}, dotted, from=2-3, to=1-3]
\end{tikzcd}\]

The rules for the extension type are similar to that of the usual $\Pi$-types but invoking the strict extension property,  <cit.>. The intuition is that $\Phi \hookrightarrow \Psi$ corresponds to a kind of cofibration along which we ask for extensions of a given section of the fibration $\Phi^*P \fibarr \Phi$. This idea originally goes back to unpublished work by Lumsdaine and Shulman, and it has also been used  in cubical type theory <cit.> to define path types <cit.>.

The extension types serve to define a notion of absolute and dependent hom-types, and analogous generalizations thereof to different shapes and higher cells. In particular, this gives rise to synthetic notions of $\infty$-groupoids  discrete types, pre-$\inftyone$-categories  Segal types, and $\inftyone$-categories  Rezk or complete Segal type. We briefly introduce and explain these notions in <Ref>. For a comprehensive treatment we refer to <cit.> and <cit.>.

In general, we will freely switch back and forth between type families and fibrations, in particular when defining notions of these. , defining the notion of a cocartesian family simultaneously introduces a notion of cocartesian fibration, and vice versa. For a formal justification,  <cit.>. Specifically, for any family we have the following type-theoretic version of the Grothendieck construction  straightening/unstraightening:

For the types

\[ \Fib(\UU) \defeq \sum_{A,B:\UU} A \to B, \qquad \Fam(\UU) \defeq \sum_{B:\UU} (B \to \UU)  \]

and maps

\begin{align*}
\partial_1 & \defeq \lambda A,B,\pi:A \to B.B:\Fib(\UU) \to \UU, \\
\pr_1 		& \defeq \lambda B,P:B \to \UU.B: \Fam(\UU) \to \UU,
\end{align*}

there is a fiberwise quasi-equivalence

\[\begin{tikzcd}
{\Fib(\UU)} && {\Fam(\UU)} \\
& \UU
\arrow["{\partial_1}"', from=1-1, to=2-2]
\arrow["{\pr_1}", from=1-3, to=2-2]
\arrow["\Un", shift left=1, from=1-3, to=1-1]
\arrow["\St", shift left=2, from=1-1, to=1-3]
\end{tikzcd}\]

at stage $B:\UU$ given by a pair

\[\begin{tikzcd}
{\UU/B} && {(B\to \UU)}
\arrow["{\St_B}", shift left=2, from=1-1, to=1-3]
\arrow["{\Un_B}", shift left=1, from=1-3, to=1-1]
\end{tikzcd}\]

with straightening

\[ \St_B(\pi) \defeq \lambda b.\fib_b(\pi)\]

and unstraightening

\[ \Un_B(P) \defeq \pair{\totalty{P}}{\pi_P}\]

($\pi_P: \totalty{P} \defeq \sum_{b:B} P\,b \to B$ the total space projection).

In particular, this yields a weak equivlence of maps $\Un_B \circ \St_B$ and $\id_{\UU/B}$, so for any map $E \to B$ we obtain a fibered equivalence, which we call the projection equivalence of $\pi$:

\[\begin{tikzcd}
E && {\sum_{b:B} b^*E} \\
& B
\arrow["\simeq", from=1-1, to=1-3]
\arrow["\pi"', from=1-1, to=2-2]
\arrow["{\pr_1}", from=1-3, to=2-2]
\end{tikzcd}\]

§.§ Synthetic $\infty$-categories

Recall the notion of extension type from <Ref>. Importantly, this will serve to define a tractable notion of synthetic $\infty$-category.

Let $A$ be a type with terms $x,y : A$. Then the extension type

\[ \hom_A(x,y) \defeq \ndexten{\Delta^1}{A}{\partial \Delta^1}{[x,y]} \]

is called the hom-type or type of directed arrows from $x$ to $y$.
We also write

\[ (x \to_A y) \defeq \hom_A(x,y),\]

or simply $(x \to y)$ if the underlying type is understood.

By the rules of extension types, a term $f : \hom_A(x,y)$ is exactly a function $f : \Delta^1 \to A$ such that $f\,0 \jdeq x$ and $f\,1 \jdeq y$.

To treat composites we have to consider diagrams of shape $\Delta^2$.

Let $A$ be a type with terms $x,y,z:A$. Then, assuming we are given $f : (x\to_A y)$, $g : (y \to_A z)$, and $h : (x \to_A z)$ (and leaving the endpoints implicit in the notation), we can consider the type

\[ \hom_A^2(f,g;h) \defeq \ndexten{\Delta^2}{A}{\partial \Delta^2}{[f,g,h]}. \]

By <Ref>, a Segal type $A$ admits composition of arrows, uniquely up to homotopy in the following sense: given terms $x,y,z : A$, arrows $f : (x \to_A y)$ and $g : (y \to_A z)$ there is some composite arrow $h : (x \to_A z)$ together with a $2$-simplex $\sigma_{f,g,h} : \hom_A^2(f,g;h)$ witnessing that $h$ is, in fact, a composite of $f$ and $g$; and more so, the type of this data is contractible.

We are now interested in singling out those simplicial types which always admit composition of (composable) arrows, uniquely up to homotopy. These will be our synthetic pre-$\inftyone$-categories.

A Segal type is a type $A$ such that

\[ \isSegal(A) \defeq \prod_{x,y,z:A} \prod_{\substack{f:(x \to_A y) \\  g:(y \to_A z)}} \isContr \Big( \sum_{h:\hom_A(x,z)} \hom_A^2(f,g,h) \Big).\]

One can show <cit.> that this is equivalent to being homotopically right orthogonal to the horn inclusion $\Lambda_1^2 \hookrightarrow \Delta^2$, see also <Ref>.

Based on the $\hom$-types we can define a notion of isomorphism.

Let $A$ be a type. Let $x,y : A$ and $f : \hom_A(x,y)$ be an arrow. We say $f$ is an isomorphism if and only if the proposition

\[ \isIso(f) \defeq \Big( \sum_{g:hom_A(y,x)} g\circ f = \id_x \Big) \times \Big( \sum_{h:hom_A(y,x)} f\circ h = \id_y \Big)  \]

is satisfied, where $\id_x \jdeq \lambda t.x : \hom_A(x,x)$ is the identity morphism of $x$.

The type of isomorphisms from $x$ to $y$ is then defined as

\[ \iso_A(x,y) \defeq (x \cong_A y) \defeq \sum_{f:\hom_A(x,y)} \isIso(f).\]

In particular, the identity maps can be shown to be isomorphisms. By path induction, we then obtain a comparison map

\[ \idtoiso_{A} : \prod_{x,y:A} (x =_A y) \to (x \cong_A y), \quad \idtoiso_{A,x,x}(\refl_x) \defeq \id_x.\]

This connects the new notion of isomorphism with the natively given notion of equivalence through paths.

§.§ Right orthogonal and LARI families

We will be concerned in our treatment with specific notions of fibrations, based on synthetic analogues of co-/cartesian fibrations, and occasionally also (discrete) left/right fibrations. However, for both conceptual and technical purposes it will be instructive to introduce the general patterns behind those definitions: right orthogonality and LARI/RARI conditions.

We remark that the notion of iso-/inner family is not so much of conceptual interest, but rather of technical convenience,  also the discussion at the beginning of <cit.>.

§.§.§ Directed arrows in type families

Let $P : B \to \UU$ be a type family with $a,b:B$ and $u: (a \to_B b)$. After <cit.>, we can then consider the type dependent homomorphisms or dependent arrows. For $x:P\,a$ and $y : P\,b$, the type of (dependent) arrows in $P$ over $u$ is given by

\[ \mathrm{dhom}_{P,a,b,u}(x,y) \defeq (x \to_u^P y) \defeq (x \to_u y) \defeq \exten{t:\Delta^1}{P(t)}{\partial \Delta^1}{[x,y]}.\]

Analogously, we can define dependent versions of $\hom^2$ and any other possible shape inclusion. This naturally leads to relative versions of the Segal and Rezk conditions, which we will take as the basis of all of our following theory: we will consider isoinner fibrations/families over a Rezk base type. This means, the base type behaves like a category, and so will the total type as well as all the fibers, compatible with the canonical projection from the total type to the base. But these families need not satisfy lifting properties w.r.t directed arrows (though they do w.r.t. the ordinary path types from standard homotopy type theory, like any type family). The precise setting for (iso)inner families is given in <cit.>, and we recall it briefly in the following.

§.§.§ Fibrations and fibered maps

We are introducing the notation $\pi : E \fibarr B$ for map between if we want to view it as a fibration of some kind. In writing so, we are somewhat imprecise in that it could mean different things: sometimes it just describes a map $\pi : E \fibarr B$ between types, but to be viewed as a fibration in a slice category over $B$, in the model. This is emphasize its role somewhat akin to to that of an (axiomatic) isofibration in the sense of $\infty$-cosmos theory <cit.>. E.g., when considering a square

\[\begin{tikzcd}
E & F \\
B & A
\arrow["\pi"', two heads, from=1-1, to=2-1]
\arrow["k", from=2-1, to=2-2]
\arrow["\xi", two heads, from=1-2, to=2-2]
\arrow["\varphi", from=1-1, to=1-2]
\end{tikzcd}\]

of maps between types, really all maps occuring could be written as $\fibarr$ (by projection equivalence). But the intuition is that a square like this encodes a fibered map $\pair{k : B \to A}{\varphi : (b :B) \to P(b) \to Q(k(b))}$ (where $P$ and $Q$, resp., denote the straightening of $E$ and $F$, resp.), so we do not regard $k$ and $\varphi$ as fibrations (but rather, as a fibered functor between fibered categories.[Though we will soon also consider certain fibered functors (between fibrations placed in the vertical direction) that can be regarded as fibrations themselves (placed in the horizontal direction).]

Sometimes $\fibarr$ might specifically mean that we are considering a (co)cartesian fibration or some related notion, which will be made explicit by the context.

§.§.§ Right orthogonal families

Let $P:B \to \UU$ be a family. Given a type map or shape inclusion $j:Y \to X$, we say that $P$ is right orthogonal to $j$ or a (right) $j$-orthogonal family, written $j \bot P$, if and only if the proposition

\[ \prod_{v:X \to B} \prod_{f:(t:Y) \to P(v\,t)} \isContr\Big( \sum_{g:(t:X) \to P(v\,t)} j^*(g) =^P_v f \Big)\]

is satisfied.

In case $B \simeq \unit$, the family $P$ can be identified with a single type $A$. In this case we say that $A$ is right orthogonal to $j$ and write $j \bot A$.

Let $\pi:E \fibarr B$ denote the projection associated to a family $P:B \to \UU$. Then $P$ is $j$-orthogonal if and only if the type of fillers $g$ in any diagram as follows is contractible:

\[\begin{tikzcd}
\Phi && E \\
\Psi && B
\arrow["j"', hook, from=1-1, to=2-1]
\arrow["v"', from=2-1, to=2-3]
\arrow["f", from=1-1, to=1-3]
\arrow["\pi", two heads, from=1-3, to=2-3]
\arrow["g"{description}, dashed, from=2-1, to=1-3]
\end{tikzcd}\]

In case of a shape inclusion $j: \Phi \hookrightarrow \Psi$ a family $P$ is right orthogonal to $j$ if and only if

\[ \prod_{v:\Phi \to B} \prod_{f:(t:Y) \to P(v\,t)} \isContr\Big( \exten{\Psi}{P}{\Phi}{f}\Big), \]

*  A type family is inner if it is right orthogonal to the horn inclusion $\Lambda_1^2 \hookrightarrow \Delta^2$. A Segal type is a type that is inner when seen as a family over the $\unit$.

*  An inner family is isoinner if it is right orthogonal to the terminal projection $\mathbb{E} \to \unit$, where $\mathbb{E}$ denotes the free bi-invertible arrow,  <cit.>. A Rezk type or complete Segal type is a type that is isoinner (again, when seen as a family over $\unit$).

The Segal types are exactly the synthetic pre-$\inftyone$-categories[ <cit.> and <cit.> for a general discussion.] in our setting while the Rezk types are precisely the synthetic $\inftyone$-categories.

The condition of being a co- or contravariant discrete family (meaning $\infty$-groupoid valued) can be naturally expressed in terms of a right orthogonality condition, as originally worked out in <cit.>. Over a point this of course specializes to the type being a synthetic $\infty$-groupoid.

A family is covariant if it is right orthogonal to the shape inclusion $0: \unit \hookrightarrow \Delta^1$. Dually, it is contravariant if it is right orthogonal to the shape inclusion $1: \unit \hookrightarrow \Delta^1$.

Over a point, in either of these cases we call the ensuing type discrete.

§.§.§ LARI families

Co-/cartesian families can be characterized in terms of certain adjoint existence criteria. Namely, a map $\pi: E \fibarr B$ is a synthetic cocartesian fibration iff the Leibniz cotensor

\[\begin{tikzcd}
{E^{\Delta^1}} && {\comma{\pi}{B}}
\arrow[""{name=0, anchor=center, inner sep=0}, curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=12pt}, dotted, from=1-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

has a left adjoint right inverse (LARI),  <cit.> and <cit.>. If the latter map exists, it exactly functions as the lifting map, mapping a pair $\pair{u:b \to_B b'}{e:P\,b}$ to its cocartesian lift $P_!(u,e): e \cocartarr^P_u e'$.

Formally generalizing this condition to any shape inclusion leads to the notion of LARI family or LARI fibration, , maps $\pi: E\to B$ such that for a certain shape inclusion or type map $j:Y \to X$ the following induced map has a LARI:

\[\begin{tikzcd}
{E^X} \\
&& {B^X \times_{B^Y} E^Y} && {E^Y} \\
&& {B^X} && {B^Y}
\arrow["{B^j}"{description}, from=3-3, to=3-5]
\arrow["{\pi^Y}", from=2-5, to=3-5]
\arrow[from=2-3, to=2-5]
\arrow[from=2-3, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-5]
\arrow["{\pi^X}"{description}, curve={height=18pt}, from=1-1, to=3-3]
\arrow["{E^j}"{description}, curve={height=-24pt}, from=1-1, to=2-5]
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=2-3]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=12pt}, dotted, from=2-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-135}, draw=none, from=1, to=0]
\end{tikzcd}\]

LARI adjunctions in simplicial HoTT have been studied in <cit.>, extending the work on adjunctions in simplicial HoTT by Riehl–Shulman <cit.>. This in turn extends the study of adjunctions in plain HoTT <cit.>. In the semantic picture, Riehl–Shulman's theory of adjunction can be understood to internalize parts of of Riehl–Verity's theory of homotopy coherent adjunctions <cit.>. In particular, they show in op. cit. that a $2$-categorical adjunction extends to a fully homotopy coherent one. In <Ref> we extend the setup of <cit.> by a fibered version of LARI adjunction.

Let $j:Y \to X$ be a shape inclusion or type map. A family $P: B \to \UU$ is a $j$-LARI family if for its unstraightening $\pi \defeq \pi_P : E \to B$ the following Leibniz cotensor map has a LARI:

\[\begin{tikzcd}
{E^X} && {E^Y\times_{B^Y} B^X}
\arrow[""{name=0, anchor=center, inner sep=0}, "{j \cotens \pi}"', curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=12pt}, dotted, from=1-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

§.§ Co-/cartesian families

§.§.§ Cocartesian families

We only treat the covariant case. The contravariant case replaces the initial vertex $i_0 : \unit \hookrightarrow \Delta^1$ with the terminal one $i_1: \unit \hookrightarrow \Delta^1$ and left adjoint inverses (LARIs) with right adjoint inverses (RARIs).

Let $P:B \to \UU$ be an isoinner family over a Rezk type $B$. An arrow $f:e \to_u^P e'$ over an arrow $u: b \to_B b'$ is $P$-cocartesian if and only if

\[\isCocartArr_u^P(f) \defeq \prod_{b'':B} \prod_{v:b' \to b''} \prod_{e'':P\,b''} \prod_{h:e \to^P_{vu} e''} \isContr\Big( \sum_{g: e' \to^P_v e''} h =_{vu}^P gf \Big).\]

An isoinner family over a Rezk type $B$ is cocartesian if and only if for $u:b \to_B b'$ and $e:P\,b$  the type

\[ \sum_{e':P\,b'} \sum_{f:e \to^P_u e'} \isCocartArr_u^P(f)  \]

is inhabited.

Given $P,u,e,e'$ as above, we will denote the subtype of cocartesian arrows as $(e\cocartarr^P_u e') \hookrightarrow (e \to^P_u e')$, and likewise for the actual arrows in the illustrating figures.

One can show that the inhabitedness condition from the above definition implies contractibility. In other words, cocartesian lifts of a given arrow in the base are determined uniquely up to homotopy by their source vertex.

Connecting back with <Ref> we can express being a cocartesian family as a LARI condition.

Let $B$ be a Rezk type, $P: B \to \UU$ be an isoinner family, and denote by $\pi: E \to B$ the associated projection map. The family $P$ is cocartesian if and only if the Leibniz cotensor map $i_0 \cotens \pi: E^{\Delta^1} \to \comma{\pi}{B}$ has a left adjoint right inverse:

\[\begin{tikzcd}
{E^{\Delta^1}} & {} \\
&& {\pi \downarrow B} && E \\
&& {B^{\Delta^1}} && B
\arrow[two heads, from=2-3, to=3-3]
\arrow["{\partial_0}"', from=3-3, to=3-5]
\arrow[from=2-3, to=2-5]
\arrow["\pi", two heads, from=2-5, to=3-5]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-5]
\arrow["{\partial_0}", shift left=2, curve={height=-18pt}, from=1-1, to=2-5]
\arrow[""{name=0, anchor=center, inner sep=0}, "\chi"', curve={height=12pt}, dashed, from=2-3, to=1-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{i_0\widehat{\pitchfork}\pi}"', curve={height=12pt}, from=1-1, to=2-3]
\arrow["{\pi^{\Delta^1}}"', shift right=2, curve={height=18pt}, two heads, from=1-1, to=3-3]
\arrow["\dashv"{anchor=center, rotate=-118}, draw=none, from=0, to=1]
\end{tikzcd}\]

In <Ref> the stipulated LARI acts as the lifting map $\chi: \comma{\pi}{B} \to E^{\Delta^1}$ with $\chi(u,e) \defeq P_!(u,e): e \cocartarr^P_u u_!\,e$. It is also possible to state cocartesianness in terms of a transport map $\tau: \comma{\pi}{B} \to_B E$, $\tau(u,e) \defeq u_!\,e : P(\partial_1 \,u)$. This is the content of the next theorem.

Let $B$ be a Rezk type, and $P:B \to \UU$ an isoinner family with associated total type projection $\pi:E \to B$.

Then, $P$ is cocartesian if and only if the map

\[ \iota \defeq \iota_P : E \to \comma{\pi}{B}, \quad \iota \, \pair{b}{e} :\jdeq \pair{\id_b}{e}  \]

has a fibered left adjoint $\tau \defeq \tau_P: \comma{\pi}{B} \to E$ as indicated in the diagram:

\[\begin{tikzcd}
{} && E && {\pi \downarrow B} \\
\\
&&& B
\arrow[""{name=0, anchor=center, inner sep=0}, "\iota"', curve={height=12pt}, from=1-3, to=1-5]
\arrow["\pi"', two heads, from=1-3, to=3-4]
\arrow["{\partial_1'}", two heads, from=1-5, to=3-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "\tau"', curve={height=12pt}, from=1-5, to=1-3]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

The adjoint criteria from <Ref> are of central importance for a variety of reasons. First, they imply a lot of closure properties,  <cit.> and <cit.>. Next, they are generalized in our present study to fibered and two-sided situations. Finally, from a broader perspective in model-independent higher category theory the adjoint criteria à la Chevalley, Gray, Street, are taken by Riehl–Verity as “reference definitions” for co-/cartesian fibrations internal to an arbitrary $\infty$-cosmos. It turns out that there is also an equivalent definition <cit.> directly on $2$-cells but the adjoint criteria are more fit to readily yield an internal definition.

In fact, recently Riehl–Verity showed that co-/cartesian arrows in the $\infty$-cosmological sense can also be characterized by Chevalley-type criteria,  <cit.>. This does not play a role in the present text but has been discussed in <cit.> within simplicial HoTT.[Generalizing to arbitrary shape inclusions or type maps again this gives rise to the notion of $j$-LARI cell.]

§.§.§ Cartesian families

Dually to the cocartesian case and the left adjoint (right inverse) characterizations, we can consider cartesian fibrations and right adjoint (right inverse) characterizations. Similarly, this can be expressed as a (contravariant) lifting condition w.r.t. cartesian arrows.

Given a cartesian family $P:B \to \UU$ over $u:b \to_B a$, for $e:P\,b$ and $d:P\,a$, we denote by $(d \cartarr^P_u e) \hookrightarrow (d \to^P_u e)$ the subtype of cartesian arrows. The cartesian lift  $e:P\,a$ is denoted by $P^*(u,e): u^*_P\,e \cartarr^P_u e$, where $u^*_P\,e$ is the cartesian transport of $e$ by $u$.

§.§.§ Cocartesian functors

We conclude our overview with a brief consideration of cocartesian functors in this setting. Those also turn out to be characterizable in terms of Chevalley criteria.[We obtain a formally analogue characterization via Chevalley criteria in the context of $j$-LARI cells and $j$-LARI-cell-preserving functors,  <cit.>.]

If $P$ and $Q$ are cocartesian families, and furthermore the map

\[ \Phi: \totalty{P} \to \totalty{Q}, \quad \Phi \, b \, e :\jdeq \pair{j(b)}{\varphi_j(e) } \]

preserves cocartesian arrows, then we call $\Phi$ a cocartesian map:[This is a proposition because being a cocartesian arrow is a proposition.]

\[ \isCocartFun_{P,Q}(\Phi) :\jdeq \prod_{f:\Delta^1\to \widetilde{P}} \isCocartArr_P(f) \to \isCocartArr_Q(\varphi f).\]

In particular, if $B$ and $C$ in addition are Segal (or Rezk) types we speak of a cocartesian functor.

We define

\[ \CocartFun_{B,C}(P,Q) :\jdeq \sum_{F:\FibMap_{B,C}(P,Q)} \isCocartFun_{P,Q}(F).\]

Given families $P: B \to \UU$ to $Q: B \to \UU$, a fibered functor from $P \to Q$ is a section $\varphi : \prod_{x:B} Px \to Qx$. It is cocartesian if

\[ \isCocartFun_{P,Q}(\pair{\id_B}{\varphi}) \equiv \prod_{\substack{u:\Delta^1 \to B \\ f: \Delta^1 \to u^*P}} \isCocartArr_P(f) \to \isCocartArr_Q(\varphi f).\]

We define

\[ \CocartFun_{B}(P,Q) :\jdeq \sum_{\varphi:\prod_B P \to Q} \isCocartFun_{P,Q}(\pair{\id_B}{\varphi}).\]

Let $A$ and $B$ be Rezk types, and consider cocartesian families $P:B \to \UU$ and $Q:A \to \UU$ with total types $E\defeq \totalty{P}$ and $F\defeq \totalty{F}$, resp.

For a fibered functor $\Phi\defeq \pair{j}{\varphi}$ giving rise to a square

\[
\begin{tikzcd}
F \ar[r, "\varphi"] \ar[d, "\xi" swap, two heads] & E \ar[d, "\pi", two heads] \\
A \ar[r, "j" swap] & B
\end{tikzcd}
\]

the following are equivalent:

* The fiberwise map $\Phi$ is a cocartesian functor.

* The mate of the induced canonical fibered natural isomorphism is invertible, too:

\[\begin{tikzcd}
{F} && {E} & {} & {F} && {E} \\
{\xi \downarrow A} && {\pi \downarrow B} & {} & {\xi \downarrow A} && {\pi \downarrow B}
\arrow["{i}"', from=1-1, to=2-1]
\arrow["{\varphi}", from=1-1, to=1-3]
\arrow["{i'}", from=1-3, to=2-3]
\arrow[Rightarrow, "{=}", from=2-1, to=1-3, shorten <=7pt, shorten >=7pt]
\arrow["{\rightsquigarrow}" description, from=1-4, to=2-4, phantom, no head]
\arrow["{\kappa}", from=2-5, to=1-5]
\arrow["{\varphi}", from=1-5, to=1-7]
\arrow["{\varphi \downarrow j}"', from=2-5, to=2-7]
\arrow["{\kappa'}"', from=2-7, to=1-7]
\arrow[Rightarrow, "{=}"', from=2-7, to=1-5, shorten <=7pt, shorten >=7pt]
\arrow["{\varphi \downarrow j}"', from=2-1, to=2-3]
\end{tikzcd}\]

* The mate of the induced canonical natural isomorphism is invertible, too:

\[\begin{tikzcd}
{F^{\Delta^1}} && {E^{\Delta^1}} & {} & {F^{\Delta^1}} && {E^{\Delta^1}} \\
{\xi \downarrow A} && {\pi \downarrow B} & {} & {\xi \downarrow A} && {\pi \downarrow B}
\arrow["{r}"', from=1-1, to=2-1]
\arrow["{\varphi \downarrow j}"', from=2-1, to=2-3]
\arrow["{\varphi^{\Delta^1}}", from=1-1, to=1-3]
\arrow["{r'}", from=1-3, to=2-3]
\arrow["{\rightsquigarrow}" description, from=1-4, to=2-4, phantom, no head]
\arrow[Rightarrow, "{=}", from=2-1, to=1-3, shorten <=7pt, shorten >=7pt]
\arrow["{\ell}", from=2-5, to=1-5]
\arrow["{\varphi \downarrow j}"', from=2-5, to=2-7]
\arrow["{\varphi^{\Delta^1}}", from=1-5, to=1-7]
\arrow["{\ell'}"', from=2-7, to=1-7]
\arrow[Rightarrow, "{=}"', from=2-7, to=1-5, shorten <=7pt, shorten >=7pt]
\end{tikzcd}\]

§.§.§ Closure properties of co-/cartesian families and functors

Over Rezk bases, it holds that:

Cocartesian families are closed under composition, dependent products, pullback along arbitrary maps, and cotensoring with maps/shape inclusions. Families corresponding to equivalences or terminal projections are always cocartesian.

Between cocartesian families over Rezk bases, it holds that:
Cocartesian functors are closed under (both horizontal and vertical) composition, dependent products, pullback, sequential limits,[all three objectwise limit notions satisfying the expected universal properties  to cocartesian functors] and Leibniz cotensors.

Fibered equivalences and fibered functors into the identity of $\unit$ are always cocartesian.

§ SLICED COCARTESIAN FAMILIES

The main object of study of this paper are two-sided cartesian fibrations $E \fibarr A \times B$. It turns out to be instructive to analyze this notion by means of fibered or sliced fibrations, , fibered functors $\varphi$ between fibrations

\[\begin{tikzcd}
F && E \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["\pi", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

where $\varphi$ is regarded itself as a fibration of some kind, over the base $\pi$ (itself a fibration). This is the point of view developed by Riehl–Verity in <cit.>, and we adapt it here. For this purpose, we develop in this section the theory of fibrations fibered or sliced over a fibration. While the development undoubtedly presents itself as technical, it will prove instrumental in our main theorems about the characterization of two-sided cartesian families and their closure properties, see <Ref>.

§.§ Sliced constructions

We introduce here type-theoretic versions of a few sliced constructions,  <cit.>.

Let $\pi:E\fibarr B$ be a map, and $X$ be a type or shape. The sliced exponential (over $B$) of $\pi$ by $X$  is given by the map $(X \iexp E) \to B$ defined as:

\[\begin{tikzcd}
{X \slcotens E} && {E^X} \\
B && {B^X}
\arrow[two heads, from=1-1, to=2-1]
\arrow["{\mathrm{cst}}"' description, from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\pi^X}", two heads, from=1-3, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

This means $X \slcotens E \simeq \sum_{b:B} X \to P\,b$.
In particular, for $X \jdeq \Delta^1$, we obtain the vertical arrow type $\VertArr_\pi(E) \to B$. We often identify vertical arrows $f: e \to^P_{\id_b} e'$ with $f: e \to_{P\,b} e'$.

Let $I$ and $B$ be types, and consider maps $\pi_i:E_i \fibarr B$ for $i:I$. The sliced product over the $\pi_i$ is defined by pullback:

\[\begin{tikzcd}
{\times_{i:I}^B E_i} && {\prod_{i:I} E_i} \\
B && {B^I}
\arrow["{\times_{i:I}^B \pi_i}"', two heads, from=1-1, to=2-1]
\arrow[from=2-1, to=2-3, "{\mathrm{cst}}"' description]
\arrow[from=1-1, to=1-3]
\arrow["{\prod_{i:I} \pi_i}", two heads, from=1-3, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

Consider a cospan $\psi:F \to_B G \leftarrow_B E: \varphi$ of fibered functors, giving rise to the sliced comma type $\relcomma{B}{\varphi}{\psi}$:

\[\begin{tikzcd}
{\varphi \downarrow_B \psi} && {\VertArr(G)} \\
{F \times E} && {G \times G} \\
& B
\arrow[from=1-1, to=2-1]
\arrow["{\psi \times \varphi}"{description}, from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\langle \partial_1,\partial_0\rangle}", from=1-3, to=2-3]
\arrow[two heads, from=2-1, to=3-2]
\arrow[two heads, from=2-3, to=3-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

§.§ Sliced cocartesian families

Let $B$ be a Rezk type.  A sliced cocartesian family over $B$ is given by the following data:

* an isoinner family $P: B \to \UU$,

* an isoinner family $K: \totalty{P} \to \UU$,

* and, writing $Q \defeq \Sigma_{\totalty{P}} K$, a witness for the proposition[recall the uniqueness of cocartesian lifts,  <cit.>]

\[ \prod_{b:B} \prod_{\substack{f:\Delta^1 \to P\,b \\ x:Q(b,f0)}} \sum_{\substack{x':Q(b,f1) \\ k:x \to^Q_{b,f} x'}} \isCocartArr^Q_f(k).\]

We call $K$ a cocartesian family sliced over $B$ with base $P$, and denote the ensuing cocartesian lifts as

\[ K_!^b(f,x) \defeq K_!(b,f,x):x \cocartarr^K_{\pair{b}{f}} f_!^{K,b}\,x.\]

Perhaps more familiarly, in fibrational terms, a cocartesian fibration sliced over $B$ with base $\pi$ is given by a fibered functor $\varphi: \xi \to_B \pi$, where $\xi: F \fibarr B$ and $\pi:E \fibarr B$ are isoinner fibrations over $B$, visualized through

\[\begin{tikzcd}
F && E \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["\pi", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

moreover satisfying the analogous lifting property: any $\pi$-vertical arrow has a $\varphi$-cocartesian lift.

As previously with ordinary cocartesian families, we will often bring in the fibrational viewpoint and reason diagrammatically.

This is a type-theoretic formulation of what, more generally in $\infty$-cosmos theory, defines for any $\infty$-cosmos $\mathcal K$ and an object $B \in \mathcal K$ a cocartesian family in the slice-$\infty$-cosmos $\mathcal K/B$. This is captured internally by the following theorem, which shows that the above condition precisely amounts to the sliced version of the familiar LARI condition for cocartesian families.

Given a Rezk type $B$, let $P:B \to \UU$ and $K: \totalty{P} \to \UU$ be isoinner families. We write $Q \jdeq \Sigma_{\totalty{P}} K:B \to \UU$, and denote

\[ \pi  \defeq \Un_B(P) :  E \defeq \totalty{P} \fibarr B, \quad \xi \defeq \Un_B(Q) :  F \defeq \totalty{Q} \fibarr B, \]

\[  \varphi \defeq \Un_E(K): F \to E  :\]

\[\begin{tikzcd}
F && E && {\widetilde{Q} \simeq \widetilde{K}} && {\widetilde{P}} \\
& B & {} && {} & B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["\pi", two heads, from=1-3, to=2-2]
\arrow["{\pi_K}", from=1-5, to=1-7]
\arrow["{\pi_Q \jdeq \pi_{\Sigma_{\totalty{P}}\,K}}"{description}, two heads, from=1-5, to=2-6]
\arrow["{\pi_P}", two heads, from=1-7, to=2-6]
\arrow[squiggly, tail reversed, from=1-3, to=1-5]
\end{tikzcd}\]

Then the following are equivalent propositions:

*  The family $K: E \to \UU$ is a cocartesian family sliced over $B$.

*  The sliced Leibniz cotensor $i_0 \cotens_B \varphi: \VertArr_{\xi}(F) \to_B \relcomma{B}{\varphi}{E}$ has a fibered LARI:

\[\begin{tikzcd}
{\VertArr_{\xi}(F) } &&  {\varphi \downarrow_B E} \\
\\
& B
\arrow[""{name=0, anchor=center, inner sep=0}, "{i_0 \widehat{\pitchfork}_B \varphi}"', curve={height=6pt}, from=1-1, to=1-3]
\arrow[two heads, from=1-1, to=3-2]
\arrow[two heads, from=1-3, to=3-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\chi_B}"', curve={height=6pt}, dashed, from=1-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

*  The fibered inclusion map $\iota_\varphi: F \to_E \relcomma{B}{\varphi}{E}$ has a fibered left adjoint:

\[\begin{tikzcd}
F &&&& {\varphi \downarrow_B E} \\
&& E \\
\\
&& B
\arrow["\varphi"{description}, from=1-1, to=2-3]
\arrow["{\partial_1}"{description}, from=1-5, to=2-3]
\arrow["\pi"{description}, two heads, from=2-3, to=4-3]
\arrow["\xi"{description}, two heads, from=1-1, to=4-3]
\arrow["{\partial_1'}"{description}, two heads, from=1-5, to=4-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\iota_\varphi}"{description}, from=1-1, to=1-5]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\tau_\varphi}"{description}, curve={height=18pt}, dashed, from=1-5, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-91}, draw=none, from=1, to=0]
\end{tikzcd}\]

$\ref{it:sl-cocart-fam-char-ii} \implies \ref{it:sl-cocart-fam-char-i}$
We abbreviate $r\defeq i_0 \widehat{\pitchfork}_B \varphi$. After the usual projection equivalence, we can identify it as the fiberwise map with components

\[ r_b \big( f:e \to_{P\,b} e', k:x \to^Q_f x' \big) \defeq \langle e, f, x \rangle \jdeq \langle \partial_0 \,f, f, \partial_0 k \rangle \]

for $b:B$.

Assume, the stated fibered LARI condition is satisfied.
First we note that the invertible unit, for every $b:B$, exhibits $\chi_{B,b}$ as a (strict) section of $r_b$,   given $e:P\,b$, $f:\comma{e}{P\,b}$ and $x:Q(b,e)$, we can assume $\chi_{B,b}(e,f,x):x \to^Q_f x'$ for some $x':Q(b,\partial_1\,f)$.
We have a fibered equivalence

\begin{align*}  & \prod_{\substack{b,b':B \\ u:b \to_B b'}} \prod_{\substack{e,e':P\,b \\ f:e \to_{P\,b} e' \\ x:Q(b,e)}} \prod_{\substack{d,d':P(b') \\ g:d \to_{P\,b'} d'}}
\prod_{\substack{y:Q(b',d), y':Q(b',d') \\ m:y \to^Q_g y'}} \cdots \\
& \cdots ( \chi_B(e,f,x) \to_u \langle g,m \rangle) \stackrel{\simeq}{\longrightarrow} ( \langle e,f,x \rangle \to_u \langle d, g,y \rangle).
\end{align*}

Just as in the second part of the proof of <Ref>, by specializing to the case that $m= \id_{x''}$ and $g=\id_{e''}$ for some $e'':P(b')$ and $x'':Q(b',e'')$, we find that the lift $\chi_{B,b}(e,f,x)$ is a $K$-cocartesian lift of the $P$-vertical arrow $f:e \to_{P\,b} e'$.

$\ref{it:sl-cocart-fam-char-i} \implies \ref{it:sl-cocart-fam-char-ii}$
On the other hand, suppose that $K$-cocartesian lifts of all $P$-cocartesian maps exist,  to a given initial vertex. Accordingly, we define $\chi_{B,b}(e,f,x)\defeq K^b_!(f,x) : x \cocartarr_f^K x'$. Again, analogously to the first part of the proof, we define a pair of maps

\[\begin{tikzcd}
{\left( \chi_{B,b}(e,f,x) \to_u \langle g,m\rangle\right)} && {\left( \langle e,f,x\rangle \to_u \langle d,g,y\rangle\right)}
\arrow[""{name=0, anchor=center, inner sep=0}, "\Phi", shift left=2, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\Psi", shift left=2, from=1-3, to=1-1]
\arrow["\simeq"{description}, shorten <=1pt, shorten >=1pt, Rightarrow, from=0, to=1]
\end{tikzcd}\]

\begin{align*}
& \Phi(h:e \to_u^P d, h': e' \to^P_u d', k: x \to^K_h y, k': x' \to^K_{h'} y') \defeq \langle h, h', k \rangle  \\
& \Psi(h:e \to_u^P d, h': e' \to^P_u d', k:x \to_h^K y) \defeq \langle h, h', k, \tyfill^K_{\chi_{B,b}(e,f,x)}(m \circ k) \rangle.
\end{align*}

Due to cocartesianness of $\chi_{B,b}(e,f,x)$ these are quasi-inverse to each other. In particular, the components of $\Phi$ are defined by applying the right adjoint $i_0 \cotens_B \varphi$. For the unit of the adjunction, we take reflexivity, and taken together this defines a fibered LARI adjunction.

$\ref{it:sl-cocart-fam-char-i} \implies \ref{it:sl-cocart-fam-char-iii}$ The fiberwise map $\iota_\varphi: F \to_E \relcomma{B}{\varphi}{E}$ is given by

\[ \iota_\varphi(b,e,x)\defeq \angled{b,e,e,\id_e,x}. \]

Because of the preconditions we can define the candidate fibered left adjoint $\tau_\varphi: \relcomma{B}{\varphi}{E} \to_E F$ by

\[ \tau_\varphi(b,e',e,f:e \to_{P\,b} e', x:Q(b,e)) \defeq \angled{b,e',f^Q_!(x):Q(b,e')}, \]

as we would expect analogously to <Ref>.
To obtain a fibered adjunction as desired, recalling <Ref>, <Ref>, we want to define a family of equivalences

\[ \Phi: \prod_{\substack{b:B \\ e':P\,b}} \prod_{\substack{e:P\,b, x:K\,b\,e\\ f:e \to_{P\,b} e'}} \prod_{x':K\,b\,e'} \Big( \underbrace{\tau_\varphi(e,f,x)}_{\jdeq f_!x} \longrightarrow_{K(b,e')} x' \Big) \stackrel{\simeq}{\to} \Big( x \longrightarrow^{Q}_{b,f} x'\Big) : \Psi, \]

generalizing <Ref>, by[Note that for the codomain of the equivalence we have identified the type of morphisms $\Big(\angled{e,f,x} \longrightarrow \angled{e',\id_{e'}, x'} \Big)$ (in the fiber $\sum_{g:\comma{P\,b}{e'}} Q(b,\partial_0\,g)$) with simply $(x \to^{b^*Q}_f x')$.]

\begin{align*} \Phi_{b,e'}\big( m:f_!\,x \to_{Q\,b\,e'} x'\big) & \defeq m \circ Q^b_!(f,e), \\ \Psi_{b,e'}\big( k:x \to_f^{b^*Q} x\big) & \defeq \tyfill_{Q^b_!(f,x)}^\varphi(k),
\end{align*}

see <Ref> for an illustration. By $Q$-cocartesianness of the lifts of $P$-vertical arrows in $K$ one can show—analogously to the proof of <Ref>—that the maps are quasi-inverse to one another.

$\ref{it:sl-cocart-fam-char-iii} \implies \ref{it:sl-cocart-fam-char-i}$ By assumption, there exists a fibered functor $\tau_\varphi: \relcomma{B}{\varphi}{E} \to_E F$ and a fibered natural transformation

\[ \eta:\big( \id_{\relcomma{B}{\varphi}{E}}\Rightarrow^K_E \iota_\varphi \circ \tau_\varphi \big) \simeq \prod_{\substack{b:B \\e:P\,b}} \prod_{\substack{d:P\,b \\ f:d \to_{P\,b}e \\ x:Q(b,d)}} \angled{d,f,x} \longrightarrow^{\relcomma{B}{K}{E}}_{\pair{b}{e}} \angled{e,\id_e,f_!x},  \]

where we write $f_!x$ for the respective component, for the sake of foreshadowing.

\[ \relcomma{B}{K}{E} \defeq \lambda b,e.\sum_{\substack{d:P\,b \\ f:d \to_{P\,b}e}} Q(b,d):E \to \UU \]

is the straightening of $\partial_1: \relcomma{B}{\varphi}{E} \fibarr E$. Note that there is an equivalence

\[ \Big( \angled{d,f,x} \to_{(\relcomma{B}{K}{E})(b,e)} \angled{e,\id_e,f_!\,x}  \Big) \simeq \Big( x \to^{b^*Q}_{\pair{b}{f}} f_!\,x\Big) ,\]

as illustrated by:

\[\begin{tikzcd}
F & x && {f_!\,x} \\
& d && e \\
E & e && e \\
B && b
\arrow["f"', from=2-2, to=3-2]
\arrow[Rightarrow, no head, from=3-2, to=3-4]
\arrow["f", from=2-2, to=2-4]
\arrow[Rightarrow, no head, from=2-4, to=3-4]
\arrow["{\eta_x}", from=1-2, to=1-4, cocart]
\arrow[Rightarrow, dotted, no head, from=1-2, to=2-2]
\arrow[Rightarrow, dotted, no head, from=1-4, to=2-4]
\arrow[Rightarrow, dotted, no head, from=3-2, to=4-3]
\arrow[Rightarrow, dotted, no head, from=3-4, to=4-3]
\arrow[two heads, from=3-1, to=4-1]
\arrow[two heads, from=1-1, to=3-1]
\end{tikzcd}\]

Furthermore, by the assumption, the induced transposing map[again, identifying $\angled{d,f,x} \longrightarrow_{\pair{v}{g}} \angled{e',\id_{e'}, x'}$ with $x \to^K_{\pair{v}{gf}} x'$] is a family of equivalences:

\begin{align*}
& \Phi : \prod_{\substack{b,b':B \\e:P\,b \\ e':P\,b'}} \prod_{\substack{v:b \to_B b' \\ g:e \to^P_v e'}} \prod_{\substack{d:P\,b \\ f:d \to_{P\,b} e \\ x:Q(b,d)}} \prod_{x':Q(b',e')} \Big( f_!\,x \longrightarrow_{\pair{v}{g}}^K x' \Big) \stackrel{\simeq}{\to} \Big( x \longrightarrow^K_{\pair{v}{gf}} x' \Big), \\
& \Phi\big(m: f_!\,x \to^K_{\pair{v}{g}} x' \big) \defeq \big( m \circ \eta_x: x \to_{Q\,b\,e}  f_!\,x \to^K_{\pair{v}{g}} x' \big)
\end{align*}

Now, $\Phi$ being a fiberwise equivalence means the proposition

\[ \prod_{\substack{b,b':B \\e:P\,b \\ e':P\,b'}} \prod_{\substack{v:b \to_B b' \\ g:e \to^P_v e'}} \prod_{\substack{d:P\,b \\ f:d \to_{P\,b} e \\ x:Q(b,d)}} \prod_{x':Q(b',e')} \prod_{k: x \to^K_{\angled{v,gf}} x'} \isContr \Big( \sum_{m:f_!\,x \to^K_{\pair{v}{g}} x'} m \circ \eta_x = k \Big) \]

is satisfied, cf. <Ref>. This exhibits $\eta_x: x \to^K_{\pair{b}{f}} \tau_\varphi(f,x)$ as $K$-cocartesian lift of the $P$-vertical arrow $f:d \to_{P\,b} e$ (starting at $x:Q(b,d)$), as claimed.

\[\begin{tikzcd}
F && x \\
\\
&& {f_!^{K,b}\,x} && {x'} \\
E && e \\
\\
&& {e'} && {e'} \\
B && b && b
\arrow["k", from=1-3, to=3-5]
\arrow["f"', from=4-3, to=6-3]
\arrow["{\id_{e'}}", Rightarrow, no head, from=6-3, to=6-5]
\arrow["f", from=4-3, to=6-5]
\arrow["\pi"{description}, two heads, from=4-1, to=7-1]
\arrow["\varphi"{description}, two heads, from=1-1, to=4-1]
\arrow["\xi"{description}, curve={height=30pt}, from=1-1, to=7-1]
\arrow["{K^b_!(f,x)}"', from=1-3, to=3-3, cocart]
\arrow["m"', from=3-3, to=3-5]
\arrow["{\id_b}", Rightarrow, no head, from=7-3, to=7-5]
\end{tikzcd}\]

Cocartesian transport for sliced cocartesian families

\[\begin{tikzcd}
&& x \\
F && {f_!\,x} && {x'} \\
&& d \\
E && e && {e'} \\
B && b && {b'}
\arrow["{\eta_x}"', from=1-3, to=2-3, cocart]
\arrow["{\exists!\, m}"', dashed, from=2-3, to=2-5]
\arrow["{\forall\,k}", from=1-3, to=2-5]
\arrow["f"', from=3-3, to=4-3]
\arrow["g"', from=4-3, to=4-5]
\arrow["gf", from=3-3, to=4-5]
\arrow["v", from=5-3, to=5-5]
\arrow[from=4-1, to=5-1, two heads]
\arrow[from=2-1, to=4-1, two heads]
\end{tikzcd}\]

Cocartesian filling in sliced cocartesian families

\[\begin{tikzcd}
x & {x'} & x & {x'} \\
{g'_!\,x} & {f_!\,x'} &&& {g'_!\,x} & {f_!\,x'} \\
e & {e'} & e & {e'} & e & {e'} \\
{e''} & {e'''} & {e''} & {e'''} & {e''} & {e'''} \\
b & {b'} & b & {b'} & b & {b'} \\
{\VertArr_\xi(F)} && {\relcomma{B}{\varphi}{E}} && {} & F
\arrow["v", from=5-3, to=5-4]
\arrow["{f'}"', from=4-3, to=4-4]
\arrow["{g'}"', from=3-3, to=4-3]
\arrow["f", from=3-4, to=4-4]
\arrow["v", from=5-5, to=5-6]
\arrow["{g'}"', from=3-5, to=4-5]
\arrow["{f'}"', from=4-5, to=4-6]
\arrow["g", from=3-5, to=3-6]
\arrow["f", from=3-6, to=4-6]
\arrow["k", from=1-3, to=1-4]
\arrow["{k'}", dashed, from=2-5, to=2-6]
\arrow[Rightarrow, dotted, no head, from=1-3, to=3-3]
\arrow[Rightarrow, dotted, no head, from=1-4, to=3-4]
\arrow["g", from=3-3, to=3-4]
\arrow["{\tau_B}", curve={height=-12pt}, maps to, from=3-4, to=3-5]
\arrow["g", from=3-1, to=3-2]
\arrow["{g'}"', from=3-1, to=4-1]
\arrow["f", from=3-2, to=4-2]
\arrow["{f'}"', from=4-1, to=4-2]
\arrow["v", from=5-1, to=5-2]
\arrow["{\chi_B}"', curve={height=12pt}, maps to, from=3-3, to=3-2]
\arrow["{k'}", dashed, from=2-1, to=2-2]
\arrow["B", two heads, from=6-3, to=6-1]
\arrow["{m'}"', from=1-1, to=2-1, cocart]
\arrow["k", from=1-1, to=1-2]
\arrow["m", from=1-2, to=2-2, cocart]
\arrow[curve={height=-18pt}, Rightarrow, dotted, no head, from=2-6, to=4-6]
\arrow[curve={height=18pt}, Rightarrow, dotted, no head, from=2-5, to=4-5]
\arrow["E"', two heads, from=6-3, to=6-6]
\end{tikzcd}\]

Action on arrows of lifting and transport of sliced cocartesian families

For future reference, we record here the actions on arrows of the induced (fibered) lifting and transport functors as established in the proof of <Ref>. Informally, these can be described as follows. An arrow in $\relcomma{B}{\varphi}{E}$ is given by a dependent square $\sigma$ in $P$ whose vertical edges $f \defeq \lambda t.\sigma(1,t)$, $g' \defeq \lambda t.\sigma(0,t)$ are $P$-vertical, and, moreover, an arrow $k$ in $Q$ over the edge $\pair{t}{0}$. The lifting functor $\chi_B$ maps this to the ensuing dependent square in $Q$ produced by adding the $Q$-cocartesian lifts of the $P$-vertical arrows and the induced filling edge. The functor $\tau_B$ yields only the filling edge of this square.

Formally, this reads as[suppressing the repeated data in the lower layers]

\begin{align}
\chi_{B,v}(\angled{g,f,g',f'}, k:x \to_g x') & \defeq \angled{k,m:x' \cartarr_{f}^Q f_!\,x', m': x \cartarr_{f}^Q g'_!\,x, k': g_!'x \to_{f'}^Q f_!\,x},\label{eq:lift-sl-cocart}\\
\tau_{B,f'}(\angled{g,f,g',f'}, k:x \to_g x') & \defeq (k':g_!\,x \to_{f'}^Q f_!\,x'). \label{eq:trans-sl-cocart}
\end{align}

The following proposition reflects the known fact that, given a cocartesian functor between cocartesian fibrations, it is a sliced cocartesian fibration if and only if it is a cocartesian fibration in the usual sense.

Let $B$ be a Rezk type. Assume $\xi:F \fibarr B$ and $\pi:E \fibarr B$ are cocartesian fibrations, and $\varphi:F \to_B E$ is a cocartesian functor:

\[\begin{tikzcd}
F && E \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["\pi", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

Then $\varphi:F \to_B E$ is a cocartesian fibration sliced over $B$ if and only if it is a cocartesian fibration $F \fibarr E$ in the usual sense.

In case $\varphi: F \to E$ is a cocartesian fibration it is also a cocartesian fibration sliced over $B$ since it automatically satisfies the weaker existence condition for lifts.

For the converse, we fibrantly replace the given diagram, considering the straightenings $P \defeq \St_B(\pi): B \to \UU$, $Q \defeq \St_B(\pi): B \to \UU$, $K \defeq  \St_E(\varphi): E \to \UU$.

We assume $K$ to be a cocartesian family sliced over $B$, and want to show that it is also a cocartesian family in the usual sense. For an illustration of what follows,  <Ref>. Consider an arrow $\pair{u:b \to_B b'}{f:e \to_u^\pi e'}$ in $E$ together with a point $x:K(b,e)\jdeq Q(b,e)$. First, consider the $P$-cocartesian lift of $u:b\to_B b'$  $e:P\,b$, given by $g \defeq P_!(u,e) : e \cocartarr^P_{u} u^P_!\,x$. This induces a filler $h \defeq \tyfill^P_g(f): u^P_!\,x \to_{P\,b'} e'$ that is in particular vertical. Since $K:E \to \UU$ is a sliced cocartesian family we have a lift  to the $Q$-cocartesian transport of the point $x:Q(b,e)$, namely an arrow $m \defeq K_!(h,u_!^Q\,x): u_!^Q\,x \to^K_{\pair{u}{f}} x'$ to some point $x':Q(b,e')$. But by assumption, $m$ (together with its $\varphi$-image $h$) is also a $Q$-cocartesian arrow, hence so is the composite $k \defeq m \circ Q_!(u,x) : x \longrightarrow^K_{g \circ \varphi(Q_!(u,x))} x'$.
The functor $\varphi$ being cocartesian means $\varphi(Q_!(u,x))$ is identified with $P_!(u,e) \jdeq g$, so up to homotopy, the dependent arrow $k:x \to^Q_u x'$ lies over the composite $h \circ g = f$—hence we can assume it does so strictly. Now, $k$ (together with its projection $f$) being a $Q$-cocartesian arrow means it is in particular $K$-cocartesian (cf. <Ref> for illustration).

\[\begin{tikzcd}
F & x && {x'} \\
&&& {u_!^Q\,x} \\
E & e && {e'} \\
&&& {u^P_!\,e} \\
B & b && {b'}
\arrow["k", from=1-2, to=1-4]
\arrow["m"', from=2-4, to=1-4]
\arrow["f", from=3-2, to=3-4]
\arrow["{g \jdeq P_!(u,e)}"', from=3-2, to=4-4, cocart]
\arrow["h"', dashed, from=4-4, to=3-4]
\arrow["u", from=5-2, to=5-4]
\arrow["\varphi"{description}, from=1-1, to=3-1]
\arrow["\pi"{description}, two heads, from=3-1, to=5-1]
\arrow["{\ell \jdeq Q_!(u,x)}"', from=1-2, to=2-4, cocart]
\arrow["\xi"{description}, curve={height=24pt}, two heads, from=1-1, to=5-1]
\end{tikzcd}\]

Absolute from sliced cocartesian fibrations

Consider a cospan $\psi:F \to_B G \leftarrow_B E: \varphi$ of fibered functors between isoinner fibrations over a Rezk type $B$, giving rise to the sliced comma type:

\[\begin{tikzcd}
{\varphi \downarrow_B \psi} &&&& E \\
\\
F &&&& G & {} \\
\\
&& B
\arrow[from=1-1, to=3-1]
\arrow[two heads, from=3-1, to=5-3]
\arrow[two heads, from=3-5, to=5-3]
\arrow[from=1-1, to=1-5]
\arrow["\varphi", from=1-5, to=3-5]
\arrow[two heads, from=1-1, to=5-3]
\arrow[two heads, from=1-5, to=5-3]
\arrow[shorten <=35pt, shorten >=35pt, Rightarrow, from=1-5, to=3-1]
\arrow["\psi"', from=3-1, to=3-5, crossing over]
\end{tikzcd}\]

The codomain projection

\[ \partial_1: \relcomma{B}{\varphi}{\psi} \fibarr F \]

is a cocartesian fibration.

Consider the families $R:B \to \UU$, $P:G \to \UU$, and $Q:G \to \UU$ associated to $G \fibarr B$, $\varphi: E \fibarr G$, and $\psi: F \fibarr G$, resp. By projection equivalence we have

\[ \partial_1: \relcomma{B}{\varphi}{\psi} \simeq \sum_{b:B} \sum_{\stackrel{x,x':R\,b}{k:x \to^R_u x'}} P\,b\,x \times Q\, b\,x' \fibarr F \simeq \sum_{b:B} \sum_{x':R\,b} Q\,b\,x'. \]

For an arrow in $F$, given by data $u:b \to_B b'$, $m:x' \to^R_u x''$, $f:d \to^Q_m d'$, we posit the cocartesian lift w.r.t. the starting vertex $\angled{b,k:x \to_{P\,b} x', d,e}$ to be the “tautological extension”

\[ \angled{\pair{\id_x}{m}: k \rightrightarrows^R_{u} mk, \id_e: e =_{P\,x} e,f:d \to^Q_m d'} \]

as illustrated:

\[\begin{tikzcd}
{\varphi \downarrow_B \psi} && e && e \\
&& d && {d'} &&&& d && {d'} \\
&& x && x & {} && {} \\
&& {x'} && {x''} &&&& {x'} && {x''} \\
B && b && {b'} &&& F & b && {b'}
\arrow[Rightarrow, no head, from=1-3, to=1-5]
\arrow["f", from=2-3, to=2-5]
\arrow["k"', from=3-3, to=4-3]
\arrow["m", from=4-3, to=4-5]
\arrow[Rightarrow, no head, from=3-3, to=3-5]
\arrow["mk", from=3-5, to=4-5, swap]
\arrow["u", from=5-3, to=5-5]
\arrow[two heads, from=1-1, to=5-1]
\arrow["{\partial_1}", two heads, from=3-6, to=3-8]
\arrow["u", from=5-9, to=5-11]
\arrow["m", from=4-9, to=4-11]
\arrow["f", from=2-9, to=2-11]
\arrow[curve={height=18pt}, Rightarrow, dotted, no head, from=2-3, to=4-3]
\arrow[curve={height=-18pt}, Rightarrow, dotted, no head, from=2-5, to=4-5]
\arrow[curve={height=18pt}, Rightarrow, dashed, no head, from=1-3, to=3-3]
\arrow[curve={height=-18pt}, Rightarrow, dashed, no head, from=1-5, to=3-5]
\arrow[Rightarrow, dotted, no head, from=2-9, to=4-9]
\arrow[Rightarrow, dotted, no head, from=2-11, to=4-11]
\end{tikzcd}\]

In the picture the right hand side indicates the action of the projection $\partial_1 : \relcomma{B}{\varphi}{\psi} \fibarr F$
That this arrow in the sliced comma $\relcomma{B}{\varphi}{\psi}$ is in fact cocartesian is seen as follows. A postcomposing arrow in $F$ consists of data $v:b' \to b''$, $\ell: x'' \to_v^R x'''$, $g:d' \to^Q_\ell d''$. A dependent arrow in $\relcomma{B}{\varphi}{\psi}$ over the composite arrow in $F$ is given by

\[ \angled{\pair{\ell'}{\ell m}: k \rightrightarrows^R_{vu} k', r:e \to^P_{\ell'} e', g \circ f: d \to^Q_{\ell \circ m} d''}\]

where $\ell':x \to_v^R y$, $k':y \to_{R\,b''} x'''$:

\[\begin{tikzcd}
{\varphi \downarrow_B \psi} && e && e && {e'} \\
&& d && {d'} && {d''} \\
&& x && x && y & {} \\
&& {x'} && {x''} && {x'''} \\
B && b && {b'} && {b''}
\arrow[Rightarrow, no head, from=1-3, to=1-5]
\arrow["f", from=2-3, to=2-5]
\arrow["k"', from=3-3, to=4-3]
\arrow["m", from=4-3, to=4-5]
\arrow[Rightarrow, no head, from=3-3, to=3-5]
\arrow["mk", from=3-5, to=4-5]
\arrow["u", from=5-3, to=5-5]
\arrow[two heads, from=1-1, to=5-1]
\arrow["{\ell'}", from=3-5, to=3-7]
\arrow["\ell", from=4-5, to=4-7]
\arrow["r", from=1-5, to=1-7]
\arrow["g", from=2-5, to=2-7]
\arrow["{k'}", from=3-7, to=4-7]
\arrow["v", from=5-5, to=5-7]
\end{tikzcd}\]

The filler is constructed just by repeating the missing data $\ell':x \to y$, $r:e \to e'$ which also shows uniqueness up to contractibility  the given data.

For a cospan of maps between Rezk types $g: C \to A \leftarrow B:f$, the codomain projection $\partial_1: \comma{f}{g} \fibarr C$ is a cocartesian fibration.

§.§ Cocartesian families in cartesian families

We now introduce the concept of cocartesian fibrations in cartesian fibrations, which semantically, really translate to cocartesian fibrations in $\infty$-cosmoses of cartesian fibrations.

Their characterization will be of relevance for the characterization of two-sided cartesian fibrations in <Ref>.

Let $\varphi: \xi \to_B \pi$ be a cartesian functor between cartesian fibrations. In addition, let $\varphi$ be a cocartesian fibration sliced over $B$:

\[\begin{tikzcd}
F && E \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["\pi", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

Then we call $\varphi$ a cocartesian fibration in cartesian fibrations.[For the official naming we prefer the fibrational variant since it is closer to its semantic counterpart, but of course by the typal Grothendieck construction there exists an indexed variant as well.]

Let $\varphi:\xi \to_B \pi$ be a cocartesian fibration in cartesian fibrations, as in <Ref>. Then the following are equivalent:

The sliced cocartesian lifting map,    the fibered LARI

\[\begin{tikzcd}
{\mathrm{Vert}_\xi(F)} && {\varphi \downarrow_B E } \\
& B
\arrow["{\overline{\xi}}"', two heads, from=1-1, to=2-2]
\arrow["{\overline{\varphi}}", two heads, from=1-3, to=2-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\chi_B}"', curve={height=12pt}, dotted, from=1-3, to=1-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{i_0 \cotens \pi}"', curve={height=6pt}, from=1-1, to=1-3]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=0, to=1]
\end{tikzcd}\]

is a cartesian functor between cartesian fibrations over $B$

The sliced cocartesian transport map, , the fibered left adjoint

\[\begin{tikzcd}
F && {\varphi \downarrow_B E} \\
& E \\
& B
\arrow["\varphi"{description}, from=1-1, to=2-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\iota_B}"{description}, curve={height=6pt}, from=1-1, to=1-3]
\arrow["{\partial_1}"{description}, from=1-3, to=2-2]
\arrow["\xi"{description}, two heads, from=1-1, to=3-2]
\arrow["{\overline{\varphi}}"{description}, two heads, from=1-3, to=3-2]
\arrow["\pi"{description}, two heads, from=2-2, to=3-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\tau_B}"{description}, curve={height=12pt}, dashed, from=1-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-93}, draw=none, from=1, to=0]
\end{tikzcd}\]

is a cartesian functor (from $\overline{\varphi}$ to $\xi$).

*  For all elements $b,b':B$, arrows $v:b' \to_B v$, vertical arrows $f:e' \to_{P\,b}e$ and $x:Q(b,e')$, let us make the following abbreviations:[Note that all the cocartesian lifts exist because they are over $P$-vertical arrows.]

\begin{align}\label{eq:abbrv-cocart-in-cart-gen}
g 	& \defeq P^*(v,e'): v^*(b'e') \cartarr^P_{v} e', & f' & \defeq P^*(v,e'): v^*(b,e) \cartarr^P_{v} e, \\
g ' & \defeq \cartFill_{f'}^P(fg), & k & \defeq Q^*(g,x): x \cartarr^Q_g g^*x, \\
k' & \defeq \cocartFill^Q_{m'}(mk): g'_!g^*x \to^Q_{f'} f_!\,x, & k'' & \defeq Q^*(f',f_!\,x): (f')^*f_!\,x \cartarr^Q_{f'} f_!x, \\
m 	& \defeq Q_!(f,x): x \cocartarr^Q_f f_!\,x. & m' & \defeq Q_!(g',g^*x): g^*x \cocartarr^Q_{g'} g_!'g^*x, \\
m'' & \defeq \cartFill^Q_{k''}(mk): g^*x \to (f')^*f_!\,x. &&
\end{align}

Then there is a homotopy $r$ such that:

\[\begin{tikzcd}
{(f')^*f_!\,x} && {f_!\,x} \\
& {g'_!g^*\,x}
\arrow["{k'}", from=1-1, to=1-3]
\arrow["r"', Rightarrow, no head, from=1-1, to=2-2]
\arrow["{k''}"', from=2-2, to=1-3, cart]
\end{tikzcd}\]

*  With the notation from <Ref> there is a homotopy $r$ such that:

\[\begin{tikzcd}
{g^*x\,} && {g_!'g^*\,x} \\
& {(f')^*f_!\,x}
\arrow["{m''}", from=1-1, to=1-3, cocart]
\arrow["{m'}"', from=1-1, to=2-2]
\arrow["r"', Rightarrow, no head, from=2-2, to=1-3]
\end{tikzcd}\]

We prove the equivalence of these four conditions by first explicating <Ref>. We will readily see that it is equivalent to either of the three remaining condition.

Recall the action of the fibered lifting $\chi_B$ and transport functor $\tau_B$, resp, <Ref>. In the first case, assume we have an identity

\begin{align}\label{eq:cart-sl-transp}
\chi_B(\overline{\varphi}^*(v,\pair{f}{x})) = \overline{\xi}^*(v,\chi_B(f,x))
\end{align}

for all $v:b'\to_B b$, $f:e' \to_{P\,b} e$, $x:Q(b,e')$. Consider the abbreviations from (<ref>).
Specifically, the case for $\chi_B$ will involve

\begin{align}\label{eq:abbrv-cocart-in-cart-chi}
m' & \jdeq Q_!(g',g^*x): g^*x \cocartarr^Q_{g'} g_!'g^*x, & & k' \jdeq \cocartFill^Q_{m'}(mk): g'_!g^*x \to^Q_{f'} f_!\,x,
\end{align}

whereas for $\tau_B$ we will need:

\begin{align}\label{eq:abbrv-cocart-in-tau}
k'' & \jdeq Q^*(f',f_!\,x): (f')^*f_!\,x \cartarr^Q_{f'} f_!x, & & m'' \jdeq \cartFill^Q_{k''}(mk): g^*x \to (f')^*f_!\,x.
\end{align}

As detailed in <cit.>, lifts of co-/cartesian families are fiberwise. Hence, we find for the left hand side in (<ref>):

\begin{align}
& \chi_B(\overline{\varphi}^*(v,\pair{f}{x})) = \chi_B(v,\angled{g,f,g',f'},k:g^*x \cartarr_{g}^Q x) \\
= & \angled{v,\angled{g,f,g',f'},\angled{k,m,m',k'}} \label{eq:abbrv-cocart-in-cart-lhs}
\end{align}

and for the right hand side:

\begin{align}
& \overline{\xi}^*(v,\chi_B(f,x)) = \overline{\xi}^*(v,\angled{g,f,g',f'},\angled{k,m,m'',k''}) \\
=	& \angled{v,\angled{g,f,g',f'},\angled{k,m,m'',k''}}. \label{eq:abbrv-cocart-in-cart-rhs}
\end{align}

Recall that a functor being cartesian is a proposition.
A path between (<ref>) and (<ref>) amounts to an isomorphism $r:(f')^*f_!\,x =_{v^*(b,e)} g'_!g^*x$ such that the entire following diagram commutes:

\[\begin{tikzcd}
{g^*\,x} && x \\
{(f')^*f_!\,x} && {f_!\,x} \\
& {g_!'g^*x}
\arrow["{m'}"', from=1-1, to=2-1, cocart]
\arrow["k"{pos=0.6}, from=1-1, to=1-3]
\arrow["m", from=1-3, to=2-3, cocart]
\arrow["r"', Rightarrow, no head, from=2-1, to=3-2]
\arrow["{k''}"', from=3-2, to=2-3, cart]
\arrow["{k'}"'{pos=0.6}, from=2-1, to=2-3]
\arrow["{m''}"{pos=0.3}, from=1-1, to=3-2, crossing over]
\end{tikzcd}\]

More generally, it can be shown that there exists a filler $r:(f')^*f_!\,x \to_{v^*(b,e)} g_!'g^*x$ s.t. $m'' = rm'$ and $k' = k''r$. Hence, this propositional condition is equivalent to this induced arrow being invertible. But moreover, we can see by universality that this is equivalent to the existence of either identification $m'=m''$ or $k'=k''$. In particular, the action by the transport functor $\tau_B$ yields just the latter. Hence, all the four conditions claimed are equivalent.

For a small indexing type $I:\UU$, let $B:I \to \UU$ be a family of Rezk types. Let $P:\prod_{i:I}(B_i \to \UU)$ be a family and $K: \prod_{i:I} (\totalty{P}_i \to \UU)$ be another family. We define $Q\defeq \lambda i.\Sigma_{\totalty{P_i}}K_i.\prod_{i:I} (B_i \to \UU)$. For every $i:I$, we denote

\begin{align*}
& \pi_i \defeq \Un_{B_i}(P_i) : E_i \defeq \totalty{P_i} \fibarr B_i,& \quad \xi_i \defeq \Un_{B_i}(Q_i) : F_i \defeq \totalty{Q_i} \fibarr B_i,  \\
& \varphi \defeq \Un_{E_i}(K_i): F_i \to E_i &
\end{align*}

giving rise to diagrams:

\[\begin{tikzcd}
{F_i} && {E_i} \\
& {B_i} & {} && {}
\arrow["{\xi_i}"', two heads, from=1-1, to=2-2]
\arrow["{\pi_i}", two heads, from=1-3, to=2-2]
\arrow["{\varphi_i}", from=1-1, to=1-3]
\end{tikzcd}\]

If each $\varphi_i$ is a sliced cocartesian fibration, then so is the product:

\[\begin{tikzcd}
{\prod_{i:I} F_i} && {\prod_{i:I} E_i} \\
& {\prod_{i:I} B_i} & {} && {}
\arrow["{\prod_{i:I} \xi_i}"', two heads, from=1-1, to=2-2]
\arrow["{\prod_{i:I} \pi_i}", two heads, from=1-3, to=2-2]
\arrow["{\prod_{i:I} \varphi_i}", from=1-1, to=1-3]
\end{tikzcd}\]

Moreover, if $\varphi_i$ is a cocartesian fibration in cartesian fibrations in the sense of <ref>, then so is $\prod_{i:I} \varphi_i$.

Since dependent products commute with sliced commas by <Ref> we find

\begin{align}
\prod_{i:I} \VertArr_{\xi_i}(F_i) & \equiv \prod_{i:I} \relcomma{B_i}{F_i}{F_i} \equiv   \relcomma{\prod_{i:I} B_i}{\big(\prod_{i:I}F_i\big)}{\big(\prod_{i:I}F_i\big)} \\
\prod_{i:I} \relcomma{B_i}{\varphi_i}{E_i} & \equiv \relcomma{\prod_{i:I} B_i}{\big(\prod_{i:I} \varphi_i\big)}{\big(\prod_{i:I} E_i\big)}.
\end{align}

Since sliced LARIs are preserved by the dependent product <Ref> we obtain an induced fibered LARI between these commas, establishing that $\prod_{i:I} \varphi$ is sliced cocartesian by <Ref>.

Moreover, since cartesian fibrations and co-/cartesian functors are preserved under the dependent product the analogous closure statement for the stronger notion of cocartesian fibration in cartesian fibrations follows readily.

For a Rezk type $B$, consider cocartesian families $P:B \to \UU$, $Q:\totalty{P} \to \UU$, and a fiberwise map $\varphi : \prod_{b:B} P\,b \to Q\,b$. We write the unstraightenings as $\pi: E \defeq \totalty{P} \fibarr B$, $\xi: F \defeq \totalty{Q} \fibarr B$. Consider the following diagram, induced by a section $\ell$ of (the totalization of) $\varphi$ over $B$, and $A$ and a map $k:A \to B$ between Rezk types:

\[\begin{tikzcd}
{F'} &&& F \\
& {E'} &&& E \\
A &&& B
\arrow["\varphi"{description}, from=1-4, to=2-5]
\arrow[from=1-1, to=1-4]
\arrow["{\varphi'}"{description}, from=1-1, to=2-2]
\arrow["\xi"{description, pos=0.3}, two heads, from=1-4, to=3-4]
\arrow["\pi"{description}, two heads, from=2-5, to=3-4]
\arrow["{\xi'}"{description, pos=0.3}, two heads, from=1-1, to=3-1]
\arrow["{\pi'}"{description}, two heads, from=2-2, to=3-1]
\arrow["k", from=3-1, to=3-4]
\arrow["\ell"{description}, curve={height=12pt}, dotted, from=2-5, to=1-4]
\arrow[from=2-2, to=2-5, crossing over]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-4]
\arrow["\lrcorner"{anchor=center, pos=0.125}, shift right=5, draw=none, from=1-1, to=3-4]
\arrow["{\ell'}"{description, pos=0.3}, curve={height=18pt}, dotted, from=2-2, to=1-1, crossing over]
\end{tikzcd}\]

If $\ell$ is a cocartesian functor, then the induced section $\ell'$ is, too.

First, projection equivalence yields:

\[E \defeq \sum_{b:B} P\,b, \quad F \defeq \sum_{\substack{b:B \\ e:P\,b}} Q\,b\,e,
E' \defeq \sum_{a:A} P\,ka, \quad F' \defeq \sum_{\substack{a:B \\ d:P\,ka}} Q\,ka\,d.  \]

The section $\ell$ is then taken to be

\[ \ell(b,e) \defeq \angled{b,e,\widehat{\ell}(b,e)}\]

for $b:B$, $e:P\,b$.
Cocartesianness means that there is a path

\begin{align*}
\ell(u,P_!(u,e)) & \jdeq \angled{u,P_!(u,e),\widehat{\ell}(u,P_!(u,e))} \\
& \jdeq \angled{u,P_!(u,e),Q_!(u, \pair{u^P_!e}{\widehat{\ell}(b,e)})}
\end{align*}

for $u:b\to_B b'$, $e:P\,b$.
The induced section $\ell'$ arises as $\ell'(a,d) \jdeq \ell(ka,d) \jdeq \angled{ka,d \widehat{\ell}(ka,d)}$ for $a:A$, $d:P'\,a \simeq P\,ka$. Applying this to the $P'$-cocartesian lift of $v:a \to a'$  $d:Q\,a$ yields

\begin{align*}
\ell'(v,P'_!(v,d)) & \jdeq \ell(kv,P'_!(kv,d)) = \ell(kv,P_!(v,d)) \defeq \angled{kv,P_!(v,d),\widehat{\ell}(kv,P_!(v,d))} \\
& = \angled{kv,P_!(kv,d),Q_!(kv, \pair{(kv)^P_!(d)}{\widehat{\ell}(kv,P_!(kv,d))})} \\
& = \angled{kv,P'_!(v,d),Q'_!(v, \pair{v^{P'}_!(d)}{\widehat{\ell'}(v,P'_!(v,d))})} \\
\end{align*}

confirming the claim.

Let $P,Q,R:B \to \UU$ be isoinner families over a Rezk type $B$ with unstraightenings

\[ \xi \defeq \Un_B(Q) : F \fibarr B, \pi \defeq \Un_B(P) : E \fibarr B, \rho \defeq \Un_B(R) : G \fibarr B. \]

Furthermore, assume we have fibered functors $\varphi:F \to_B E$, $\psi: E \to_B G$ that are sliced cocartesian over $B$. Then, so is their composite $\kappa:F \to_B G$:

\[\begin{tikzcd}
F && E && G \\
\\
&& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\pi"{description}, two heads, from=1-3, to=3-3]
\arrow["\psi", from=1-3, to=1-5]
\arrow["\xi"{description}, two heads, from=1-1, to=3-3]
\arrow["\rho"{description}, two heads, from=1-5, to=3-3]
\arrow["\kappa"{description}, curve={height=-24pt}, from=1-1, to=1-5]
\end{tikzcd}\]

Moreover, if $\varphi$ and $\psi$ are cocartesian fibrations in cartesian fibrations, then so is $\psi \circ \varphi$.

This proof works analogously to the one for the absolute situation in <cit.>. First of all, we fibrantly replace the objects at play (with some abbreviation for the term declarations):

\begin{align*}
G & \equiv \sum_{b:B} Q\,b, & E & \equiv \sum_{\substack{b:B \\ x:R\,b}} P\,b\,x, \\
F & \equiv \sum_{\substack{b:B \\ x:R\,b \\ e:P\,b\,x}} Q\,b\,\,x\,e, & \relcomma{B}{\psi}{G} & \equiv \sum_{b,x,e} \sum_{x':R\,b} (x \to_{R\,b} x'), \\
\relcomma{B}{\varphi \psi}{G} & \equiv \sum_{b,x,x',e} \sum_{d:Q\,b\,x\,e} (x \to_{R\,b} x'), & \relcomma{B}{\varphi}{E} & \equiv \sum_{b,x,x',e,d} \sum_{u:x \to_{R\,b} x'} (e \to_u^P e'), \\
\VertArr_\pi(E) & \equiv \sum_{b,x,x',u,e,e'} (e \to_u^P e'). & 	& &
\end{align*}

We are to construct from the given fibered LARI adjunctions

\[\begin{tikzcd}
{\VertArr(F)} && {\relcomma{B}{\varphi}{E}} && {\VertArr(E)} && {\relcomma{B}{\psi}{G}} \\
& B &&&& B
\arrow[""{name=0, anchor=center, inner sep=0}, "r"{description}, curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{r'}"{description}, curve={height=12pt}, from=1-5, to=1-7]
\arrow[""{name=2, anchor=center, inner sep=0}, "\ell"{description}, curve={height=18pt}, dotted, from=1-3, to=1-1]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\ell'}"{description}, curve={height=18pt}, dotted, from=1-7, to=1-5]
\arrow[two heads, from=1-1, to=2-2]
\arrow[two heads, from=1-3, to=2-2]
\arrow[two heads, from=1-5, to=2-6]
\arrow[two heads, from=1-7, to=2-6]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=2, to=0]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=3, to=1]
\end{tikzcd}\]

a fibered LARI adjunction:

\[\begin{tikzcd}
{\VertArr(E)} && {\relcomma{B}{\varphi \psi}{G}} \\
& B
\arrow[""{name=0, anchor=center, inner sep=0}, "{r''}"{description}, curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\ell''}"{description}, curve={height=18pt}, dotted, from=1-3, to=1-1]
\arrow[two heads, from=1-1, to=2-2]
\arrow[two heads, from=1-3, to=2-2]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

Using the projection equivalences, indeed we find the diagram analogous to the proof in <cit.>, all fibered over $B$:

\[\begin{tikzcd}
{\VertArr_\xi(F)} \\
&& {\relcomma{B}{\varphi}{E}} && {\relcomma{B}{\varphi \psi}{G}} && F \\
&& {\VertArr_\pi(E)} && {\relcomma{B}{\psi}{G}} && E \\
&&&& B
\arrow[from=2-7, to=3-7]
\arrow[from=3-5, to=3-7]
\arrow[from=2-5, to=3-5]
\arrow[from=2-5, to=2-7]
\arrow[""{name=0, anchor=center, inner sep=0}, curve={height=6pt}, from=2-3, to=2-5]
\arrow[from=2-3, to=3-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "r"', curve={height=6pt}, from=3-3, to=3-5]
\arrow[from=3-3, to=4-5]
\arrow[from=3-5, to=4-5]
\arrow[from=3-7, to=4-5]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-5, to=3-7]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-5]
\arrow[curve={height=-18pt}, from=1-1, to=2-7]
\arrow[curve={height=12pt}, from=1-1, to=3-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "\ell"{description}, curve={height=12pt}, dotted, from=3-5, to=3-3]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=12pt}, dotted, from=2-5, to=2-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "{r'}"{description}, curve={height=6pt}, from=1-1, to=2-3]
\arrow[""{name=5, anchor=center, inner sep=0}, "{\ell'}"{description}, curve={height=12pt}, dotted, from=2-3, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=2, to=1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=3, to=0]
\arrow["\dashv"{anchor=center, rotate=-144}, draw=none, from=5, to=4]
\end{tikzcd}\]

As before, the proclaimed fibered LARI arises by pulling back and then composing.

The closure property descends to cocartesian fibrations in cartesian fibrations by closedness under composition of cartesian functors, and pullback stability of fibered cartesian sections by the dual of <Ref>.

Let $\varphi:F \to_B E$ be a sliced cocartesian fibration over a Rezk type $B$. For any map $k:A \to B$ consider the pullback:

\[\begin{tikzcd}
{k^*F} && F \\
& {k^*E} && E \\
A && B
\arrow["\xi"{description, pos=0.25}, two heads, from=1-3, to=3-3]
\arrow["\varphi", curve={height=-6pt}, from=1-3, to=2-4]
\arrow["\pi"{description}, two heads, from=2-4, to=3-3]
\arrow[from=1-1, to=1-3]
\arrow["{k^*\varphi}"{pos=0.8}, curve={height=-6pt}, dashed, from=1-1, to=2-2]
\arrow["{k^*\xi}"{description, pos=0.3}, two heads, from=1-1, to=3-1]
\arrow["{k^*\pi}"{description}, two heads, from=2-2, to=3-1]
\arrow["k"', from=3-1, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, shift right=2, draw=none, from=1-1, to=3-3]
\arrow[crossing over, from=2-2, to=2-4]
\end{tikzcd}\]

Then the induced fibered functor $k^*\varphi: k^*F \to_A k^*E$ is a sliced cocartesian fibration over $A$.

In particular, the analogous statement is true if $\varphi$ is assumed to be a cocartesian fibration in cartesian fibrations.

Since pullback commutes with sliced commas[as can  be checked by projection equivalence] we get the following square:

\[\begin{tikzcd}
{k^*\VertArr_{k^*\xi}(F)} && {\VertArr_\xi(F)} \\
& {\relcomma{A}{k^*\varphi}{k^*E}} && {\relcomma{B}{\varphi}{E}} \\
A && B
\arrow[two heads, from=1-3, to=3-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\varphi'}", curve={height=-6pt}, from=1-3, to=2-4]
\arrow[two heads, from=2-4, to=3-3]
\arrow[from=1-1, to=1-3]
\arrow["{k^*\varphi'}"{pos=0.8}, curve={height=-6pt}, dashed, from=1-1, to=2-2]
\arrow[two heads, from=1-1, to=3-1]
\arrow[two heads, from=2-2, to=3-1]
\arrow["k"', from=3-1, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, shift right=2, draw=none, from=1-1, to=3-3]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=-6pt}, dotted, from=2-4, to=1-3]
\arrow["\dashv"{anchor=center, rotate=12}, draw=none, from=1, to=0]
\arrow[from=2-2, to=2-4, crossing over]
\end{tikzcd}\]

The fibered LARI on the right gets pulled back to define a fibered LARI on the left, as desired, hence the pulled back functor $k^*\varphi$ is sliced cocartesian as well.

If $\varphi:F \to_B E$ is a cartesian functor between cartesian functors, then $\varphi'$ pulls back to define a cartesian functor between cartesian fibrations by (the dual of) <cit.>,  also <cit.>. In case the fibered LARI is cartesian, the induced fibered LARI is as well, as one can see by the dual of <Ref>.

§ TWO-SIDED CARTESIAN FAMILIES

Two-sided cartesian families can be presented by spans

\[\begin{tikzcd}
& E \\
A && B
\arrow["\xi"', two heads, from=1-2, to=2-1]
\arrow["\pi", two heads, from=1-2, to=2-3]
\end{tikzcd}\]

where $\xi$ is a cocartesian fibration and $\pi$ is a cartesian fibration, satisfying some compatibility conditions between the lifts of opposite variance.

We will develop this notion in a systematic manner, closely following Riehl–Verity's treatment in $\infty$-cosmoses <cit.>.

Semantically, they correspond to $\inftyone$-functors $A^{\Op} \times B \to \Cat_\infty$, and their discrete variant models $\inftyone$-functors $\inftyone$-functors $A^{\Op} \times B \to \mathrm{Space}$ factoring through the $\inftyone$-category of spaces  $\inftyone$-distributors or $\inftyone$-profunctors (sometimes also called correspondence or bifibration, though the latter terminology can also be used to mean a fibration that is simultaneously cartesian and cocartesian).

(Discrete) two-sided cartesian fibrations have a long history of study in various contexts <cit.>.

In the higher categorical context they are used in the theory of fibrations of $(\infty,1)$-categories <cit.>, the formal category theory of $\infty$-categories <cit.>, and higher algebra and geometry <cit.>.

§.§ Two-variable families and bifibers

For types $A,B: \UU$ consider a family

\[ P:A \to B \to \UU.\]

For $a:A$ and $b:B$, the type $P(a,b)$ is called the bifiber of $P$ at $a$ and $b$. Fixing one of the elements gives rise to the definitions

\[ P_b \defeq \lambda a.P(a,b): A \to \UU, \quad P^a \defeq \lambda b.P(a,b): B \to \UU.\]

The two “legs” of the family $P$ are given by the families

\[ P_B \defeq \lambda a.\sum_{b:B} P_b(a):A \to \UU, \quad  P^A \defeq \lambda b.\sum_{a:B} P^a(b): B \to \UU.\]

We obtain the following version of the typal Grothendieck construction. By transposition we have a chain of fiberwise equivalences:

\[{\small \begin{tikzcd}
{\sum_{A,B:\UU} A \to B \to \UU} && {\sum_{A,B:\UU} (A \times B) \to \UU} && {\sum_{A,B:\UU} \Fib_\UU(A \times B)} \\
&& {\UU \times \UU}
\arrow[from=1-1, to=2-3]
\arrow[from=1-3, to=2-3]
\arrow["\simeq", from=1-3, to=1-5]
\arrow[from=1-5, to=2-3]
\arrow["\simeq", from=1-1, to=1-3]
\end{tikzcd}}\]

Hence two-sided families $P:A \to B \to \UU$ correspond to maps over $\pair{\xi}{\pi}:\widetilde{P} \to A \times B$.

Diagrammatically, this manifests as follows:

\[\begin{tikzcd}
& {\sum_{\substack{a:A \\ b:B}} P\,a\,b } \\
& {A \times B} \\
A && B
\arrow["\varphi"', two heads, from=1-2, to=2-2]
\arrow[two heads, from=2-2, to=3-1]
\arrow[two heads, from=2-2, to=3-3]
\arrow["{\xi \defeq \Un_A(P_B)}"{description}, curve={height=18pt}, two heads, from=1-2, to=3-1]
\arrow["{ \Un_B(P^A) \defeq \pi}"{description}, curve={height=-18pt}, two heads, from=1-2, to=3-3]
\end{tikzcd}\]

The fibers at $a:A$ or $b:B$, resp., are obtained as follows

\[\begin{tikzcd}
{E_b} && E && {E^a} && E \\
A && {A \times B} && B && {A \times B}
\arrow["{\xi_b}"', from=1-1, to=2-1]
\arrow["{\langle \id_A,b\rangle}"', from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\langle\xi, \pi\rangle}", from=1-3, to=2-3]
\arrow["{\pi^a}"', from=1-5, to=2-5]
\arrow["{\langle a,\id_B\rangle}"', from=2-5, to=2-7]
\arrow[from=1-5, to=1-7]
\arrow["{\langle\xi, \pi\rangle}", from=1-7, to=2-7]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-5, to=2-7]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

where the projections arise as unstraightenings

\[ \xi_b \defeq \Un_A(P_b): E_b \to A, \quad \pi^a \defeq \Un_B(P^a): E^a \to B. \]

The notation comes from the convention of denoting the components of the projection $E \to A \times B$ conceived as a fibered functor in two different ways

\[\begin{tikzcd}
E && {A \times B} && E && {A \times B} \\
& B &&&& A
\arrow["{\langle \xi,\pi\rangle}", from=1-1, to=1-3]
\arrow["\pi"', from=1-1, to=2-2]
\arrow["q", from=1-3, to=2-2]
\arrow["{\langle \xi,\pi\rangle}", from=1-5, to=1-7]
\arrow["\xi"', from=1-5, to=2-6]
\arrow["p", from=1-7, to=2-6]
\end{tikzcd}\]

\[ \xi_b \defeq \pair{\xi}{\pi}_b :E_b \to (A\times B)_b \simeq A, \quad  \pi^a \defeq  \pair{\xi}{\pi}^a : E^a \to (A\times B)^a \simeq B. \]

§.§ Cocartesianness on the left

A two-sided family $P:A \to B \to \UU$ is cocartesian on the left if the family $P_B:A \to \UU$ is cocartesian, and every $P_B$-cocartesian arrow in $\totalty{P}$ is $P^A$-vertical.

[Cocartesian families]
A family $P:A \to \UU$ is cocartesian if and only if it is cocartesian on the left, seen as a family $P: (A \to \UU) \simeq (A \to 1 \to \UU)$.

For a two-sided family $P:A \to B \to \UU$, corresponding to $\pair{\xi}{\pi}:E \to A \times B$, the following are equivalent:

*  The fibered functor

\[\begin{tikzcd}
E && {A \times B} \\
& B
\arrow["{\langle \xi, \pi \rangle}", two heads, from=1-1, to=1-3]
\arrow["\pi"', from=1-1, to=2-2]
\arrow["q", from=1-3, to=2-2]
\end{tikzcd}\]

is a cocartesian fibration sliced over $B$.

*  The fibered functor

\[\begin{tikzcd}
E && {A \times B} \\
& A
\arrow["{\langle \xi, \pi \rangle}", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["p", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

is a cocartesian functor between cocartesian fibrations.

*  The fibered functor given by

\[ \iota_\xi: E \to_{A \times B} \comma{\xi}{A}, \quad \iota_\xi(a,b,e) \defeq \angled{a,a,\id_a,b,e} \]

has a fibered left adjoint $\tau_\xi$:

\[\begin{tikzcd}
E &&&& {\xi \downarrow A} \\
&& {A \times B}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\iota_\xi}"{description}, from=1-1, to=1-5]
\arrow["{\langle \xi,\pi \rangle}"', from=1-1, to=2-3]
\arrow["{\langle \partial_1,\pi \circ \partial_0\rangle}", from=1-5, to=2-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\tau_\xi}"{description}, curve={height=18pt}, dashed, from=1-5, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}\]

*  The two-sided family $P:A \to B \to \UU$ is cocartesian on the left.

We abbreviate $\varphi \defeq \pair{\xi}{\pi}: E \to_B A \times B$.

$\ref{it:coc-left-i} \iff \ref{it:coc-left-iv}$ The fibered functor $\varphi$ being a cocartesian fibration sliced over $B$ is equivalent to the condition that for all $q$-vertical maps exist a $\varphi$-cocartesian lift ( to a given initial vertex). By Rezk-completeness, this is equivalent to any arrow $\pair{u:a \to a'}{\id_b}$ having a $\varphi$-cocartesian lift $f$ with prescribed initial vertex $e:P(a,b)$. Note that $f$ is $\pi$-vertical. Projecting away the $B$-component, we obtain that $f$ is $\xi$-cocartesian.

$\ref{it:coc-left-ii} \iff \ref{it:coc-left-iv}$ Since $p:A \times B \fibarr A$ is a cocartesian fibration in any case, the assumption is equivalent to $\xi:E \fibarr A$ being a cocartesian fibration and every $\xi$-cocartesian arrow being mapped to $p$-cocartesian arrows under $\varphi$. But $\varphi$ is just the projection pairing $\pair{\xi}{\pi}$, and $p$-cocartesian arrows are exactly given by arrows whose $B$-component is an identity. Projecting down to $B$ this means exactly that the $\xi$-cocartesian arrows are $\pi$-vertical.

$\ref{it:coc-left-iii} \implies\ref{it:coc-left-iv}$ We denote

\[ \tau_\xi(a',b,u:a\to a',e) \defeq  \angled{a',b,\widehat{\tau}_{\xi,a',b}(u,e)}. \]

Again, similarly to the considerations in the proof of <Ref>, the unit is a family of arrows

\[ \eta:\prod_{a',b:A} \prod_{a:A, u:a \to_A a'} \prod_{e:P(a,b)} \angled{a',b,a,u,e} \to \angled{a',b,a',\id_{a'}, \widehat{\tau}_{\xi,a',b}(u,e)},\]

illustrated as follows:

\[\begin{tikzcd}
e && {\widehat{\tau}_{\xi,a',b}(u,e)} \\
a && {a'} \\
{a'} && {a'} \\
{a'} && {a'} \\
b && b
\arrow["{\eta_{a',b,a,u,e}}", from=1-1, to=1-3, cocart]
\arrow["u"', from=2-1, to=3-1]
\arrow["u", from=2-1, to=2-3]
\arrow["{\id_{a'}}", Rightarrow, no head, from=3-1, to=3-3]
\arrow["{\id_{a'}}", Rightarrow, no head, from=2-3, to=3-3]
\arrow["{\id_{a'}}", Rightarrow, no head, from=4-1, to=4-3]
\arrow["{\id_{b}}", Rightarrow, no head, from=5-1, to=5-3]
\arrow[curve={height=12pt}, Rightarrow, dotted, no head, from=1-1, to=2-1]
\arrow[curve={height=-12pt}, Rightarrow, dotted, no head, from=1-3, to=2-3]
\arrow[curve={height=12pt}, Rightarrow, dotted, no head, from=3-1, to=4-1]
\arrow[curve={height=-12pt}, Rightarrow, dotted, no head, from=3-3, to=4-3]
\end{tikzcd}\]

By assumption, the transposing map induced by $\eta$ is an equivalence:

\begin{align*}
\Phi_\eta & : \prod_{\substack{a',a'':A \\ b,b':B}} \prod_{\substack{u':a' \to_A a'' \\ v:b \to_B b'}} \prod_{\substack{a:A \\ u:a \to_A a' \\ e:P(a,b)}} \prod_{\substack{a'':A \\ b':B \\ d:P(a'',b')}} \left( \angled{a',b,\widehat{\tau}_{\xi,a',b}(u,e):P(a',b)} \to_{\pair{u'}{v}} \angled{a'',b',d} \right) \\
\stackrel{\simeq}{\longrightarrow} & \left( \angled{a',b,a,u:a \to_A a', e:P(a,b)} \to_{\pair{u'}{v}}  \angled{a'',b',a'', \id_{a''}, d:P(a'',b')} \right), \\
\Phi_\eta & \defeq \lambda u',v,e,d,g.\iota_\xi(g) \circ \eta_{u,e} : \big(e \to_{\pair{v}{g}}^P d\big)
\end{align*}

After contracting away redundant data, this is equivalent to the proposition

\[ \prod_{h:e \to^P_{\pair{u'u}{v}} d} \isContr\Big( \sum_{g:\widehat{\tau}_{\xi,a',b}(u,e) \to^P_{\pair{u'}{v}} d} g \circ^P_{\eta_{u,e}} = h \Big), \]

<Ref> for illustration. But this precisely means that $\xi:E \fibarr A$ is a cocartesian fibration whose cocartesian lifts all are $\pi$-vertical, namely the components of the fibered unit $\eta$.

$\ref{it:coc-left-iv} \implies\ref{it:coc-left-iii}$ We can strictify the diagram as follows, including the fibered left adjoint to be defined:

\[{\small \begin{tikzcd}
{E \simeq \sum_{\substack{a':A \\ b:B}} P(a',b)} &&&& {\sum_{\substack{a,a':A \\ b:B}} (a \to_A a') \times P(a,b) \simeq \xi \downarrow A} \\
\\
&& {A \times B}
\arrow["{\langle \partial_1, \pi \circ \partial_0\rangle}", two heads, from=1-5, to=3-3]
\arrow["{\langle \xi,\pi \rangle}"', two heads, from=1-1, to=3-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\iota_\xi}"{description}, curve={height=12pt}, from=1-1, to=1-5]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\tau_\xi}"', curve={height=6pt}, from=1-5, to=1-1]
\arrow["\dashv"{anchor=center,rotate=-90}, draw=none, from=1, to=0]
\end{tikzcd}}\]

The fibered “inclusion” map is defined as

\[ \iota_\xi(a',b,e) \defeq \angled{a',b,a',\id_{a'},e}.\]

By the preconditions from <Ref>, the map $\xi:E \fibarr A$ is a cocartesian fibration, moreover whose cocartesian lifts are all $\pi$-vertical. We let

\[ \tau_\xi(a',b,a,u:a \to a',e) \defeq \angled{a',b,u_!\,e}.\]

Now, similarly, as in the proof of <Ref>, we exhibit the fibered adjunction as given by a fiberwise equivalence[Here, we write $\xi_b \defeq (\id_A \times b)^*\pair{\xi}{\phi}: E_b \simeq \sum_{a:A} P(a,b) \fibarr A$, giving rise to the comma object $\sum_{a:A} (a \to_A a') \times P(a,b)$]

\begin{align*}
\prod_{\substack{a':A \\ b:B}} \prod_{\substack{a:A \\ u:a \to_A a' \\ e:P(a,b)}} & \prod_{e':P(a',b)} \big( \tau_{\xi,a',b}(a,u,u_!\,e) \to_{P(a',b)} e'\big) \\ & \stackrel{\simeq}{\longrightarrow} \big( \angled{a,u,e} \longrightarrow_{\comma{\xi_b}{A}}  \angled{a',\id_{a'}, e'} \big)
\end{align*}

as follows: Over a point $\pair{a'}{b}:A \times B$ in the base, fix $\angled{a:A, u:a \to_A a', e:P(a,b)}$, $e':P(a',b)$, and define maps between the transposing hom types, in opposite directions,

\begin{align*}
& \Phi(g:u_!e \to_{P(a',b)} e') \defeq g \circ \xi_!(u,e), \\
& \Psi(u:a \to_A a', u:u \to_{\comma{A}{a}} \id_{a'}, h:e \to_u^P e') \defeq \tyfill_{\xi_!(u,e)}^\xi(h).
\end{align*}

Again, by the universal property of cocartesian lifts it can be checked that the two maps are quasi-inverses. Note that by assumption, the $\xi$-cocartesian lifts are $\pi$-vertical, so everything stays in “the fibers over $b$”, or, more precisely, in the pullback type $(\id_A \times b)^*E$.

\[\begin{tikzcd}
e && d \\
{\widehat{\eta}(u,e)} && d \\
a && {a''} \\
{a'} && {a''} \\
{a'} && {a''} \\
b && {b'}
\arrow["{\eta_{u,e}}"', swap, description, from=1-1, to=2-1, cocart]
\arrow["u"', from=3-1, to=4-1]
\arrow["{u'u}", from=3-1, to=3-3]
\arrow["{u'}", from=4-1, to=4-3]
\arrow["{\id_{a''}}"', Rightarrow, no head, from=3-3, to=4-3]
\arrow["{u'}", from=5-1, to=5-3]
\arrow["v", from=6-1, to=6-3]
\arrow["{\forall \,h}", from=1-1, to=1-3]
\arrow[Rightarrow, no head, from=1-3, to=2-3]
\arrow[curve={height=30pt}, Rightarrow, dotted, no head, from=1-1, to=3-1]
\arrow[curve={height=-30pt}, Rightarrow, dotted, no head, from=1-3, to=3-3]
\arrow["{\exists! \, g}", from=2-1, to=2-3, dashed]
\arrow[curve={height=30pt}, Rightarrow, dotted, no head, from=2-1, to=4-1, crossing over]
\arrow[curve={height=-30pt}, Rightarrow, dotted, no head, from=2-3, to=4-3, crossing over]
\end{tikzcd}\]

Fibered adjunction criterion for cocartesian-on-the-left families

\[\begin{tikzcd}
&& e && {e'} \\
E && {u_!'e} \\
&& {a''} && {a'} \\
&& a && {a'} \\
{A \times B} && b && {b'}
\arrow["{\xi_!(u',e)}"', from=1-3, to=2-3, cocart]
\arrow["h", from=1-3, to=1-5]
\arrow["g"', dashed, from=2-3, to=1-5]
\arrow["{u'}"', from=3-3, to=4-3]
\arrow["u", from=4-3, to=4-5]
\arrow["{uu'}", dashed, from=3-3, to=3-5]
\arrow[Rightarrow, no head, from=3-5, to=4-5]
\arrow["v", from=5-3, to=5-5]
\arrow[two heads, from=2-1, to=5-1]
\end{tikzcd}\]

Lifts in a family that is cocartesian on the left

By dualization, one obtains the notion of a two-sided family cartesian on the right. As a corollary, we obtain a characterization of the conjunction of both properties.

A two-variable family $P:A \to B \to \UU$ is cocartesian on the left and cartesian on the right if and only if the following equivalent propositions are true.

* The fibered functor

\[\begin{tikzcd}
E && {A \times B} \\
& B
\arrow["{\langle \xi,\pi \rangle}", two heads, from=1-1, to=1-3]
\arrow["\pi"', two heads, from=1-1, to=2-2]
\arrow["q", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

is both a cartesian functor between cartesian fibrations and a relative cocartesian fibration over $B$.

* The fibered functor

\[\begin{tikzcd}
E && {A \times B} \\
& A
\arrow["{\langle \xi,\pi \rangle}", two heads, from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["p", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

is both a cocartesian functor between cocartesian fibrations and a relative cartesian fibration over $B$.

In the case that $P:A \to B \to \UU$ is cocartesian on the left and cartesian on the right, we denote the ensuing lifting operations as follows. Given $a:A$, $b:B$, $e:P\,a\,b$, for arrows $u:a \downarrow A$, $v:B \downarrow b$, there are lifts

\[ P_!(u,e): e \cocartarr_{\pair{u}{b}} u_!\,e, \quad P^*(v,e): v^*\,e \cartarr_{\pair{a}{v}} e,\]

where in the notation we identify elements and identity maps.

The notion of two-sided cartesian fibration adds on top a certain compatibility condition between the lifts of different variance. Before defining two-sided cartesian fibrations in <Ref>, we first investigate the compatibility condition in the following lemma.

For Rezk types $A$ and $B$, let $P: A \to B \to \UU$ be a two-variable family which is cocartesian on the left and cartesian on the right. Denoting its unstraightening as $\varphi\jdeq \pair{\xi}{\pi}:E \fibarr A \times B$, for arrows $u:a \to_A a'$, $v:b' \to_B b$ and a point $e:P\,a\,b$ we abbreviate:

\begin{align*}
k & \defeq \xi_!(u,e):e \cocartarr^\xi_{\pair{u}{b}} u_!\,e  &  k' & \defeq \pi^*(v,e):v^*\,e \cartarr^\pi_{\pair{a}{v}} e \\
f & \defeq \xi_!(u,v^*\,e) : v^*\,e \cocartarr^\xi_{\pair{u}{b'}} u_!\,v^*\,e & f' & \defeq \pi^*(v,u_! \,e) : v^*\,u_!\,e \cartarr^\pi_{\pair{a'}{v}} u_!\,e \\
g & \defeq \tyfill_f^\xi(k'k): u_!\,v^*\,e \to_{\pair{a'}{v}}^\xi u_!\,e & g' & \defeq \tyfill_{f'}^\pi(k'k): v^*\,e \to^\pi_{\pair{u}{b'}} v^*\, u_!\,e
\end{align*}

We claim that there is an identification between the following two induced morphisms $h,h':u_!\,v^*\,e \to_{P(a',b')} v^*\,u_!\,e$  ( <ref>):

\[\begin{tikzcd}
{v^*\,e} && e && {u_!\,e} \\
{u_!v^*\,e} &&&& {v^* u_!\,e} \\
{v^*\,e} && e && {u_!\,e} \\
{u_!v^*\,e} &&&& {v^* u_!\,e}
\arrow["f"', from=1-1, to=2-1]
\arrow["{k'}", from=1-1, to=1-3, cart]
\arrow["k", from=1-3, to=1-5, cocart]
\arrow["{f'}"', from=2-5, to=1-5, cart]
\arrow["{h:\defeq \tyfill^\pi_{f'}(g)}"', dashed, from=2-1, to=2-5]
\arrow["g"{description}, dashed, from=2-1, to=1-5]
\arrow["{k'}", from=3-1, to=3-3, cart]
\arrow["k", from=3-3, to=3-5, cocart]
\arrow["f"', from=3-1, to=4-1, cocart]
\arrow["{h':\defeq \tyfill^\xi_{f}(g')}"', dashed, from=4-1, to=4-5]
\arrow["{f'}"', from=4-5, to=3-5, cart]
\arrow["{g'}"{description}, dashed, from=3-1, to=4-5]
\end{tikzcd}\]

It is sufficient to provide an identification $g=f'h'$. For this, it is sufficient—and necessary—to provide a witness for $f'(h'f) = k'k$. But this follows from $f'h=g$, since $gf=k'k$.

\[\begin{tikzcd}
E && {v^*e} && e && {u_!e} \\
&&& {u_!v^*e} &&&& {v^*u_!e} \\
{A \times B} && {\langle a,b'\rangle} && {\langle a,b \rangle} && {\langle a',b\rangle} \\
{} &&& {\langle a',b' \rangle} &&&& {\langle a',b'\rangle}
\arrow["{\xi_!(u,v^*e)}"'{pos=0.2}, from=1-3, to=2-4, cocart]
\arrow["{\pi^*(v,e)}", from=1-3, to=1-5, cart]
\arrow["{\xi_!(u,e)}", from=1-5, to=1-7, cocart]
\arrow["{\pi^*(v,u_!e)}"'{pos=0.1}, from=2-8, to=1-7, cart]
\arrow[dashed, from=2-4, to=2-8]
\arrow["{\langle u,b' \rangle}"', from=3-3, to=4-4]
\arrow["{\langle a,v \rangle}", from=3-3, to=3-5]
\arrow["{\langle u,b \rangle}", from=3-5, to=3-7]
\arrow[two heads, from=1-1, to=3-1]
\arrow["{\langle a',v \rangle}"', from=4-8, to=3-7]
\arrow[Rightarrow, no head, from=4-4, to=4-8]
\end{tikzcd}\]

Comparing cartesian and cocartesian transport

§.§ Two-sided cartesian families

§.§.§ Definition and examples of two-sided cartesian fibrations

Let $P:A \to B \to \UU$ be a (two-sided) family, where $A$ and $B$ are Rezk types. We call $P$ a two-sided cartesian family (short: two-sided family) if

* $P$ is cocartesian on the left and cartesian on the right,

*  and $P$ satisfies the condition that cocartesian and cartesian lifts commute: for any $a:A$, $b:B$, $e:P\,a\,b$ and arrows $u:a \to_A a'$, $v:b' \to_B b$, the filler $\kappa:u_!(v^*e) \to v^*(u_!e)$ from <Ref> is an isomorphism, hence there is an identity $u_!v^*e =_{P(a',b')} v^*u_!e$.

For any Rezk type $A$ the $\hom$-span

\[\begin{tikzcd}
& {A^{\Delta^1}} \\
A && A
\arrow["{\partial_1}"', from=1-2, to=2-1]
\arrow["{\partial_0}", from=1-2, to=2-3]
\end{tikzcd}\]

is a two-sided cartesian fibration: the $\partial_1$-cocartesian lift are exactly the $\partial_0$-vertical squares, and vice versa, and the transports satisfy the necessary compatibility condition ( <cit.>). In fact, this gives an example of a discrete two-sided family, since all the fibers are discrete types,  <cit.>, as well as <Ref> and <Ref>.

More generally, comma fibrations of the form

\[\begin{tikzcd}
& {\comma{f}{g}} \\
A && B
\arrow["{\partial_1}"', from=1-2, to=2-1]
\arrow["{\partial_0}", from=1-2, to=2-3]
\end{tikzcd}\]

for functors $f : B \to A$ and $g : C \to A$ yield examples of two-sided discrete cartesian fibrations, by the analogous arguments.

Furthermore, given two-sided cartesian fibrations $E \fibarr A \times B$ and $F \fibarr B \times C$, we will see that their span composition

\[\begin{tikzcd}
&& {E \times_B Q } \\
& E && Q \\
A && B && C
\arrow[two heads, from=2-2, to=3-1]
\arrow[two heads, from=2-2, to=3-3]
\arrow[two heads, from=2-4, to=3-3]
\arrow[two heads, from=2-4, to=3-5]
\arrow[two heads, from=1-3, to=2-2]
\arrow[two heads, from=1-3, to=2-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=3-3]
\end{tikzcd}\]

is a two-sided cartesian fibration, too. For example, composing the $\hom$-span $A^{\Delta^1} \fibarr A \times A$, which is a discrete two-sided fibration, with itself yields a two-sided cartesian fibration

\[\begin{tikzcd}
&& {A^{\Delta^2}} \\
& {A^{\Delta^1}} && {A^{\Delta^1}} \\
A && A && A
\arrow["{\partial_1}"', two heads, from=2-2, to=3-1]
\arrow["{\partial_0}", two heads, from=2-2, to=3-3]
\arrow["{\partial_1}"', two heads, from=2-4, to=3-3]
\arrow["{\partial_0}", two heads, from=2-4, to=3-5]
\arrow[two heads, from=1-3, to=2-2]
\arrow[two heads, from=1-3, to=2-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=3-3]
\end{tikzcd}\]

whose total type is equivalent to $A^{\Delta^2}$ due to $A$ being Segal. Its fiber at $\langle c,a \rangle : A \times A$ is $\sum_{b:A} \hom(a,b) \times \hom(b,c)$, which is in general not discrete. Thus, $A^{\Delta^2} \fibarr A \times A$ is an example of a not necessarily discrete two-sided cartesian fibration.[We are grateful to Emily Riehl for pointing out this example.]

Furthermore, any family $P : A \times B \to \UU$ with associated span $\xi : A \leftarrow E \rightarrow B : \pi$ of functors gives rise to the free-two sided fibration, see <cit.>:

\[\begin{tikzcd}
&&& {L^{\mathrm{2s}}(E)} \\
&& {\comma{\xi}{A}} && {\comma{B}{\pi}} \\
& {A^{\Delta^1}} && E && {B^{\Delta^1}} \\
A && A && B && B
\arrow[two heads, from=1-4, to=2-3]
\arrow[two heads, from=1-4, to=2-5]
\arrow[two heads, from=2-3, to=3-4]
\arrow[two heads, from=2-5, to=3-4]
\arrow[from=2-3, to=3-2]
\arrow[from=2-5, to=3-6]
\arrow["{{\partial_0}}", two heads, from=3-2, to=4-3]
\arrow["\xi"', from=3-4, to=4-3]
\arrow["\pi", from=3-4, to=4-5]
\arrow["{{\partial_1}}"', two heads, from=3-6, to=4-5]
\arrow["{{\partial_1}}"', two heads, from=3-2, to=4-1]
\arrow["{{\partial_0}}", two heads, from=3-6, to=4-7]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=2-3, to=4-3]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=2-5, to=4-5]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-4, to=3-4]
\end{tikzcd}\]

That this is a two-sided cartesian fibration satisfying the corresponding universal property can be proven using the results about the free cocartesian fibration from <cit.> and their dual analogue for the free cartesian fibration.

The fiber of $L^{\mathrm{2s}}(E) \fibarr A \times B$ at $\pair{a}{b} : A \times B$ is given, up to equivalence, by the type $\sum_{a' : A} \sum_{b' : B} (a' \to_A a) \times (b \to_B b') \times P(a',b')$.

§.§.§ Characterization of two-sided cartesian families

Let $P:A \to B \to \UU$ be a family with both $A$ and $B$ Rezk which is cocartesian on the left and cartesian on the right. We denote by $\xi:F \fibarr A$ and $\pi:E \fibarr B$, resp., the unstraightenings.
Then cocartesian and cartesian lifts commute if and only if the following property is satisfied:
Given $u:a \to_A a'$, $v:b' \to_B b$, $e:P\,a\,b$, and a diagram

\[\begin{tikzcd}
{v^*\,e} && e \\
d && {u_!\,e}
\arrow["f"', from=1-1, to=2-1]
\arrow["{k'\defeq \pi^*(v,e)}", from=1-1, to=1-3, cart]
\arrow["g"', from=2-1, to=2-3]
\arrow["{k \defeq \xi_!(u,e)}", from=1-3, to=2-3, cocart]
\end{tikzcd}\]

where $g$ (and necessarily $k'$) is $\xi$-vertical and $f$ (and necessarily $k$) is $\pi$-vertical. Then $f$ is $\xi$-cocartesian if and only if $g$ is $\pi$-cartesian.

In light of <Ref>, the commutation condition is equivalent to the type of paths $h:u_!\,v^*\,e =_{P(a',b')} v^*\,u_!\,e$ together with witnesses, necessarily propositional, that the following diagram commutes:

\[\begin{tikzcd}
&& {v^*\,e} &&&& e \\
\\
&& {u_!\,v^*\,e} &&&& {u_!\,e} \\
\\
\arrow["{f \defeq \xi_!(u,v^*\,e)}", from=1-3, to=3-3, cocart]
\arrow["{g \defeq \tyfill_f^\xi(kk')}", dashed, from=3-3, to=3-7]
\arrow["{k' \defeq \pi^*(v,e)}", from=1-3, to=1-7, cart]
\arrow["{k \defeq \xi_!(u,e)}", from=1-7, to=3-7, cocart]
\arrow["{g' \defeq \tyfill_{f'}^\pi(kk')}"', dashed, from=1-3, to=5-1]
\arrow["{f' \defeq \pi^*(v,u_!\,e)}"', from=5-1, to=3-7, cart]
\arrow["h"{description}, Rightarrow, no head, from=5-1, to=3-3]
\end{tikzcd}\]

But since these diagrams commute in any case by the assumptions
(recall <Ref>) said type is equivalent to the proposition that the filler $h$ is an isomorphism:

\[\begin{tikzcd}
&& {u_!\,v^*\,e} \\
{v^*\,e} && {v^*\,u_!\,e} && {u_!\,e}
\arrow["h"', dashed, from=1-3, to=2-3]
\arrow["{f'}"', from=2-3, to=2-5, cart]
\arrow["g", from=1-3, to=2-5]
\arrow["{g'}"', from=2-1, to=2-3]
\arrow["f", from=2-1, to=1-3, cocart]
\end{tikzcd}\]

Finally due to the commutation of both of the “completed squares” above, this is equivalent to the new alternative criterion: up to identification, $f$ is $\xi$-cocartesian if and only if $g$ is $\pi$-cartesian.

\[\begin{tikzcd}
{\mathrm{Vert}_\pi(E)} & {v^*\,e} && e & {E \times_{A \times B} \mathrlap{\mathrm{Vert}_q(A \times B)}} \\
{} & {v^*\,e'} && {e'} && {v^*e} & e & {} & {} \\
& a && a && a & a && {} \\
& {a'} && {a'} && {a'} & {a'} && {} \\
B & b && {b'} & B & b & {b'}
\arrow["{\pi^*(v,e)}", from=1-2, to=1-4, cocart]
\arrow["{\mathrm{fill}}"', dashed, from=1-2, to=2-2]
\arrow["{\pi^*(v,e')}"', from=2-2, to=2-4, cocart]
\arrow["f", from=1-4, to=2-4]
\arrow["u"', from=3-2, to=4-2]
\arrow[Rightarrow, no head, from=3-2, to=3-4]
\arrow["u", from=3-4, to=4-4]
\arrow[Rightarrow, no head, from=4-2, to=4-4]
\arrow["v", from=5-2, to=5-4]
\arrow["u"', from=3-6, to=4-6]
\arrow["\psi"{description}, from=1-5, to=5-5]
\arrow["{\pi'}"{description}, two heads, from=1-1, to=5-1]
\arrow["{\pi^*(v,e)}", from=2-6, to=2-7, cocart]
\arrow[Rightarrow, no head, from=3-6, to=3-7]
\arrow["u", from=3-7, to=4-7]
\arrow[Rightarrow, no head, from=4-6, to=4-7]
\arrow["v", from=5-6, to=5-7]
\end{tikzcd}\]

Cartesian lifts in the induced fibrations $\pi'$ and $\psi$

The following theorem finally contains several characterizations of a two-variable family being two-sided cartesian.[We are indebted to Emily Riehl for helpful explanations and discussions about <cit.>.] This consists in several sliced Chevalley/fibered adjoint criteria and a criterion formulated directly on the level of two-variable families.

For a family $P:A \to B \to \UU$, corresponding to $\varphi \defeq \pair{\xi}{\pi}: E \defeq \sum_{a:A,b:B} P(a,b) \to A \times B$, the following are equivalent:

*  The two-variable family $P$ is two-sided.

*  Considering

\[\begin{tikzcd}
E && {A \times B} \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\pi"', two heads, from=1-1, to=2-2]
\arrow["q", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

the map $\pi$

is a cartesian fibration, the functor $\varphi$ is cartesian and a cocartesian fibration sliced over $B$. Furthermore, the fibered LARI

\[ \chi_B: \VertArr_q(A \times B) \times_{A\times B} E \to_B \VertArr_\pi(E)\]

is a cartesian functor.

*  Considering

\[\begin{tikzcd}
E && {A \times B} \\
& B
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\pi"', two heads, from=1-1, to=2-2]
\arrow["q", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

the map $\pi$

is a cartesian fibration, the functor $\varphi$ is cartesian and a cocartesian fibration sliced over $B$. Furthermore, the fibered LARI

\[ \tau_B: \VertArr_q(A \times B) \times_{A\times B} E \to_B E\]

is a cartesian functor.

*  Considering

\[\begin{tikzcd}
E && {A \times B} \\
& A
\arrow["\varphi", from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=2-2]
\arrow["p", two heads, from=1-3, to=2-2]
\end{tikzcd}\]

the map $\xi$

is a cocartesian fibration, the functor $\varphi$ is cocartesian and a cartesian fibration sliced over $A$. Furthermore, the fibered RARI

\[ \chi^A: \VertArr_p(A \times B) \times_{A\times B} E \to_A \VertArr_\xi(E)\]

is a cocartesian functor.

The fibered adjoints in the following diagram exist:

\[\begin{tikzcd}
E &&& {B \downarrow \pi} \\
\\
&& {\xi \downarrow A} &&& {\xi \downarrow A \times_E B \downarrow \pi} \\
\\
&&& {A\times B}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\iota^\pi}"{description}, from=1-1, to=1-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\iota_\xi}"{description}, from=1-1, to=3-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\langle \iota_\xi \circ \partial_1',\id \rangle}"{description, pos=0.25}, from=1-4, to=3-6]
\arrow["{\langle \partial_1, \pi \, \partial_0 \rangle}"{description}, two heads, from=3-3, to=5-4]
\arrow["{\langle \partial_1, \partial_0\rangle}"{description}, two heads, curve={height=-15pt}, from=3-6, to=5-4]
\arrow["{\langle \xi\,\partial_1, \partial_0 \rangle}"{description, pos=0.3}, two heads, from=1-4, to=5-4]
\arrow["\varphi"{description}, shift right=2, curve={height=30pt}, two heads, from=1-1, to=5-4]
\arrow[""{name=4, anchor=center, inner sep=0}, "{\tau_\xi}"{description}, curve={height=-18pt}, dashed, from=3-3, to=1-1]
\arrow[""{name=5, anchor=center, inner sep=0}, "\ell"{description}, curve={height=18pt}, dashed, from=3-6, to=1-4]
\arrow[""{name=7, anchor=center, inner sep=0}, "{\tau^\pi}"{description}, curve={height=18pt}, dashed, from=1-4, to=1-1]
\arrow["\dashv"{anchor=center, rotate=-91}, draw=none, from=7, to=0]
\arrow["\dashv"{anchor=center, rotate=-133}, draw=none, from=5, to=3]
\arrow["\dashv"{anchor=center, rotate=44}, draw=none, from=4, to=1]
\arrow[""{name=6, anchor=center, inner sep=0}, "r"{description}, curve={height=-24pt}, dashed, from=3-6, to=3-3, crossing over]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\langle \id, \iota^\pi \circ \partial_0' \rangle}"{description, pos=0.6}, from=3-3, to=3-6, crossing over]
\arrow["\dashv"{anchor=center, rotate=108}, draw=none, from=6, to=2]
\end{tikzcd}\]

where the pullback type is given by:

\[\begin{tikzcd}
{\comma{\xi}{A} \times_E \comma{B}{\pi}} && {\comma{\xi}{A}} \\
{\comma{B}{\pi}} && E
\arrow[from=1-1, to=2-1]
\arrow["{\partial_1}"', from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\partial_0'}", from=1-3, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

Moreover, the mate of the identity $2$-cell defines a fibered isomorphism

\[ \prod_{a:A, b:B} (\tau_\xi \circ r)_{a,b} =_{Q(a,b) \to P(a,b)} (\tau^\pi \circ \ell)_{a,b},\]

\[ Q: A \times B \to \UU, \quad Q(a,b) \simeq \comma{a}{A} \times \comma{B}{b} \times P(a,b)\]

is the straightening of the map

\[ F \defeq \comma{\xi}{A} \times_E \comma{B}{\pi} \fibarr A \times B.\]

$\ref{it:char-two-sid-i} \iff \ref{it:char-two-sid-ii}$ By <Ref>, the map $P: A \to B \to \UU$ is cocartesian on the left and cartesian on the right if and only if $\varphi: E \to_B A \times B$ is both a cartesian functor between cartesian fibrations and a cocartesian fibration sliced over $B$.

In the following, we assume this is satisfied for $P$.

Thus, we are left to show that, under this assumption—$P$ being cocartesian on the left and cartesian on the right—the following holds:

\begin{align*}
& \text{``The fibered LARI $\chi_B: \VertArr_q(A \times B) \times_{A\times B} E \to_B \VertArr_\pi(E)$} \\
& \text{is a cocartesian functor.''} \\
& \iff  \text{``In $P$, cocartesian and cartesian lifts commute.''}
\end{align*}

We write $F \defeq \mathrm{Vert}_q(A \times B) \times_{A \times B} E \fibarr B$, so by projection equivalence, we consider the projection

\[ \psi : \sum_{b:B} \sum_{a:A} (\comma{a}{A} \times P(a,b)) \simeq F \fibarr B. \]

The induced sliced Leibniz cotensor is given by

\[ \kappa : \VertArr_\pi(E) \to_B F,\quad \kappa_b\big(u:\Delta^1 \to A,f:\prod_{t:\Delta^1} P(u(t),b) \big) \defeq \angled{\partial_0\,u,u, \partial_0\,f}. \]

It  has a fibered LARI $\mu: F \to_B \VertArr_\pi(E)$ as indicated in:

\[\begin{tikzcd}
{\mathrm{Vert}_\pi(E)} && {\mathrm{Vert}_q(A \times B) \times_{A \times B} E} \\
\\
& B
\arrow[""{name=0, anchor=center, inner sep=0}, "\kappa"{description}, curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\mu"{description}, curve={height=18pt}, dashed, from=1-3, to=1-1]
\arrow["{\pi'}"{description}, two heads, from=1-1, to=3-2]
\arrow["\psi"{description}, two heads, from=1-3, to=3-2]
\arrow["\dashv"{anchor=center, rotate=-94}, draw=none, from=1, to=0]
\end{tikzcd}\]

\[\begin{tikzcd}
{e''} & e & {e''} & e && {e'} & e & {e'} & e \\
{e'''} & {e'} &&&&&& {u_!\,e'} & {u_!\,e} \\
{a''} & a & {a''} & a && {a''} & a & {a''} & a \\
{a'''} & {a'} & {a'''} & {a'} && {a'''} & {a'} & {a'''} & {a'} \\
{b'} & b & {b'} & b && {b'} & b & {b'} & b
\arrow["g", from=1-1, to=1-2]
\arrow["{f'}"', from=1-1, to=2-1]
\arrow["f", from=1-2, to=2-2]
\arrow["{g'}"', from=2-1, to=2-2]
\arrow["m", from=3-1, to=3-2]
\arrow["{u'}", from=3-1, to=4-1]
\arrow[""{name=0, anchor=center, inner sep=0}, "u"', from=3-2, to=4-2]
\arrow["v", from=5-1, to=5-2]
\arrow["g", from=1-3, to=1-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "{u'}", from=3-3, to=4-3]
\arrow[Rightarrow, dotted, no head, from=1-3, to=3-3]
\arrow[Rightarrow, dotted, no head, from=1-4, to=3-4]
\arrow["u"', from=3-4, to=4-4]
\arrow["m", from=3-3, to=3-4]
\arrow["{m'}"', from=4-3, to=4-4]
\arrow["v", from=5-3, to=5-4]
\arrow["{m'}"', from=4-1, to=4-2]
\arrow["v", from=5-8, to=5-9]
\arrow["u", from=3-6, to=4-6]
\arrow[from=3-6, to=3-7]
\arrow[from=4-6, to=4-7]
\arrow[""{name=2, anchor=center, inner sep=0}, "u"', from=3-7, to=4-7]
\arrow["f", from=1-6, to=1-7]
\arrow[Rightarrow, dotted, no head, from=1-6, to=3-6]
\arrow[Rightarrow, dotted, no head, from=1-7, to=3-7]
\arrow["{\xi_!(u,e')}"', from=1-8, to=2-8, cocart]
\arrow["f", from=1-8, to=1-9]
\arrow["{\xi_!(u,e)}", from=1-9, to=2-9, cocart]
\arrow["{\mathrm{fill}}"', dashed, from=2-8, to=2-9]
\arrow[""{name=3, anchor=center, inner sep=0}, "u", from=3-8, to=4-8]
\arrow[from=3-8, to=3-9]
\arrow["u"', from=3-9, to=4-9]
\arrow[from=4-8, to=4-9]
\arrow["v", from=5-6, to=5-7]
\arrow["\kappa", shorten <=6pt, shorten >=6pt, maps to, from=0, to=1]
\arrow["\mu", shorten <=6pt, shorten >=6pt, maps to, from=2, to=3]
\end{tikzcd}\]

Action on arrows of the fibered functors $\kappa: F\to_B \VertArr_\pi(E)  : \mu$

By our discussion of cocartesian-on-the-left fibrations,  <Ref>, the fibered LARI $\mu:F \to \VertArr_\pi(E)$ at $b:B$ is given by

\[ \mu_b(a:A,u:\comma{a}{A},e:P(a,b)) \defeq \pair{u:\comma{a}{A}} {\xi_!(u,e):e \to_{\pair{u}{b}}^P u_!\,e}. \]

By the closure properties of cartesian fibrations <cit.> we obtain that the pulled back maps

\[\pi' \defeq \cst^*\pi^{\Delta^1}: \VertArr_\pi(E) \fibarr B\]

\[q' \defeq \cst^*q:\VertArr_q(A \times B) \fibarr B\]

are cartesian fibrations. Moreover, by op. cit., Proposition 5.3.10, so is $\psi \defeq q' \times_q \pi : F \fibarr B$. By the computations of lifts, as elobarated in op. cit., Propositions 5.2.9, 5.3.9, and 5.3.10, the cartesian lifts in $\pi': \VertArr_\pi(E) \fibarr B$ and, resp. $\psi: F \fibarr B$ are given by as follows ( <Ref> for illustration):

\begin{align*}
& (\pi')^*\left( v:b \to_B b', \pair{u:a \to_A a'}{f:e \to^P_{\pair{u}{a}} e'}\right) \\
& = \left \langle v, \pair{\id_a}{\id_a'} : u \rightrightarrows_A u, \pair{\pi^*(v,e)}{\pi^*(v,e')}: \tyfill \rightrightarrows^P f \right \rangle \\
& \\
& \psi^*\left( v:b\to_B b', \pair{u:a \to_A a'}{e:P(a,b)} \right) \\
& = \left \langle v, \langle \pair{\id_a}{\id_a'}: u \rightrightarrows_A u, \pi^*(v,e): v^* \cartarr^\pi_v e \right \rangle
\end{align*}

Note that, instead of using the formulas for the lifts, one can also directly verify that the given maps are indeed cartesian. Since for $\psi$ this is straightforward to see we only discuss the case of $\pi': \VertArr_\pi(E) \fibarr B$. Consider probing maps as indicated in:

\[\begin{tikzcd}
d && {v^*\,e} && e \\
{d'} && {v^*\,e'} && {e'} \\
{a''} && a && a \\
{a'''} && {a'} && {a'} \\
b && b && b
\arrow["v"{description}, from=5-3, to=5-5]
\arrow["{v'}"{description}, from=5-1, to=5-3]
\arrow["{v'v}"{description}, curve={height=18pt}, from=5-1, to=5-5]
\arrow[Rightarrow, no head, from=4-3, to=4-5, shorten <=9pt, shorten >=9pt]
\arrow["{m'}"{description}, dashed, from=4-1, to=4-3]
\arrow["m"{description, pos=0.7}, curve={height=18pt}, from=4-1, to=4-5]
\arrow["{u'}"', from=3-1, to=4-1]
\arrow["u"', from=3-3, to=4-3]
\arrow[Rightarrow, no head, from=3-3, to=3-5, shorten <=9pt, shorten >=9pt]
\arrow["u", from=3-5, to=4-5]
\arrow["{f'}"', from=1-1, to=2-1]
\arrow["{g'}"{description}, from=2-1, to=2-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "g"{description}, from=1-1, to=1-3]
\arrow["{k :\jdeq \mathrm{fill}}"', dashed, from=1-3, to=2-3]
\arrow["\ell", from=1-3, to=1-5]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\ell'}", from=2-3, to=2-5]
\arrow["f", from=1-5, to=2-5]
\arrow[""{name=2, anchor=center, inner sep=0}, "{h'}"{description}, curve={height=18pt}, from=2-1, to=2-5]
\arrow[""{name=3, anchor=center, inner sep=0}, "h"{description}, curve={height=-18pt}, from=1-1, to=1-5]
\arrow[Rightarrow, no head, from=2-3, to=1-5, shorten <=9pt, shorten >=9pt]
\arrow["{(?)}"{description}, draw=none, from=2-1, to=1-3]
\arrow[shorten <=9pt, shorten >=9pt, Rightarrow, no head, from=2, to=1]
\arrow[shorten <=8pt, shorten >=8pt, Rightarrow, no head, from=0, to=3]
\arrow["m"{description}, dashed, from=3-1, to=3-3]
\arrow["m"{description, pos=0.7}, curve={height=-16pt}, from=3-1, to=3-5, crossing over]
\end{tikzcd}\]

By the property of the $\pi$-cartesian lifts the two triangles and the right hand square commute as indicated. For the square in question on the left hand side we employ a line of reasoning familiar from fibered $1$-category theory: to give a homotopy $kg = g'f'$ it suffices to show that the $\pi$-cartesian arrow $\ell'$ equalizes both composite arrows. Note that from a path $\ell'k = f\ell$ we obtain a chain of homotopies

\[ (\ell' k)g = (f\ell)g = fh = h'f' = (\ell' g')f'\]

as desired. Hence the whole diagram $(?)$ commutes.

Now, the fibered transport functor $\mu:F \to \VertArr_\pi(E)$ is cartesian if and only if it maps $\psi$-cartesian arrows to $\pi'$-cartesian arrows. Its action on $\psi$-cartesian arrows is given by

\begin{align*}
& \mu_v(\psi^*(v,\pair{u}{e}))  = \mu_v\big(\pair{\id_a}{\id_{a'}}:u \rightrightarrows_A u, \pi^*(v,e)\big) \\
= & \Big \langle \pair{\id_a}{\id_{a'}}:u \rightrightarrows_A u, \\
&  \big \langle \pi^*(v,e), \tyfill^\xi_{\xi_!(u,v^*e)}(\xi_!(u,e) \circ \pi^*(v,e))\big \rangle :\xi_!(u,v^*e) \rightrightarrows^P \xi_!(u,e) \Big \rangle,
\end{align*}

for $u:a \to_A a'$, $v:b \to_B  b'$, $e:P(a,b)$.
Conversely, $\pi'$-cartesian lifts of $\mu$-images are of the form

\begin{align*}
& (\pi')^*(v,\mu_b(u,e))  = (\pi')^*(v, \pair{u}{\xi_!(u,e)}) \\
= &	\Big \langle \pair{\id_a}{\id_{a'}} : u \rightrightarrows_A u,\\
&  \pair{\pi^*(v,e)}{\pi^*(v,u_!\,e)}: \tyfill^\pi_{\pi^*(v,u_!\,e)}(\xi_!(u,e) \circ \pi^*(v,e)) \rightrightarrows^P \xi_!(u,e)\Big \rangle.