Cocartesianness is readily verified.[Cf. <ref>.] Namely, for $u':\hom_B(b',b'')$, let $t:\hom_B(a',b'')$, $e':P\,a'$, together with $w:\hom_B(a,a')$ and $f:\dhom^P_{u'u}(e,e')$ s.t. $t \circ w = (u'u) \circ v$. We find the ensuing filler over $v$ as indicated:

\[
\begin{tikzcd}
L(\pi) \ar[dddddd, two heads] &
e \ar[r, equal]
%e \ar[r, "\id_e"]
\ar[rr, bend left = 40, "f"] & e \ar[r, dashed, "f" swap] & e' \\
& & & \\
& a \ar[r, equal]
%& a \ar[r, "\id_a"]
\ar[rr, bend left = 40, "w"] \ar[d, "v" swap] & a \ar[d, "vu"] \ar[r, dashed, "w"] & a' \ar[d, "t"]\\
& b \ar[r, "u" swap]  \ar[rr, bend right = 40, "u'u" swap]  & b' \ar[r, dashed, "u'" swap] & b''
& & & \\
& & & \\
& & & \\
B & b \ar[r, "u" swap] \ar[rr, bend left = 40, "u'u"] & b' \ar[r, "u'" swap] & b'' \\
\end{tikzcd}
\]

By construction, the dashed arrows are unique up to homotopy.

For example, the free fibration of the identity $\id_B: B \fibarr B$ is the codomain opfibration $\partial_1: B^{\Delta^1} \fibarr B$ (cf. <cit.>).

We now demonstrate how the cocartesian replacement is in fact a “free” construction.[With categorical universes at hand, one would obtain statements more closely resembling <cit.>, <cit.>, and <cit.>.] We take as the “unit map”

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

the “inclusion”

\[ \iota\defeq \lambda b,e.\pair{\id_b}{e}:\prod_{b:B} P\,b \to (LP)\,b,\]

known from <ref>.

For a Rezk type $B$, consider an isoinner fibration $\pi:E \to B$, and a cocartesian fibration $\xi:F \to B$. Then the map

\[ \CocartFun_{B}(L(\pi),\xi) \stackrel{\Phi \defeq -\circ \iota_P}{\longrightarrow} \Fun_B(\pi,\xi)\]

is an equivalence of types.

We aim to give a quasi-inverse of the precomposition map. Let

\[ \Psi \defeq \lambda \varphi.\varphi': \Fun_B(\pi, \xi) \to \CocartFun_{B}(L(\pi),\xi)\]

\[ \varphi'_b(v,e) \defeq v_!^Q(\varphi_a \,e),\]

for $v:a \to b$, $e:P\,a$.
First, we are to show that this operation is really valued in cocartesian functors.
For this, we have to show that, for any $v:a \to b$, $e:P\,a$, the arrow

\[ \lambda t.(u(t) \circ v)_!^Q(\varphi_b \,e) : v_!Q(\varphi_b\,e) \longrightarrow^P_u (uv)_!^Q(\varphi_b\,a)\]

is $Q$-cocartesian. To that end, we observe the following. Let $a:B$, $d:Q\,a$ be fixed. Consider the maps $\cst(d), \tau_Q(-,d): \comma{a}{B} \to E$ defined by

\[ \cst(d)(v:a \to b) \defeq  d, \quad \tau_Q(-,d)(v:a \to b) \defeq v^Q_!(d):d . \]

We define the natural transformation

\[ Q_!(-,d):\nat{\comma{\pi}{B}}{E}(\cst(d),\tau_Q(-,d)), \quad Q_!(-,d)(v:a \to b) \defeq Q_!(v,d) : d \cocartarr_v v^Q_!(d).\]

Morphisms in $\comma{a}{B}$ are given by commutative triangles $u:v \to w$, so for fixed $v$ the type of morphisms in $\comma{a}{B}$ starting at $v$ is equivalent to the type $\comma{(\partial_1 \, v)}{B}$. Hence, any morphism in $\comma{a}{B}$ can be taken to be of the form $u:v \to uv$, for $v:a \to b$, $u:b \to b'$. The naturality squares of $Q_!(-,d)$ thus are of the following form:

\[\begin{tikzcd}
d && d \\
{v_!^Q(d)} && {(uv)_!^Q(d)} \\
a && a \\
b && {b'}
\arrow[Rightarrow, no head, from=3-1, to=3-3]
\arrow["u"', from=3-1, to=4-1]
\arrow["v"', from=4-1, to=4-3]
\arrow["vu", from=3-3, to=4-3]
\arrow[from=1-1, to=2-1, cocart]
\arrow["{(u:v \to uv)^Q_!(d)}"', from=2-1, to=2-3]
\arrow[Rightarrow, no head, from=1-1, to=1-3]
\arrow[from=1-3, to=2-3, cocart]
\end{tikzcd}\]

Note that the lower vertical arrow is given by

\[ \lambda t.(u(t) \circ v)^Q_!(d) = (u:v \to uv)^Q_!(d).\]

By right cancelation, $(u:v \to uv)^Q_!(d)$ is cocartesian, and hence we have an identity of arrows:

\[\begin{tikzcd}
&& {(uv)_!^Q(d)} \\
{v^Q_!(d)} && {u^Q_!(v_!^Q(d))}
\arrow["{Q_!(u,v_!^Q(d))}", from=2-1, to=2-3, cocart, swap]
\arrow["{(u:v \to uv)^Q_!(d)}", from=2-1, to=1-3, cocart]
\arrow[Rightarrow, no head, from=1-3, to=2-3]
\end{tikzcd}\]

In the cocartesian replacement $\partial_1': \comma{\pi}{B} \fibarr B$, the cocartesian lift of $u:b \to b'$ w.r.t. $\angled{v:a \to b,e:P\,a}$ is given by $\angled{\id_a,u,\id_e}$. Now, by the previous discussion we have

\begin{align*}
\varphi'_u(\id_a,u,\id_e)  & = \lambda t.(u(t) \circ v)_!^Q(\varphi_a\,e) \\
& =  (u:v \to uv)^Q_!(\varphi_a\,e) \\
& = Q_!(u,v^Q_!(\varphi_a\,e)) \\
& = Q_!(u, \varphi'_a(v,e))
\end{align*}

which shows that $\varphi': L(\pi) \to_B \xi$ is a cocartesian functor, as desired.

We now turn to showing that precomposing with $\iota$ gives an equivalence

\[ \Fun_B(\pi, \xi) \simeq \CocartFun_{B}(L(\pi),\xi).\]

We define

\[ \Phi \defeq \lambda \psi. \iota^*\psi \defeq \lambda \psi.\psi \circ \iota : \Fun_B(\pi, \xi) \to \CocartFun_{B}(L(\pi),\xi),\]

and recall that in the converse direction

\[ \Psi \defeq \lambda \varphi. \varphi' : \CocartFun_{B}(L(\pi),\xi) \to  \Fun_B(\pi, \xi)\]

with $\varphi'_b(v,e) \defeq v_!^Q(\varphi_a\,e)$.
Let $\psi: L\,E \to_B F$ be a cocartesian functor.
We compute

\[ (\iota^*\psi)_b'(v,e) = v_!^Q(\iota^*\psi_a(e)) = v_!^Q(\psi_a(\id_a,e)).\]

Since $\psi$ is cocartesian, we have $v_!^Q(\psi_a(\id_a,e)) = \psi_b(v_!^{LP}(\id_a,e))$, cf. <ref>. Now, the $LP$-cocartesian lift of $v:a \to b$ w.r.t. $\pair{\id_a}{e}$ is given by $\angled{\id_a, v,\id_e}: \pair{\id_a}{e} \to \pair{v}{e}$:

\[\begin{tikzcd}
e && e \\
a && a \\
a && b \\
a && b
\arrow[Rightarrow, no head, from=1-1, to=1-3]
\arrow[Rightarrow, no head, from=2-1, to=3-1]
\arrow["v"', from=3-1, to=3-3]
\arrow[Rightarrow, no head, from=2-1, to=2-3]
\arrow["v", from=2-3, to=3-3]
\arrow["v", from=4-1, to=4-3]
\end{tikzcd}\]

As a dependent arrow in $LP$, the codomain of this morphism is the pair $\pair{v}{e}$. In sum, this means

\[ v_!^Q(\psi_a(\id_a,e)) = \psi_b(v_!^{LP}(\id_a,e)) = \psi_b(v,e) = (\iota^*\psi)_b'(v,e),\]

, $\Psi(\Phi(\psi))$.
On the other hand, for an arbitrary fiberwise map $\varphi$ from $P$ to $Q$, we find that

\[ (\iota^* \varphi)'(b,e)= \varphi_b'(\id_b,e) = (\id_b)_!^Q(\varphi_b\,e) = \varphi_b(e)\]

since cocartesian lifts of identities are themselves identities. This gives an identification $\Phi(\Psi(\varphi))= \varphi$.

In fact, there also exists a discrete version of co-/cartesian replacement, cf. e.g. <cit.>. In type theory, this construction demands some more involvement, since it will include fiberwise localization.

§.§ Cocartesian functors

Cocartesian functors are an approproiate notion of morphism between cocartesian fibrations (not necessarily over the same base). They are defined as fiberwise maps that preserve cocartesian morphisms. We discuss several closure properties of cocartesian functors coming from $\infty$-cosmos theory. We also transfer the alternative characterizations of cocartesian functors from <cit.>, reworking the necessary tools from formal category theory in <ref>.

§.§.§ Morphisms of sections

We commence this section with a brief discussion of morphisms between sections. This willl turn out to be particularly important in the context of the Yoneda Lemma in <ref>.

First, let $B$ be any type and $P: B \to \UU$ any family. For any morphism $u:\hom_A(a,b)$, $a,b:A$, there is an induced dependent morphism

\[ \sigma\, u: \dhom^P_u(\sigma \,a, \sigma \, b), \quad \sigma \,u: \jdeq \lambda t.\sigma(u(t)). \]

Consider sections $\sigma,\tau :\prod_B P$ and a morphism $\kappa : \hom_{\prod_B P}(\sigma, \tau)$. Again, we imagine $\kappa$ as a kind of $2$-cell, and abbreviate $\hom_{\prod_B P}(\sigma, \tau) \defeq (\sigma \Rightarrow \tau)$.

For any $x:A$, $\kappa$ induces a vertical morphism

\[ \kappa x :\hom_{P\,x}(\sigma \, x, \tau \, x), \quad \kappa x : \jdeq \lambda t.\kappa(t,x). \]

By the axiom of choice, we have

\[ (\Delta^1 \to \prod_B P ) \equiv \sum_{u:\Delta^1 \to B} (\Delta^1 \to P(u)). \]

Let $B$ is a Rezk type and $P: B \to \UU$ an isoinner family. Then $\kappa$ acts on arrows in the base $B$ in the sense that in $\prod_B P$ there are canonical squares

\[
\begin{tikzcd}
\sigma a \ar[d, "\kappa a" swap] \ar[r, "\sigma u"] & \sigma b \ar[d, "\kappa b"] \\
\tau a \ar[r, "\tau u" swap] & \tau b \\
a \ar[r, "u"] & b
\end{tikzcd}
\]

and these squares compose over composable morphisms.[But we will not discuss the validity of the Segal condition for $\Pi$-types here.]

§.§.§ Definition and basic properties

Let $P: B \to \UU$ and $Q: C \to \UU$ be families. A fiberwise map or fibered functor from $P$ to $Q$  is a pair of functions $\Phi \jdeq \pair{j}{\varphi}$, where

* $j: B \to C$,

* $\varphi : \prod_{b:B} (P\,b \to Q\,j(b))$.

We call $F$ an equivalence if $j$ and $\varphi$ are equivalences.

We write $\FibFun_{B,C}(P,Q) \jdeq (P \xbigtoto[]{}  Q) \jdeq (\pi_P \xbigtoto[]{} \pi_Q)$ for the ensuing type of fiberwise maps. In the case of $B \jdeq C$, we denote this type as $\FibFun_{B}(P,Q) = (P \to_B Q) = (\pi_P \to_B \pi_Q)$.

Note that (by fibrant replacement) the type of commutative squares is equivalent to the type of maps between families.

Observe that given a map between families $P$ and $Q$ as above we get a strictly commutative square:

\[\begin{tikzcd}
{\widetilde{P}} && {\widetilde{Q}} \\
B && C
\arrow["{\pi_P}"', from=1-1, to=2-1]
\arrow["j"', from=2-1, to=2-3]
\arrow["{\mathrm{total}(\varphi)}", from=1-1, to=1-3]
\arrow["{\pi_Q}", from=1-3, to=2-3]
\end{tikzcd}\]

For any $u:\hom_B(a,b)$, the fiberwise map $\Phi$ acts on arrows over $u$ in the following way. For $f:\dhom^P_u(d,e)$, $d:Pa$, $e:Pb$, we have

\[ \varphi_u(f):\jdeq \lambda t.\varphi_{u(t)}(f(t)) : \dhom^Q_{ju}(\varphi_a(d), \varphi_b(e)).\]

Let $P:B \to \UU$ and $Q:B \to \UU$ be cocartesian families over Rezk types. Given a fibered functor $\Phi \defeq \pair{j}{\varphi}$ from $P$ to $Q$, if

\[ \Phi = \total(\varphi): \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 functor:[This is a proposition because being a cocartesian arrow is a proposition in our usual setting.]

\[ \isCocartFun_{P,Q}(\Phi) :\jdeq \prod_{\pair{u}{f}:\Delta^1\to \widetilde{P}} \isCocartArr_u^P(f) \to \isCocartArr_{ju}^Q(\varphi f).\]

We define

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

For cocartesian families $P: B \to \UU$ to $Q: B \to \UU$ over a common base, we have

\[ \isCocartFun_{P,Q}(\varphi) \equiv \prod_{\substack{u:\Delta^1 \to B \\ f: (t:\Delta^1) \to P(u\,t)}} \isCocartArr^P_u(f) \to \isCocartArr^Q_u(\varphi f)\]

and write

\[  \CocartFun_{B}(P,Q) \simeq  \sum_{\varphi:P \to_B Q} \isCocartFun_{P,Q}(\varphi).\]

If the unstraightening of $P$ is an identity, $\Phi$ can be identified with its second component, which in turn is the same as a section of $Q$. In this case, if $\Phi$ is a cocartesian functor it is called a cocartesian section. For a section $\sigma:\prod_B P$, this condition amounts to

\[  \isCocartSect_P(\sigma) :\jdeq \prod_{\substack{u:\Delta^1 \to B}} \isCocartArr_{u}^P(\sigma \circ u). \]

We denote by

\[ \prod_B^{\mathrm{cocart}} P :\jdeq \sum_{\sigma:\prod_B P} \isCocartSect_P(\sigma)  \]

the subtype of cocartesian sections.

In general, cocartesian families can have non-cocartesian sections. This implies that fiberwise maps between cocartesian families are not automatically cocartesian. As an example, consider the map $\partial_0 : (\Delta^1)^{\Delta^1} \to \Delta^1$ which is equivalent to:

\[ \pi: \Delta^2 \to \Delta^1, \pi \,t :\jdeq \begin{cases}
0 & \text{if $t \jdeq 0$} \\
1 & \text{else}
\end{cases}\]

The inclusion of $\Delta^1$ into $\Lambda_1^2$ as the “long edge” $0 \to 2$ is a non-cocartesian section of $\pi$.

Let $B$ be a Rezk type, $P:B \to \UU$, $Q:C \to \UU$ cocartesian families, and $\Phi \jdeq \pair{j}{\varphi} : \CocartFun_{B,C}(P,Q)$ a cocartesian functor. Then $\Phi$ commutes with cocartesian lifts, , for any $u:\hom_B(a,b)$ there is an identification of arrows

\[ \varphi_{P_!(u,d)} =_{\Delta^1 \to (ju)^*Q} Q_!(ju,\varphi_ad) \]

and hence of endpoints

\[ \varphi_b(u_!^Pd) =_{Q(jb)} (ju)_!^Q(\varphi_ad). \]

In particular there is a homotopy commutative square:

\[
\begin{tikzcd}
Pa \ar[rr, "\varphi_a"] \ar[d, "\coliftptfammap{P}{u}" swap] & & Qa \ar[d, "\coliftptfammap{Q}{(ju)}"] \\
Pb \ar[rr, "\varphi_b" swap] && Qb
\end{tikzcd}
\]

For $u:\hom_B(a,b)$ and $d:P\,a$, consider the $P$-cocartesian lift $\coliftarr{P}{u}{d}:\dhom^P_u(d,\coliftptfam{P}{u}{d})$. Since $\varphi$ is a cocartesian functor the arrow $\varphi_u(\coliftarr{P}{u}{d}):\dhom^Q_{ju}(\varphi_ad,\varphi_b(\coliftptfam{P}{u}{d}))$ is $Q$-cocartesian.

On the other hand, $\coliftarr{Q}{ju}{\varphi_ad}:\dhom^Q_{ju}(\varphi_ad, \coliftptfam{Q}{ju}{\varphi_ad})$ is as well a $Q$-cocartesian lift of $ju$ with domain $\varphi_ad$, thus coincides with $\varphi_u(\coliftarr{P}{u}{d})$ up to a path, in particular this gives an identification $\varphi_b(\coliftptfam{P}{u}{d}) = \coliftptfam{Q}{ju}{\varphi_ad}$.

Consider a Rezk type $B$, cocartesian families $P,Q: B \to \UU$, and a cocartesian functor $\varphi:\CocartFun_{B}(P,Q)$. Then $\varphi$ commutes with the actions of arrows, , for any $a,b:B$, $u:\hom_B(a,b)$, $d:P(a)$, we get an

\[ \varphi_b(\coliftptfam{P}{u}{d}) =_{Qb} \coliftptfam{Q}{u}{\varphi_a(d)},\]

thus a homotopy commutative square:

\[
\begin{tikzcd}
Pa \ar[rr, "\varphi_a"] \ar[d, "\coliftptfammap{P}{u}" swap] & & Qa \ar[d, "\coliftptfammap{Q}{u}"] \\
Pb \ar[rr, "\varphi_b" swap] && Qb
\end{tikzcd}
\]

§.§.§ Closure properties of cocartesian functors

The closure properties stated in this section are to be understood w.r.t. the (non-full) sub-$\inftyone$-category of the $\inftyone$-category of arrows which has as objects cocartesian fibrations $E\tofib B$ and as arrows cocartesian functors between those. In the absence of categorical universes, we capture the proclaimed limits and cotensors by spelling out type-theoretically their universal properties.

We start by explaining horizontal and vertical composition of cocartesian functors, alluding to the fact that in the model cocartesian fibrations form an $\inftytwo$-double category.

In the following, for a fibered functor $\varphi$, we often write $\widetilde{\varphi}$ for its totalization.

* Cocartesian functors compose horizontally: Suppose, we are given cocartesian families $P: A \to \UU$, $Q: B \to \UU$, $R: C \to \UU$ over Rezk types $A,B,C$. If $\Phi \jdeq \pair{j}{\varphi}:\CocartFun_{A,B}(P,Q)$, $\Psi \jdeq \pair{k}{\psi}:\CocartFun_{B,C}(\xi,\chi)$ are cocartesian functors, then the horizontal composite $\Psi \hcomp \Phi :\jdeq \pair{k \circ j}{\psi \circ \varphi}$ defines a cocartesian functor from $P$ to $R$:

\[\begin{tikzcd}
{\widetilde{P}} & {\widetilde{F}} & {\widetilde{G}} \\
{A} & {B} & {C}
\arrow["{\widetilde{\varphi}}", from=1-1, to=1-2]
\arrow["{\xi}", from=1-2, to=2-2, two heads]
\arrow["{\widetilde{\psi}}", from=1-2, to=1-3]
\arrow["{\chi}", from=1-3, to=2-3, two heads]
\arrow["{\pi}"', from=1-1, to=2-1, two heads]
\arrow["{j}"', from=2-1, to=2-2]
\arrow["{k}"', from=2-2, to=2-3]
\arrow["{\widetilde{\psi} \circ \widetilde{\varphi}}", from=1-1, to=1-3, curve={height=-24pt}]
\arrow["{k \circ j}"', from=2-1, to=2-3, curve={height=24pt}]
\end{tikzcd}\]

* Cocartesian functors compose vertically: Suppose, we are given cocartesian families $P: B \to \UU$, $P': \widetilde{P} \to \UU$, $Q: A \to \UU$, $Q': \widetilde{Q} \to \UU$, over Rezk types $A$ and $B$. If $\Phi \jdeq \pair{j}{\varphi}:\CocartFun_{B,A}(P,Q)$, $\Psi \jdeq \pair{\widetilde{\varphi}}{\psi}:\CocartFun_{B,A}(P',Q')$ are cocartesian functors, then the vertical composite $\Phi \vcomp \Psi :\jdeq \pair{j}{\psi}$ defines a cocartesian functor from $R\defeq \Sigma_{P}Q$ to $R':\jdeq \Sigma_{P'}Q'$:[We have $\Sigma_P Q \jdeq Q \compfam P$.]

\[\begin{tikzcd}
{\widetilde{Q}} & {\widetilde{Q'}} \\
{\widetilde{P}} & {\widetilde{P'}} \\
{B} & {A}
\arrow["{\widetilde{\psi}}", from=1-1, to=1-2]
\arrow["{\xi}"', from=1-1, to=2-1, two heads]
\arrow["{\xi'}", from=1-2, to=2-2, two heads]
\arrow["{\widetilde{\varphi}}"', from=2-1, to=2-2]
\arrow["{\pi}"', from=2-1, to=3-1, two heads]
\arrow["{j}"', from=3-1, to=3-2]
\arrow["{\pi'}", from=2-2, to=3-2, two heads]
\arrow["{\pi \circ \xi}" description, from=1-1, to=3-1, curve={height=24pt}, two heads]
\arrow["{\pi' \circ \xi'}" description, from=1-2, to=3-2, curve={height=-24pt}, two heads]
\end{tikzcd}\]

Recall <ref> for the closure properties of cocartesian fibrations, and how to compute cocartesian lifts in the respective constructions.

* Fiberwise composition of the fiberwise maps $\varphi:\prod_{a:A} P\,a \to Q\,ja$, $\psi:\prod_{b:B} Q\,b \to R\,kb$ is given by

\begin{align}
\psi \circ \varphi :\jdeq \lambda a.\psi_{ja} \circ \varphi_a:\prod_{a:A} P\,a \to R\,kja \label{eq:fibw-comp}.
\end{align}

Since $\varphi$ and $\psi$ both are cocartesian functors, for arrows $u:a \to a'$ in $A$, $v:b \to b'$ in $B$, and points $e:P\,a$, $d:Q\,b$, there are paths:

\begin{align}
\varphi_u(P_!(u,e)) & = Q_!(ju, \varphi_a e) \label{eq:phi-hor-cocart} \\
\psi_v(Q_!(v,d)) & = R_!(kv,\psi_b d) \label{eq:psi-hor-cocart}
\end{align}

Using these identifications, we find

\begin{align*}
(\psi \circ \varphi)_u(P_!(u,e)) & \stackrel{\ref{eq:fibw-comp}}{=}  \psi_{ju}(\varphi_u(P_!(u,e))) \stackrel{\ref{eq:phi-hor-cocart}}{=} \psi_{ju}(Q_!(ju,\varphi_a e)) \\
\stackrel{\ref{eq:psi-hor-cocart}}{=}  R_!(kju,\psi_{kja}(\varphi_a e)) &  \stackrel{\ref{eq:fibw-comp}}{=} R_!(kju, (\psi \circ \varphi)(a)).
\end{align*}

* Let $u:b \to b'$ in $B$, $u':a \to a'$ in $A$, be arrows with points $e:P\,b$, $\pair{e}{d}:Q(b,e)$, and $e':P\,b'$. First, recall that lifts in the composite families are given by:

\begin{align}
R_!(u,e,d) & = Q_!(P_!(u,e),d) \label{eq:comp-lifts} \\
R'_!(u',e',d') & = Q'_!(P'_!(u',e'),d') \label{eq:comp'-lifts}
\end{align}

Since $\varphi$ and $\psi$ are cocartesian functors, there are identifications:

\begin{align}
\varphi(P_!(u,e)) & = P_!'(ju, \varphi_b(e)) \label{eq:phi-vert-cocart} \\
\psi(Q_!(u,f,e,d)) & =  Q_!'(ju, \varphi_u(f), \varphi_b(e), \psi_{\varphi_b(e)}(d)) \label{eq:psi-vert-cocart}
\end{align}

This gives a path

\begin{align*}
\psi(R_!(u,e,d)) & \stackrel{\ref{eq:comp-lifts}}{=} \psi(Q_!(P_!(u,e),e,d)) \stackrel{\ref{eq:psi-vert-cocart}}{=}Q'_!(ju, \varphi_uP_!(u,e),\varphi_b e, \psi_{\varphi_b e} d) \\
\stackrel{\ref{eq:phi-vert-cocart}}{=}  Q'_!(ju,P_!'(ju,\varphi_b e), \varphi_b e, \psi_{\varphi_b e} d) & \stackrel{\ref{eq:comp'-lifts}}{=} R_!'(ju, \varphi_b e, \psi_{\varphi_b e}d).
\end{align*}

Let $B:I \to \UU$ be a type family over an arbitrary type $I$, and $P_i: B_i \to \UU$ cocartesian families with total types $E_i\defeq \totalty{P_i}$. Then, for any $k:I$ the projections from the product fibration

\[\begin{tikzcd}
{\prod_i E_i} & {E_k} \\
{\prod_i B_i} & {B_k}
\arrow[two heads, from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow[from=2-1, to=2-2]
\arrow[two heads, from=1-2, to=2-2]
\end{tikzcd}\]

are cocartesian.

The projection maps are given by evaluation at $i$. From the description of the cocartesian arrows in <ref> it follows that this defines a cocartesian functor.

Let $I$ be a small type, $B:I \to \UU$ be a family, and $P: \prod_{i:I} B_i \to \UU$ a family such that for all $i:I$ the family $P_i: B_i \to \UU$ is a cocartesian family. We denote the associated projections by $\pi_i : E_i \fibarr B_i$.

Then the product fibration $\prod_i E_i \tofib  \prod_i B_i$ satisfies the following universal property: For any cocartesian family $Q: A \to \UU$, with associated projection $\xi:F \fibarr A$, given a family of cocartesian functors $\pair{\alpha_k}{\psi_k}: \xi \xbigtoto[]{} \pi_k$ for $k:I$, there exists a unique cocartesian functor, the target tupling $\pair{(\alpha_i)_{i:I}}{(\psi_i)_{I:I}} : \xi \xbigtoto[]{} \prod_{i:I} \pi_i$ s.t. that every diagram of the form

\[\begin{tikzcd}
{F} && {E_k} \\
{A} & {\prod_i E_i} & {B_k} \\
& {\prod_i B_i}
\arrow["{\psi_k}", from=1-1, to=1-3]
\arrow[two heads, from=2-2, to=3-2]
\arrow["\xi"', two heads, from=1-1, to=2-1]
\arrow["{(\alpha_i)_{i:I}}"{description}, dashed, from=2-1, to=3-2]
\arrow["{\mathrm{ev}_k}"{description}, from=2-2, to=1-3]
\arrow["{\mathrm{ev}_k}"{description}, from=3-2, to=2-3]
\arrow["{(\psi_i)_{i:I}}"{description}, dashed, from=1-1, to=2-2]
\arrow["{\pi_k}", two heads, from=1-3, to=2-3]
\arrow[no head, from=2-1, to=2-2]
\arrow["{\alpha_k}", from=2-2, to=2-3]
\end{tikzcd}\]

We only discuss cocartesianness of the square given by $\pair{(\alpha_i)_{i:I}}{(\psi_i)_{i:I}}$. But this is again clear, because cocartesian lifts in the product fibration are defined pointwisely.

Let $P: B \to \UU$ be a cocartesian family with projection $\pi:E \tofib B$. For any map $k:A \to B$, the pullback square

\[\begin{tikzcd}
{k^*E} && E \\
A && B
\arrow["{k^*\pi}"', two heads, from=1-1, to=2-1]
\arrow["\varphi", from=1-1, to=1-3]
\arrow["k"', from=2-1, to=2-3]
\arrow["\pi", 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}\]

is a cocartesian functor.

The square acts as

\[ \pair{k}{\varphi}(v,d) = \pair{kv}{d}.\]

By <ref>, the pullback map $k^*\pi: k^*E \to A$ is a cocartesian fibration,

We abbreviate $Q\defeq k^*P$. Let $v:a \to a'$ in $A$ be an arrow and $d:k^*P(a) \jdeq P(ka)$ a point in the fiber. Again by <ref>, the $Q$-cocartesian lift is given by

\[ Q_!(v,d) = P_!(kv,d).\]

This leads to

\[
\varphi(v,Q_!(v,d)) = \pair{kv}{Q_!(v,d)} = \pair{kv}{P_!(kv,d)} = \pair{kv}{P_!(kv,\varphi d)}.\qedhere
\]

Let $P:B \to \UU$, $P':B' \to \UU$, and $P'':B'' \to \UU$ be cocartesian families with associated projection maps $\pi :E \to B$, $\pi':E' \to B'$, and $\pi'':E'' \to B''$, resp.

Consider a commutative cubical diagram as below, where the given vertical maps are cocartesian fibrations and the front and right square are cocartesian functors:

\[\begin{tikzcd}
{E' \times_E E''} &&& {E''} \\
& {E'} &&& E \\
{B' \times_B B''} &&& {B''} \\
& {B'} &&& B
\arrow["{\pi'\times_\pi \pi''}"{description}, dashed, two heads, from=1-1, to=3-1]
\arrow[from=1-1, to=1-4]
\arrow[from=1-1, to=2-2]
\arrow["\pi"{description, pos=0.3}, from=2-5, to=4-5, two heads]
\arrow["{\beta''}"{description}, from=3-4, to=4-5]
\arrow["{\varphi''}"{description}, from=1-4, to=2-5]
\arrow["{\beta'}"{description}, from=4-2, to=4-5]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=3-1, to=4-5]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-1, to=2-5]
\arrow["{\pi''}"{description, pos=0.2}, from=1-4, to=3-4, two heads]
\arrow[from=3-1, to=4-2]
\arrow[from=3-1, to=3-4]
\arrow["{\varphi'}"{description}, from=2-2, to=2-5, crossing over]
\arrow["{\pi'}"{description, pos=0.3}, from=2-2, to=4-2, crossing over, two heads]
\end{tikzcd}\]

Then the mediating map

\[ \pi''':\jdeq \pi' \times_\pi \pi'' : E''': \jdeq E' \times_E E'' \to B' \times_{B} B'' \jdeq : B'''\]

is a cocartesian fibration. Furthermore, the back and the left square are cocartesian functors.

Specifically, the cocartesian lift of an arrow $u''':\jdeq \langle u,u',u''\rangle$ w.r.t. $\langle e,e',e'' \rangle$ is given by

\[ \langle  P_!(u,e), P_!(u',e'), P_!(u'',e''). \rangle \]

Denote by $Q',Q'':B \to \UU$ the families associated to the maps $\beta'$ and $\beta''$, respectively.
The map in question is equivalent to ( <cit.>) the following projection:

\[\begin{tikzcd}
E''':\jdeq \sum_{b''':B'''} P'\,b' \times_{P\,b} P''\,b'' \ar[rr,two heads, "\pi'''"] && B'''\equiv \sum_{b:B} Q' \,b \times_{Q\,b} Q''\,b
\end{tikzcd}\]

The candidate $\pi'''$-cocartesian lift of $\angled{u,u',u''}$ w.r.t. $\angled{e:P(u0),e':P'(u'0),e'':P''(u''0)}$ is given by

\[ \angled{P_!(u,e), P_!'(u',e'), P_!''(u'',e'')},\]

and since the universal property is satisfied fiberwisely it is satisfied in the pullback fibration.

Given a commutative cube of cocartesian fibrations

\[\begin{tikzcd}
F &&& {E''} \\
& {E'} &&& E \\
A &&& {B''} \\
& {B'} &&& B
\arrow["\xi"{description}, two heads, from=1-1, to=3-1]
\arrow["{\alpha''}", from=3-1, to=3-4]
\arrow["{\psi''}", from=1-1, to=1-4]
\arrow["{\pi''}"{description, pos=0.2}, two heads, from=1-4, to=3-4]
\arrow["{\psi'}", from=1-1, to=2-2]
\arrow["{\pi'}"{description, pos=0.3}, two heads, from=2-2, to=4-2]
\arrow["\pi"{description, pos=0.3}, two heads, from=2-5, to=4-5]
\arrow["{\alpha'}", from=3-1, to=4-2]
\arrow["{\beta''}"{description}, from=3-4, to=4-5]
\arrow["{\varphi''}"{description}, from=1-4, to=2-5]
\arrow["{\beta'}"{description}, from=4-2, to=4-5]
\arrow["{\varphi'}"{description}, from=2-2, to=2-5, crossing over]
\arrow["{\pi'}"{description, pos=0.3}, two heads, from=2-2, to=4-2, crossing over]
\end{tikzcd}\]

where the vertical faces are cocartesian functors, there exists up to homotopy a unique cocartesian functor $\pair{\alpha'''}{\psi'''}:\xi \xbigtoto[]{} \pi'''$ s.t. the diagram

\[\begin{tikzcd}
F && {E'''} &&& {E''} \\
&&& {E'} &&& E \\
A && {B'''} &&& {B''} \\
&&& {B'} &&& B
\arrow[from=1-3, to=1-6]
\arrow["{\pi''}"{description}, two heads, from=1-6, to=3-6, near start]
\arrow[from=3-3, to=3-6]
\arrow[from=1-3, to=2-4]
\arrow["{\varphi''}", from=1-6, to=2-7, description]
\arrow["{\beta'}"{description}, from=4-4, to=4-7]
\arrow["\pi"{description}, two heads, from=2-7, to=4-7, near start]
\arrow[from=3-3, to=4-4]
\arrow["{\beta''}"{description}, from=3-6, to=4-7]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=3-3, to=4-7]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-3, to=2-7]
\arrow["\xi"', two heads, from=1-1, to=3-1, description]
\arrow["{\alpha'''}"{description}, dashed, from=3-1, to=3-3, description]
\arrow["{\psi'''}"{description}, dashed, from=1-1, to=1-3]
\arrow["{\psi''}"{description}, curve={height=-22pt}, from=1-1, to=1-6]
\arrow["{\alpha'}"{description}, from=3-1, to=4-4]
\arrow["{\alpha''}"{description}, curve={height=-22pt}, from=3-1, to=3-6]
\arrow["{\varphi'}", from=2-4, to=2-7,crossing over, description]
\arrow["{\pi'}"{description}, two heads, from=2-4, to=4-4, very near start,crossing over]
\arrow["{\pi'''}"{description}, two heads, from=1-3, to=3-3, crossing over]
\arrow["{\psi'}"{description}, from=1-1, to=2-4, crossing over]
\end{tikzcd}\]

By fibrant replacement, we can take the whole diagram to commute strictly. This gives a cocartesian functor comprised of the dependent pair

\[ \alpha\defeq \beta' \circ \alpha' \jdeq \beta'' \circ \alpha'': A \to B, \quad \psi\defeq \varphi' \circ \psi' \jdeq \varphi'' \circ \psi'':F \to E. \]

Then $\alpha'''$ acts as the fiber product tupling $\angled{\alpha, \alpha', \alpha''}$, and likewise $\psi'''$ is given by $\angled{\psi, \psi', \psi''}$. Denote by $R:A \to \UU$ the family associated to the fibration $\xi:F \to A$. For an arrow $v:a \to a'$ in $A$ and a point $d:R\,a$, the $R$-cocartesian lift gets mapped to

\begin{align*}
\psi(R_!(v,d)) & = \angled{\psi(R_!(v,d)), \psi'(R'_!(v,d)), \psi''(R_!(v,d))} \\
& = \angled{P_!(\alpha v,\psi d), P_!'(\alpha'v,\psi'd), P_!''(\alpha''v, \psi''d)}  \tag{\text{$\alpha, \alpha', \alpha''$ cocart.~functors}} \\
& = P'''_!(\alpha \, v, \psi \,d ) \tag{\text{construction of lifts by \cref{prop:cocart-fun-pb}}},
\end{align*}

which establishes the claim.

Consider an inverse diagram of cocartesian fibrations as below where all of the connecting squares are cocartesian functors:

\[\begin{tikzcd}
& \ldots &&&& {E_\infty} \\
\cdots && {E_2} && {E_1} && {E_0} \\
& \ldots &&&& {B_\infty} \\
\cdots && {B_2} && {B_1} && {B_0}
\arrow["{\pi_\infty}"{description, pos=0.3}, dashed, from=1-6, to=3-6]
\arrow["{\pi_0}"{description, pos=0.3}, two heads, from=2-7, to=4-7]
\arrow["{f_0}"{description, pos=0.7}, from=4-5, to=4-7]
\arrow["{\varphi_0}"{description}, dashed, from=1-6, to=2-7]
\arrow["{\psi_0}"{description}, dashed, from=3-6, to=4-7]
\arrow["{f_1}"{description, pos=0.7}, from=4-3, to=4-5]
\arrow["{g_1}"{description, pos=0.7}, from=2-3, to=2-5]
\arrow["{g_2}"{description, pos=0.7}, from=2-1, to=2-3]
\arrow["{f_2}"{description, pos=0.7}, from=4-1, to=4-3]
\arrow["{\varphi_1}"{description}, dashed, from=1-6, to=2-5]
\arrow["{\varphi_2}"{description}, dashed, from=1-6, to=2-3]
\arrow["{\psi_2}"{description}, dashed, from=3-6, to=4-3]
\arrow["{\psi_1}"{description}, dashed, from=3-6, to=4-5]
\arrow["{\varphi_3}"{description}, curve={height=12pt}, dashed, from=1-6, to=2-1]
\arrow["{\psi_3}"{description}, curve={height=12pt}, dashed, from=3-6, to=4-1]
\arrow["{g_0}"{description, pos=0.7}, from=2-5, to=2-7, crossing over]
\arrow["{\pi_1}"{description, pos=0.3}, two heads, from=2-5, to=4-5, crossing over]
\arrow["{\pi_2}"{description, pos=0.3}, two heads, from=2-3, to=4-3, crossing over]
\end{tikzcd}\]

Then the induced map $\pi_\infty: E_\infty \to B_\infty$ between the limit types is a cocartesian fibration, and the projections give rise to cocartesian functors.

Note that we can present the limiting types as pullbacks in the following way: First, for the base types, we have

\[\begin{tikzcd}
{} & {\sum_{\beta:\prod_{n:\mathbb N} B_n} \prod_{k:\mathbb N} \beta_{n} = f_n(\beta_{n+1}) \equiv B_\infty} && {\prod_{n:\mathbb N} B_{2n}} \\
\\
{} & {\prod_{n:\mathbb N} B_{2n+1}} && {\prod_{n:\mathbb N} B_n}
\arrow[from=1-2, to=3-2]
\arrow[from=3-2, to=3-4]
\arrow[from=1-2, to=1-4]
\arrow[from=1-4, to=3-4]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=3-4]
\end{tikzcd}\]

\[
\prod_{n:\mathbb N} B_{2n}  \equiv \sum_{\beta:\prod_{n:\mathbb N} B_n} \prod_{k:\mathbb N}\beta_{2k+1} = f_{2k+1}(\beta_{2k+2}), \quad \text{and} \quad
\prod_{n:\mathbb N} B_{2n+1} \equiv \prod_{\beta:\prod_{n:\mathbb N} B_n} \prod_{k:\mathbb N}\beta_{2k} = f_{2k}(\beta_{2k+1}).
\]

Lying over, the limiting total type arises as

\[\begin{tikzcd}
{} & {\sum_{\langle \beta, \sigma \rangle:B_\infty} \sum_{\vartheta:\prod_{n:\mathbb N} P_n(\beta_n)}\prod_{k:\mathbb N} \vartheta_{n} =_{\sigma_n} g_n(\vartheta_{n+1}) \equiv E_\infty} && {\prod_{n:\mathbb N} E_{2n}} \\
\\
{} & {\prod_{n:\mathbb N} E_{2n+1}} && {\prod_{n:\mathbb N} E_n}
\arrow[from=1-2, to=3-2]
\arrow[from=3-2, to=3-4]
\arrow[from=1-2, to=1-4]
\arrow[from=1-4, to=3-4]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=3-4]
\end{tikzcd}\]

\begin{align*}
\prod_{n:\mathbb N} E_{2n}  & \equiv \sum_{\pair{\beta}{\sigma}:B_{2n}} \sum_{\vartheta:\prod_{n:\mathbb N} P_n(\beta_n)} \prod_{k:\mathbb N}\vartheta_{2k+1} =_{\sigma_{2k+1}} g_{2k+1}(\vartheta_{2k+2}) \\
\prod_{n:\mathbb N} E_{2n+1}  & \equiv \sum_{\pair{\beta}{\sigma}:B_{2n+1}} \sum_{\vartheta:\prod_{n:\mathbb N} P_n(\beta_n)} \prod_{k:\mathbb N}\vartheta_{2k} =_{\sigma_{2k}} g_{2k}(\vartheta_{2k+1})
\end{align*}

Since cocartesian fibrations are closed under composition by <ref> and dependent products by <ref>, and the induced maps are cocartesian functors by <ref> the diagram

\begin{equation}\label{cd:seqlim-pb}
\begin{tikzcd}
{E_\infty} & {} && {\prod_{n:\mathbb N} E_{2n}} \\
& {\prod_{n:\mathbb N} E_{2n+1}} & {} & {} & {\prod_{n:\mathbb N} E_n} \\
{B_\infty} &&& {\prod_{n:\mathbb N} B_{2n}} \\
& {\prod_{n:\mathbb N} B_{2n+1}} &&& {\prod_{n:\mathbb N} B_n}
\arrow[from=1-4, to=2-5]
\arrow["{\pi_\infty}"{description}, dashed, two heads, from=1-1, to=3-1]
\arrow[two heads, from=2-2, to=4-2]
\arrow[two heads, from=2-5, to=4-5]
\arrow[from=3-4, to=4-5]
\arrow[from=3-1, to=4-2]
\arrow[from=4-2, to=4-5]
\arrow[from=3-1, to=3-4]
\arrow[from=1-1, to=1-4]
\arrow[dashed, from=1-1, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=3-1, to=4-5]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=45}, draw=none, from=1-1, to=2-5]
\arrow[two heads, from=2-2, to=4-2, crossing over]
\arrow[from=1-4, to=3-4, crossing over]
\arrow[from=2-2, to=2-5, crossing over]
\end{tikzcd}
\end{equation}

shows that the induced map $\pi_\infty : E_\infty \to B_\infty$ is a cocartesian fibration, too, by <ref>.

Finally, coming back to the sequential limit of squares, it is clear that the mediating squares

\[\begin{tikzcd}
{E_\infty} && {E_k} \\
{B_\infty} && {B_k}
\arrow["{\pi_\infty}"', two heads, from=1-1, to=2-1]
\arrow["{\psi_k}"', from=2-1, to=2-3]
\arrow["{\varphi_k}", from=1-1, to=1-3]
\arrow["{\pi_k}", two heads, from=1-3, to=2-3]
\end{tikzcd}\]

consisting of evaluations are cocartesian functors.

Given an inverse diagram of cocartesian fibrations

\[\begin{tikzcd}
{E_{n+1}} && {E_n} \\
{B_{n+1}} && {B_n}
\arrow["{\pi_{n+1}}"', from=1-1, to=2-1, two heads]
\arrow["{g_n}", from=1-1, to=1-3]
\arrow["{f_n}"', from=2-1, to=2-3]
\arrow["{\pi_n}", from=1-3, to=2-3, two heads]
\end{tikzcd}\]

and a cone

\[\begin{tikzcd}
F && {E_{n+1}} && {E_n} \\
A && {B_{n+1}} && {B_n}
\arrow["{\pi_{n+1}}"', two heads, from=1-3, to=2-3]
\arrow["{g_n}", from=1-3, to=1-5]
\arrow["{f_n}"', from=2-3, to=2-5]
\arrow["{\pi_n}", two heads, from=1-5, to=2-5]
\arrow["\xi"', two heads, from=1-1, to=2-1]
\arrow["{\varphi_n}"{description}, curve={height=-24pt}, from=1-1, to=1-5]
\arrow["{k_n}"{description}, curve={height=24pt}, from=2-1, to=2-5]
\arrow["{\varphi_{n+1}}", from=1-1, to=1-3]
\arrow["{f_n}"', from=2-1, to=2-3]
\end{tikzcd}\]

lying above, there exists uniquely up to homotopy a cocartesian functor

\[\begin{tikzcd}
F && {E_\infty} \\
A && {B_\infty}
\arrow["\xi"', two heads, from=1-1, to=2-1]
\arrow["{\lim_{i:I} \varphi_i}", from=1-1, to=1-3]
\arrow["{\lim_{i:I} k_i}"', from=2-1, to=2-3]
\arrow["{\pi_\infty}", two heads, from=1-3, to=2-3]
\end{tikzcd}\]

together with homotopies as indicated in the following diagram:

\[\begin{tikzcd}
F && {E_{n+1}} && {E_n} \\
& {E_\infty} \\
A && {B_{n+1}} && {B_n} \\
& {B_\infty}
\arrow["{\varphi_{n+1}}"{description, pos=0.7}, from=1-1, to=1-3]
\arrow["{g_{n}}"{description}, from=1-3, to=1-5]
\arrow["\xi"{description}, two heads, from=1-1, to=3-1]
\arrow["{\pi_n}"{description}, two heads, from=1-5, to=3-5]
\arrow["{f_n}"{description}, from=3-3, to=3-5]
\arrow["{\lim_{i:I} \varphi_i}"{description}, dashed, from=1-1, to=2-2]
\arrow[from=2-2, to=1-3]
\arrow["{\lim_{i:I}k_i}"{description}, dashed, from=3-1, to=4-2]
\arrow[from=4-2, to=3-3]
\arrow[from=4-2, to=3-5]
\arrow["{\varphi_{n}}"{description, pos=0.7}, curve={height=-24pt}, from=1-1, to=1-5]
\arrow["{k_n}"{description, pos=0.7}, curve={height=-24pt}, from=3-1, to=3-5]
\arrow["{k_{n+1}}"{description, pos=0.7}, from=3-1, to=3-3]
\arrow["{\pi_{n+1}}"{description}, two heads, from=1-3, to=3-3, crossing over]
\arrow["{\pi_\infty}"{description, pos=0.7}, shift right=1, two heads, from=2-2, to=4-2,crossing over]
\arrow[from=2-2, to=1-5, crossing over]
\end{tikzcd}\]

The type of cones over a fixed inverse diagram of squares is equivalent to the type of cones over the ensuing cube (<ref>). Then the claim follows by <ref>.

For a type $I:\UU$, suppose there are families $A,B: I \to \UU$ with families of families $P,Q: \prod_{i:I} B_i \to \UU$ such that $P_i:B_i\to \UU$ and $Q_i:A_i \to \UU$ are cocartesian for each $i:I$. Then, writing $\xi_i: F_i \to A_i$ and $\pi_i: E_i \to B_i$, resp., for the associated projections, given a family of cocartesian functors

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

the square induced by taking the dependent product

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

is a cocartesian functor.

Recall that cocartesian lifts in the product families are computed pointwise. For an arrow $\sigma: \alpha \Rightarrow \alpha'$ of sections in $\prod_{i:I} A_i$ and a section $\vartheta:\prod_{i:I} \alpha^* P_i$ lying over we obtain

\begin{align*}
& \big( \prod_{i:I} \varphi_i\big) \big( (\prod_{i:I} \xi_i)_!(\sigma,\vartheta) \big) = \lambda i. \varphi_i(Q_i)_!(\sigma_i,\vartheta_i) \\
= & \lambda i.(P_i)_!(k_i \sigma_i, \varphi_i \vartheta_i)) = \big( \prod_{i:I} \pi_i\big)_!(\kappa \sigma, \varphi \vartheta ).\tag{\text{$\varphi$ cocart.}}
\end{align*}

Let $P:B \to \UU$ be a cocartesian family with associated projection $\pi:E \fibarr B$. For any type map or shape inclusion $j:Y \to X$, the maps $\pi^X$ and $\pi^Y$ are cocartesian families, and moreover the square

\[\begin{tikzcd}
{E^X} && {E^Y} \\
{B^X} && {B^Y}
\arrow["\pi^X", two heads, from=1-1, to=2-1]
\arrow["B^j", from=2-1, to=2-3, swap]
\arrow["E^j", from=1-1, to=1-3]
\arrow["\pi^Y",two heads, from=1-3, to=2-3]
\end{tikzcd}\]

is a cocartesian functor.

By <ref>, $P^X$ and $P^Y$ are cocartesian families with associated projections $\pi^X$ and $\pi^Y$, resp. Furthermore, said proposition tells us that cocartesian lifts in exponentials are computed pointwise. Invoking fibrant replacement and the axiom of choice, this gives the following.

Lifts in the cocartesian fibration

\[  E^Y \equiv \sum_{u:Y \to B} \prod_{y:Y} P(u(y)) \xfib{\pi^Y} B^Y \]

are given by

\[ (P^Y)_! \Big(\alpha:u\to u', f:\prod_Y u^*P \Big) :\jdeq \lambda y.P_!(\alpha_y:u_y \to u_y', f_y).\]

Lifts in the cocartesian fibration

\[ E^X \equiv \sum_{\substack{u:Y \to B \\ v: X \to B}} \sum_{f:\prod_Y u^*P} \sum_{g:\prod_X v^*P} j^*g=_p f \xfib{\pi^X} \sum_{\substack{u:Y \to B \\ v:X \to B}} j^*v=u \equiv B^X \]

“sitting above” are given by

\begin{align*} & (P_!)^X\Big(\alpha:u\to u', f:\prod_Y u^*P, \beta:v \to v', g:\prod_X v^*P, \varphi:j^*\beta=\alpha, r:j^*g =_{\varphi_0} f\Big) \\
:\jdeq & \left \langle P_!^Y(\alpha,f), \lambda x.P_!(\beta_x,g_x), \lambda y.P_!^2(\varphi_y, r_y) \right \rangle
\end{align*}

where the $2$-dimensional lift of $\varphi$ w.r.t. $r$ is constructed as follows:

\[\begin{tikzcd}
&&& {j^*g} && f \\
{E^Y} &&& \cdot && \cdot \\
&&& {j^*v} && u \\
{B^Y} &&& {j^*v'} && {u'}
\arrow[""{name=0, anchor=center, inner sep=0}, from=3-4, to=3-6,equals]
\arrow["{j^*\beta}"', from=3-4, to=4-4]
\arrow["\alpha", from=3-6, to=4-6]
\arrow[""{name=1, anchor=center, inner sep=0}, from=4-4, to=4-6]
\arrow["{(P^Y)_!(j^*\beta,j^*g)}"', from=1-4, to=2-4, cocart]
\arrow[""{name=2, anchor=center, inner sep=0}, dashed, from=2-4, to=2-6, equals]
\arrow[""{name=3, anchor=center, inner sep=0}, "r", from=1-4, to=1-6, equals]
\arrow["{(P^Y)_!(\alpha,f)}", from=1-6, to=2-6, cocart]
\arrow[two heads, from=2-1, to=4-1]
\arrow["\varphi"{description}, shorten <=4pt, shorten >=4pt, Rightarrow, from=0, to=1]
\arrow["{(P^Y)_!^2(\varphi,r)}"{description}, shorten <=4pt, shorten >=4pt, Rightarrow, dashed, from=3, to=2]
\end{tikzcd}\]

Since the functor $E^j$ maps tuples $\langle u,v,p,f,g, r \rangle$ in $E^X$ to pairs $\langle u,f \rangle$ in $E^Y$ one can readily verify that it is cocartesian, using the computations above.

Let $j: Y \to X$ be a type map or shape inclusion. Then, given cocartesian fibrations $\pi: E \fibarr B$, $\xi: F \fibarr A$, and a cocartesian functor

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

the square induced between the Leibniz cotensors

\[\begin{tikzcd}
{F^X} & {F^X\times_{E^X} E^Y} \\
{A^X} & {A^X\times_{B^X} B^Y}
\arrow["\xi^X", two heads, from=1-1, to=2-1, swap]
\arrow["j \cotens \psi", from=1-1, to=1-2]
\arrow["j \cotens k", from=2-1, to=2-2, swap]
\arrow["\xi^Y \times_{\pi^Y} \pi^X", two heads, from=1-2, to=2-2]
\end{tikzcd}\]

is a cocartesian functor.

This follows from using <ref> and then applying the universal property <ref>.

To sum up the results from <ref> and the ones above, our synthetic cocartesian families satisfy stability properties analogous to those of an $\infty$-cosmos,  <cit.>:

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.

C.f. the previous statements, as well as <ref>, and <ref>.

We end the section with yet another useful stability property.

Let $A,B$ be a Rezk type and $j:A \to B$ be a map.

We consider cocartesian families $P,P':B \to \UU$ and a cocartesian functor $\varphi:\CocartFun_B(P,P')$. Then the mediating map $\psi \jdeq \lambda a,e.\pair{ja}{e}:\CocartFun_A(j^*P,j^*P')$ is also a cocartesian functor.
We write $\pi:E \fibarr B$, $\pi':E' \fibarr B$ for the fibrations corresponding to $P$, $P'$, and similarly for the pullback fibrations:

\[\begin{tikzcd}
{F} && {E} \\
& {F'} && {E'} \\
& {A} && {B}
\arrow["{\xi'}", from=2-2, to=3-2, two heads]
\arrow["{\pi'}", from=2-4, to=3-4, two heads]
\arrow["{\widetilde{\psi}}"', swap, pos=0.8, from=1-1, to=2-2, dashed]
\arrow["{\xi}"', from=1-1, to=3-2, curve={height=6pt}, two heads]
\arrow["{\widetilde{\varphi}}", from=1-3, to=2-4]
\arrow["{\pi}"', from=1-3, to=3-4, curve={height=6pt}, two heads]
\arrow["\lrcorner"{very near start, rotate=0}, pos=0.125, from=2-2, to=3-4, shift right=2, phantom]
\arrow["\lrcorner"{very near start, rotate=0},pos=0.125, from=1-1, to=3-4, shift left=1, phantom]
\arrow["{j}"', from=3-2, to=3-4]
\arrow[from=2-2, to=2-4, crossing over]
\arrow[from=1-1, to=1-3, crossing over]
\end{tikzcd}\]

Let $v:a \to a'$ be an arrow in $A$, and $f:e \to_{jv} e'$ a dependent arrow in $P$. By definition, we have identifications:

\begin{align}
\psi_u(f) & = \varphi_{ju}(f) \label{eq:pb-fibw-f} \\
\psi_a(e) & = \varphi_{ja}(e) \label{eq:pb-fibw-e}
\end{align}

Since $\varphi$ is a cocartesian functor, there is a path

\begin{align}
\varphi_u(P_!(u,e)) = P_!'(u, \varphi_b e). \label{eq:pb-varphi-cocart} \\
\end{align}

The cocartesian lifts in the pullback family are given by

\begin{align}
Q_!'(v,e) = P_!'(jv,e). \label{eq:pb-lifts}
\end{align}

Taken together, this gives rise to an identification

\[
\psi_v(Q_!(v,e)) \stackrel{\ref{eq:pb-fibw-f}}{=} \varphi_{jv}(P_!(jv,e))   \stackrel{\ref{eq:pb-varphi-cocart}}{=} P_!'(jv,\varphi_{ja}(e))  \stackrel{\ref{eq:pb-fibw-e}, \ref{eq:pb-lifts}}{=} Q_!'(v,\psi_a e).\qedhere
\]

§.§.§ Characterizations of cocartesian functors

Let $A$ and $B$ be Rezk types, and consider cocartesian families $P:B \to \UU$ and $Q:A \to \UU$ with associated fibrations $\xi: F \fibarr  A$ and $\pi: E \fibarr B$, 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] & E \ar[d, "\pi"] \\
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 natural isomorphism, fibered over $j:A \to B$, 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 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}\]

$\ref{it:cocart-fun-cocart} \iff \ref{it:cocart-fun-mate-fibered}$: Consider the first (fibered) adjunction, where the mate of the canonical isomorphism cell is constructed through the following pasting diagram:

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

The unit $\eta: \hom_{\xi \downarrow A}(\id_F, \kappa i)$ at $\pair{u:a \to a'}{d:P_a}$ is given as follows:

\[\begin{tikzcd}
{d} && {u_!d} \\
{a} && {a'} \\
{a'} && {a'}
\arrow["{P_!(u,d)}", from=1-1, to=1-3]
\arrow["{u}"', from=2-1, to=3-1]
\arrow[from=3-1, to=3-3, no head, equals]
\arrow["{u}", from=2-1, to=2-3]
\arrow[from=2-3, to=3-3, no head, equals]
\end{tikzcd}\]

The pasting $2$-cell can be identified with the natural transformation

\[ \alpha: \hom_{F \to \pi \downarrow B}(\kappa' \circ \varphi \downarrow j, \varphi \circ \kappa) \]

whose components at $\pair{u:a\to a'}{d:Pa}$ are given by the fillers

\[ \alpha_{\pair{u}{d}}:\jdeq (\kappa' \circ \varphi \downarrow j)\eta_{\pair{u}{d}}: \pair{jd'}{(ju)_!(\varphi d)} \to \pair{jd'}{\varphi(u_!d)} \]

\[\begin{tikzcd}
&&&&&& {\varphi(u_!d)} \\
{d} && {u_!d} & {} & {\varphi(d)} && {(ju)_!(\varphi d)} \\
{a} && {a'} & {} & {j(a)} && {j(a')}
\arrow["{Q_!(u,d)}", from=2-1, to=2-3]
\arrow["{u}", from=3-1, to=3-3]
\arrow["{\rightsquigarrow}", from=2-4, to=3-4, phantom, no head]
\arrow["{j(u)}", from=3-5, to=3-7]
\arrow["{P_!(ju,\varphi d)}"', from=2-5, to=2-7, cocart]
\arrow["{\alpha_{\langle u,d \rangle}}"', from=2-7, to=1-7, dashed]
\arrow["{\varphi\big(P_!(u,d)\big)}", from=2-5, to=1-7]
\end{tikzcd}\]

If $\Phi \jdeq \pair{j}{\varphi}$ is a cocartesian functor there is an identification $\varphi(Q_!(u,d)) = P_!(ju, \varphi d)$ in $E^{\Delta^1}$, hence $\alpha_{\pair{u}{d}}$ is an identity.

On the other hand, if the induced filler $\alpha_{\pair{u}{d}}$ happens to be an isomorphism, and thus an identity, we obtain an identification $\varphi(Q_!(u,d)) = P_!(ju, \varphi d)$ rendering $\Phi$ a cocartesian functor.

$\ref{it:cocart-fun-cocart} \iff \ref{it:cocart-fun-mate}$: In case of the second adjunction, the mate is given by the cell constructed by pasting from the diagram:

\[\begin{tikzcd}
{\xi\downarrow A} & {F^{\Delta^1}} & {E^{\Delta^1}} \\
& {\xi\downarrow A} & {\varphi \downarrow B} & {E^{\Delta^1}}
\arrow["{\ell}", from=1-1, to=1-2]
\arrow["{r}"', from=1-2, to=2-2]
\arrow["{\varphi\downarrow j}"', from=2-2, to=2-3]
\arrow["{\varphi^{\Delta^1}}", from=1-2, to=1-3]
\arrow["{r'}"', from=1-3, to=2-3]
\arrow["{\ell'}"', from=2-3, to=2-4]
\arrow[""{name=0, inner sep=0}, from=1-1, to=2-2, no head, equals]
\arrow[""{name=1, inner sep=0}, from=1-3, to=2-4, no head, equals]
\arrow[Rightarrow, "{=}", from=2-2, to=1-3, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{=}", from=0, to=1-2, shorten <=2pt, shorten >=2pt]
\arrow[Rightarrow, "{\varepsilon'}", from=2-3, to=1, shorten <=1pt, shorten >=1pt]
\end{tikzcd}\]

The counit $\varepsilon':\hom_{E^{\Delta^1} \to E^{\Delta^1}}(\ell' \circ r', \id_{E^{\Delta^1}})$ at $\pair{v:b \to b'}{g:e \to e'}$ is given by the fillers:

\[\begin{tikzcd}
&& {e'} \\
{e} && {v_!e} \\
{b} && {b'}
\arrow["{v}"', from=3-1, to=3-3]
\arrow["{P_!(v,e)}"', cocart, from=2-1, to=2-3]
\arrow["{g}", from=2-1, to=1-3]
\arrow["{\varepsilon'_{\langle {v,g} \rangle}}"', from=2-3, to=1-3, dashed]
\end{tikzcd}\]

The pasting cell can be identified with the natural transformation

\[ \beta:\hom_{\xi \downarrow A \to F^{\Delta^1}}(\varphi \downarrow j \circ \ell', \varphi^{\Delta^1} \circ \ell)\]

whose components at $\pair{u:a\to a'}{d:Pa}$ are given by

\[ \beta_{\pair{u}{d}} \jdeq \varepsilon'_{\varphi^{\Delta^1}(\ell \pair{u}{d})}: \pair{ju}{P_!(ju,\varphi(d))} \to \pair{ju}{\varphi Q_!(u,d)},  \]

\[\begin{tikzcd}
&& {\varphi(u_!d)} \\
{\varphi d} && {(ju)_!(\varphi d)} \\
{ja} && {ja'}
\arrow["{ju}"', from=3-1, to=3-3]
\arrow["{P_!(ju,\varphi d)}"', cocart, from=2-1, to=2-3]
\arrow["{\varphi(Q_!(u,d))}", from=2-1, to=1-3]
\arrow["{\beta_{\langle {v,g} \rangle}}"', from=2-3, to=1-3, dashed]
\end{tikzcd}\]

If $\Phi \jdeq \pair{\varphi}{u}$ is a cocartesian functor, then $\varphi(Q_!(u,d))$ is a cocartesian arrow, so the filler $\beta_{\pair{v}{g}}$ must be too, thus an identity.

Conversely, $\beta_{\pair{v}{g}}$ being an identity gives rise to an identification $\varphi(Q_!(u,d)) =  P_!(ju,\varphi d)$. This implies that $\Phi$ is a cocartesian functor.

An application of the characterization theorem is a proof that any fibered left adjoint (over a common base) is a cocartesian functor.

Let $g:C \rightarrow A \leftarrow B : f$ be a cospan of Rezk types. For generalized elements $\alpha, \alpha':X \to f \downarrow g$, consider a natural transformation $\tau: \alpha \Rightarrow \alpha'$. If $\partial_k \tau$  for both $k=0,1$ are natural isomorphisms, then $\tau$ is a natural isomorphism.

We have an equivalence $X \to f \downarrow g \equiv \sum_{\substack{\alpha_0:X \to B \\ \alpha_1 : X \to C}} \prod_{x:X} f \alpha_0 x \to g \alpha_1 x$. The natural transformation $\tau$ at stage $x:X$ is given by a square:

\[\begin{tikzcd}
{f \alpha_0x} && {f \alpha'_0x} \\
{g \alpha_1x} && {g \alpha_1'x}
\arrow["{\alpha_x}"', from=1-1, to=2-1]
\arrow["{g(\partial_1\tau_x)}"', from=2-1, to=2-3]
\arrow["{f(\partial_0 \tau_x)}", from=1-1, to=1-3]
\arrow["{\alpha'_x}", from=1-3, to=2-3]
\arrow["{\tau_x}"{description}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

Invoking transformation extensionality, if both whiskered $2$-cells $\partial_k \tau_x$ are isomorphisms, then by functoriality the squares $\tau_x$ degenerate to

\[\begin{tikzcd}
\cdot && \cdot \\
\cdot && \cdot
\arrow["{\alpha_x}"', from=1-1, to=2-1]
\arrow[""{name=0, anchor=center, inner sep=0}, no head, from=1-1, to=1-3,equals]
\arrow[""{name=1, anchor=center, inner sep=0}, no head, from=2-1, to=2-3,equals]
\arrow["{\alpha'_x}", from=1-3, to=2-3]
\arrow["{\tau_x}"{description}, Rightarrow, draw=none, from=0, to=1]
\end{tikzcd}\]

exhibiting $\tau$ as a natural isomorphism.

Consider a fibered functor between cocartesian fibrations where the horizontal arrows make up a fibered adjunction:

\[\begin{tikzcd}
F && E & {} \\
\\
& B && {}
\arrow[""{name=0, anchor=center, inner sep=0}, "\psi"', curve={height=12pt}, from=1-3, to=1-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "\varphi"', curve={height=12pt}, from=1-1, to=1-3]
\arrow["\xi"', two heads, from=1-1, to=3-2]
\arrow["\pi", two heads, from=1-3, to=3-2]
\arrow["\dashv"{anchor=center, rotate=90}, draw=none, from=1, to=0]
\end{tikzcd}\]

Then $\varphi$ is a cocartesian functor.

Since $\xi$ and $\pi$ are cocartesian, we obtain the following induced diagram:

\[\begin{tikzcd}
{} & {F^{\Delta^1}} && {E^{\Delta^1}} \\
&& {} \\
{} & {\xi \downarrow B} && {\pi \downarrow B}
\arrow["{\varphi\downarrow k}"{name=0, swap}, from=3-2, to=3-4, curve={height=12pt}]
\arrow["{\psi \downarrow k}"{name=1, swap}, from=3-4, to=3-2, curve={height=12pt}]
\arrow["{r'}"{name=2, swap}, from=1-4, to=3-4]
\arrow["{\varphi^{\Delta^1}}"{name=3, swap}, from=1-2, to=1-4, curve={height=12pt}]
\arrow["{\psi^{\Delta^1}}"{name=4, swap}, from=1-4, to=1-2, curve={height=12pt}]
\arrow["{r}"{name=5}, from=1-2, to=3-2]
\arrow["{\ell}"{name=6}, from=3-2, to=1-2, curve={height=-18pt}]
\arrow["{\ell'}"{name=7, swap}, from=3-4, to=1-4, curve={height=18pt}]
\arrow[Rightarrow, "{=}" description, from=3-2, to=1-4, shorten <=8pt, shorten >=8pt]
\arrow["\dashv"{rotate=90}, from=0, to=1, phantom]
\arrow["\dashv"{rotate=90}, from=3, to=4, phantom]
\arrow["\dashv"{rotate=-1}, from=6, to=5, phantom]
\arrow["\dashv"{rotate=-179}, from=7, to=2, phantom]
\end{tikzcd}\]

Specifically, the vertical adjunctions follow from the Chevalley criterion for cocartesian fibrations. The top horizontal adjunction exists because of <ref>. The bottom horizontal adjunction exists by <ref>.
We now have to show that the the mate w.r.t. the vertical adjunctions is invertible, which by <ref> is equivalent to the mate w.r.t. the horizontal adjunctions being invertible. But this is established by $2$-cell conservativity of comma objects, cf. <ref>.

Any fibered equivalence between arbitrary maps is also cocartesian.

For (cocartesian) fibrations $\xi: F \fibarr A$ and $\pi:E \fibarr B$, any square of the form

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

is a cocartesian functor.

By univalence we can replace anonymous equivalences by identities (equivalence induction), and these are easily seen to be cocartesian functors (since they preserve cocartesian lifts).

Alternatively, in the case of cocartesian fibrations, one could argue similarly as in <ref>, cf. <cit.>

§ MORE ON COVARIANT FAMILIES

Covariant families have been introduced and thoroughly analyzed by Riehl–Shulman, cf. <cit.>. Since they can be characterized by a right orthogonality condition (namely  the map $0: \unit \hookrightarrow \Delta^1$), it follows formally that they satisfy all the closure properties from Subsection <ref>, yielding the analog of the $\infty$-cosmological closure properties <ref>. As a perhaps rather non-obvious result, we prove that covariant families (over an arbitrary type) are automatically inner. Furthermore, we prove the expected result that, over Rezk types a family is covariant if and only if its cocartesian and all its fibers are discrete. We also argue how covariant families can be seen as a type-theoretic analogue of discrete cocartesian fibrations in the $\infty$-cosmological sense.

The section concludes by establishing a directed version of the encode-decode method <cit.>, which we expect to be useful when analyzing localization or other higher inductive types in later work.

In the following section, the Yoneda Lemma for covariant families, originally established in <cit.>, is recovered in <ref> as a special case of the Yoneda Lemma for cocartesian families.

§.§ Properties and characterizations of covariant families

§.§.§ Covariant vs. inner families

Every covariant family is an inner family.

Since inner families are a relative version of Segal types the proposition at hand can be seen as a relative version of <cit.>.

Let $P : B \to \UU$ be a covariant family.
Suppose we are given a
$2$-simplex $\sigma$ in $B$ with boundary given by
$u:\hom_B(b,b')$, $v:\hom_B(b',b'')$, and $w:\hom_B(b,b'')$, for
$b,b',b'':B$, , $\sigma:\hom_B^2(u,v;w)$. Furthermore, assume
there are dependent arrows $f:\hom^P_u(e,e')$,
$g:\hom^{P}_v(e',e'')$ for $e:P\,b$, $e':P\,b'$, $e'':P\,b''$.

We prove that there is a contractible choice of elements of the
extension type

\begin{equation}\label{eq:cov-lift-type}
\ext[\Big]{\prod_{t_2\le t_1}P(\sigma(t_1,t_2))}{\Lambda^2_1}{[f,g]}
\end{equation}

by giving a center and by showing that any two elements are equal.

The center is obtained using the homotopy extension property (HEP),
cf. <cit.>, <ref>. Since $P$ is covariant, there is an element

\[
H : \prod_{b_1: B}\prod_{u_1:\hom_B(b,b_1)}
\isContr\ext[\Big]{\prod_{t}P(u_1(t))}{0}{e}.
\]

To use the HEP, we first give an element of
$\prod_{t_2\le t_1}P(\sigma(t_1,t_2))$. If $t_2$ is given, consider
$K(t_2) :\jdeq H\,\sigma(1,t_2)\,(\lambda t.\,\sigma(t,t\land
t_2))$. The corresponding center applied to $t_1$ is in
$P(\sigma(t_1,t_1\land t_2)) \jdeq P(\sigma(t_1,t_2))$. We now need
to provide a homotopy between this and $[f,g]$, but this is
obtained from the contraction part of $H$.

To show that any two elements $\tilde\sigma_1,\tilde\sigma_2$
in (<ref>) are equal, we use relative function
extensionality <cit.>, <ref>, by which it suffices to give
an element of the extension type

\[
\ext[\Big]{\prod_{t_2\le t_1}
\tilde\sigma_1(t_1,t_2) = \tilde\sigma_2(t_1,t_2)}{\Lambda^2_1}{\refl}
\]

Again we appeal to HEP. Given $t_2\le t_1$, from $K(t_2)$ we get an
identity between $\tilde\sigma_1$ and $\tilde\sigma_2$ restricted to
the extension type $\ext{\prod_t P(t,t\land t_2)}{0}{e}$. From the
easy direction of relative function extensionality we get an
identity $\tilde\sigma_1(t_1,t_2) = \tilde\sigma_2(t_1,t_2)$.
To show that the resulting homotopy is homotopic to $\refl$ on
$\Lambda^2_1$, we use tope disjunction elimination.

On the edge $t_2=0$ we have an identity $f=f$ in the contractible
type $\ext{\prod_tP(\sigma(t,0))}{0}{e}$. But an identity
type in a contractible type is itself contractible, so this identity
is equal to $\refl$.

On the edge $t_1=1$ we may consider an arbitrary $t_2$ and use the
same argument.

§.§.§ Covariant vs. cocartesian families

Any covariant family over a Rezk type $B$ is a cocartesian family.

A family $P:B \to \UU$ is covariant if and only if the Leibniz cotensor $i_0 \cotens \pi_P: \totalty{P}^{\Delta^1} \to B^{\Delta^1} \times_{B} \totalty{P}$ is an equivalence. By <ref> this also constitutes an equivalence, and by fibrant replacement the left adjoint can be chosen a (strict) section.

Let $B$ be a Segal type. Assume $P : B \to \UU$ is such that the following properties are satisfied:

* $P$ is an inner family.

* $P$ has the cocartesian lifting property.

* All fibers $P\,b$ for $b:B$ are discrete.

Then $P$ is covariant.

Let $b,b':B$ with $u:\hom_B(b,b')$, and $e:P\,b$. There is $e':P\,b'$ and a lift $f:\hom^P_u(e,e')$ which is cocartesian, meaning that for any $e'':P\,b'$ and $g:\hom^P_u(e,e'')$ there is a unique arrow $h:\hom^{P}_{\id_{b'}}(e',e'')$ such that $h \circ f = g$. This dependent composition becomes an ordinary composition in the total space $\totalty{P}$ which is Segal, since $B$ is. Now, as $\hom^{P}_{\id_{b'}}(e',e'') \equiv \hom_{P\,b'}(e',e'')$, and $P\,b'$ is discrete, $h$ can be taken to be an identity. But then $f = g$.

A cocartesian family over a Segal type is covariant if and only if all its fibers are discrete.

A cocartesian family is covariant if and only if all dependent arrows are cocartesian.

Let $P: B \to \UU$ be a cocartesian family.

If $P$ is covariant, then the unique lift for any $u:b \to b'$ in $B$  $e:P\,b$ must be (identifiable with) a cocartesian arrow. Since any dependent arrow is given as a lift of some arrow in the base, it follows that any dependent arrow is cocartesian.

Conversely, if every dependent arrow in $P$ is cocartesian, any two lifts of $u:b \to b'$ beginning at some $e:P\,b$ become equal (since the filler induced by the universal property is exhibited as an isomorphism).

§.§ Closure properties of covariant families

Over Rezk bases, it holds that:

Covariant families are closed under composition, dependent products, pullback along arbitrary maps, and cotensoring with maps/shape inclusions. Furthermore, they are closed under sequential limits, and satisfy left cancelation. Families corresponding to equivalences or terminal projections are always covariant.

Between covariant families over Rezk bases, it holds that:
Fibered 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 fibered functors], and Leibniz cotensors.

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

Most of the properties follow from the established results about cocartesian fibrations <ref>, or the additional closure properties that hold for right classes. Recall that fibered functors between covariant families are automatically cocartesian.
We are only left with stability under objectwise pullback (which will imply stability under objectwise sequential limits). But it is easy to see that given covariant fibrations

\[\begin{tikzcd}
& {} && {} \\
{E'\defeq \widetilde{P'}} & {} & {E \defeq \widetilde{P}} && {E'' \defeq \widetilde{P''}} \\
& {} \\
{B'} & {} & B && {B''}
\arrow[two heads, from=2-3, to=4-3]
\arrow[two heads, from=2-1, to=4-1]
\arrow[from=2-1, to=2-3]
\arrow[from=4-1, to=4-3]
\arrow[two heads, from=2-5, to=4-5]
\arrow[from=4-5, to=4-3]
\arrow[from=2-5, to=2-3]
\end{tikzcd}\]

in the objectwise pullback

\[ E' \times_E E'' \to B' \times_B B'' \]

a lift of $\angled{u,u', u''}$ w.r.t. $\angled{e_0,e'_0,e''_0}$ is given by

\[ \angled{P_!(u,e_0), P'_!(u',e_0'), P''_!(u'',e_0'')}.\]

Since due to covariance all the components each are uniquely determined (after projecting), the lift in $E' \times_E E'' \to B' \times_B B''$ is as well.

§.§ Covariant families as discrete objects

In $\infty$-cosmos theory, covariant families arise as a kind of discrete object, which we are able to capture in simplicial type theory as well.

More precisely, over a fixed base, a discrete cocartesian fibration in an $\infty$-cosmos is defined as a cocartesian fibration (relative to the given $\infty$-cosmos) that is required to be discrete as an object of the slice $\infty$-cosmos <cit.>. There are two equivalent ways of expressing the latter. In our current type-theoretic setting, in absence of categorical universes, we cannot give a systematic account of these definitions, but we can still give appropriate translations of both of these criteria, and prove they are satisfied by discrete covariant families.

To state these principles, we need to type-theoretically capture some of the structure of sliced $\infty$-cosmoses, namely sliced or relative versions of function types as well as simplicial cotensors.

For two maps $\pi:E\to B$, $\xi:F \to B$ over a common base type $B$, the relative function type (over $B$) is given by the pullback object:

\[\begin{tikzcd}
{\underline{\mathrm{Fun}}_B(\xi,\pi)} && {E^F} \\
{\unit} && {B^F}
\arrow[from=1-1, to=2-1]
\arrow["{\xi}"', from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\pi^F}", from=1-3, to=2-3]
\arrow["\lrcorner"{very near start, rotate=0}, from=1-1, to=2-3, phantom]
\end{tikzcd}\]

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

\[\begin{tikzcd}
{X \boxtimes E} && {E^X} \\
{B} && {B^X}
\arrow[from=1-1, to=2-1]
\arrow["{\mathrm{cst}}"', from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["{\pi^X}", from=1-3, to=2-3]
\arrow["\lrcorner"{very near start, rotate=0}, from=1-1, to=2-3, phantom]
\end{tikzcd}\]

If $X$ is a shape $\Phi$, we can take the strict extension type

\[\begin{tikzcd}
{\Phi\boxtimes E} && {\sum_{b:B} \Phi \to P\,b} \\
& {B}
\arrow[from=1-1, to=2-2, two heads]
\arrow["{\equiv}", from=1-1, to=1-3]
\arrow[from=1-3, to=2-2, two heads]
\end{tikzcd}\]

where $P:B \to \UU$ denotes the family of fibers of $\pi$.

Over a Rezk type, for a cocartesian family $P:B \to \UU$ with associated projection $\pi:E \to B$ the following are equivalent:

*  The map $\pi$ is $i_0$-orthogonal.

*  The map induced by the canonical inclusion $\Delta^1 \hookrightarrow \walkBinv$ is a fibered equivalence:

\[\begin{tikzcd}
{\mathbb E \boxtimes E} && {\Delta^1 \boxtimes E} \\
& {B}
\arrow["{\equiv}", from=1-1, to=1-3]
\arrow[from=1-1, to=2-2, two heads]
\arrow[from=1-3, to=2-2, two heads]
\end{tikzcd}\]

*  For all global elements $b:\unit \to B$, the relative function type $\ifun(b,\pi)$ is discrete.

Furthermore, if $P:B \to \UU$ is a covariant family, then, for any map $\xi: F \to B$, the relative function type $\ifun(\xi,\pi)$ is discrete.

$\ref{it:disc-orth} \iff \ref{it:disc-shape}$: Criterion $\ref{it:disc-shape}$ is equivalent to $\prod_{b:B} \isEquiv((\walkBinv \to P\,b) \to (\Delta^1 \to P\,b))$, which precisely says that all fibers of $P$ are discrete. Given that $P$ is cocartesian, this is equivalent to $P$ being covariant by <ref>.

$\ref{it:disc-orth} \iff \ref{it:disc-shape}$: Similarly, since $\ifun(b,\pi) \equiv P\,b$, Criterion $\ref{it:disc-fun}$ is also equivalent to $P$ being covariant.

Now, assume $P$ is covariant. Given a map $\xi:F \to B$, the exponential $\pi^F: E^F \to B^F$ is a covariant fibration, too, hence the fiber $\xi^* \pi^F \equiv \ifun_B(\xi,\pi)$ is discrete.

§.§ Directed encode-decode

We point out a directed version of the
“encode-decode method” in order to characterize
$\hom$-types in higher inductive types
(and localizations).

The encode-decode method is used for a type $A$ with $a:A$,
together with a family $P : A \to \UU$ with $d: P(a)$.
The elimination rule for identity types gives a fiberwise
map $\varphi : \prod_{x:A}(a=x \to P(x))$,
sending the reflexivity path to $u$.
Since $\sum_{x:A}a=x$ is contractible,
and a fiberwise map is a fiberwise equivalence if and only if
the map on total types is an equivalence,
we get that $\varphi$ is a fiberwise equivalence
if and only if $\sum_{x:A}P(x)$ is contractible.

This has the following directed analog:

Let $A$ be a Segal type with $a:A$, and let
$P : A \to \UU$ be a covariant family with $d:P(a)$.
The fiberwise map
$\varphi : \prod_{x:A}(\hom_A(a,x) \to P(x))$
given by $\varphi(x,f) := f_!\,x$,
is a fiberwise equivalence if and only if
$\pair ad$ is an initial object in $\sum_{x:A}P(x)$.[Recall that $\sum_{x:A}P(x)$ is a Segal type.]

By <cit.>, $\sum_{x:A}\hom_A(a,x)$ has $\pair{a}{\id_a}$
as initial object.

Conversely, if $\pair ad$ is initial in $\sum_{x:A}P(x)$,
then each type $\sum_{f:\hom_A(a,x)}\dhom^P_f(d,e)$
is contractible, where $x:A$ and $e:P(x)$.
By <cit.>,
we have equivalences $\dhom^P_f(d,e) \equiv (f_!\,d = e)$,
and hence we get that the fiber of $\varphi_x$ at $e$,
which is $\sum_{f:\hom_A(a,x)}(f_!\,d=e)$,
is equivalent to $\sum_{f:\hom_A(a,x)}\dhom^P_f(d,e)$,
and is hence contractible.

§ YONEDA LEMMA FOR COCARTESIAN FAMILIES

In our synthetic setting, we prove a version of the Yoneda Lemma for cocartesian fibrations which reads as follows: For a Rezk type $B$ and a cocartesian family $P:B \to \UU$, evaluation at the identity map
is an equivalence:

\[ \prod_{b:B} \isEquiv \left( \Big( \prod^\cocart_{u:\comma{b}{B}} P(\partial_1\,u) \Big) \stackrel{\ev_{\id_b}}{\longrightarrow} P\,b\right)\]

Generalizing work by Street <cit.>, this Yoneda Lemma has been formulated and proved by Riehl–Verity w.r.t. $\infty$-cosmoses <cit.>, showing that it applies to cocartesian fibrations of $(\infty,n)$-categories for $0 \le n \le \infty$. For our proof, we adapt Riehl–Verity's methods to the type-theoretic setting, with significant simplifications because we are only considering $\inftyone$-categories. At the same time, this generalizes Riehl–Shulman's type-theoretic Yoneda Lemma for discrete covariant fibrations <cit.>.[In the discrete covariant case, the statement reads exactly the same, only without the restriction to cocartesian sections which has become vacuous.] A semantic version of the fibered Yoneda Lemma for discrete (co-)cartesian fibrations over Segal spaces has also been established by Rasekh <cit.>.

As discussed by Riehl–Shulman, the synthetic Yoneda Lemma can be understood as a directed path induction principle, now also applying to the case of categorical fibers. In fact—following Riehl–Verity as well as Riehl–Shulman—the Yoneda Lemma will follow from a general result about cocartesian fibrations $P:B \to \UU$ over a base $B$ with initial element $b:B$. Namely, evaluation at $b$ induces a LARI adjunction between the fiber and the type of sections which yields a (quasi-)equivalence when restricted to the cocartesian sections:

\[\begin{tikzcd}
{\prod_B^{\mathrm{cocart}} P} && {P\,b} \\
& {} \\
& {\prod_B P}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\mathrm{ev}_b}"', curve={height=12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\mathbf{y}_b}"', curve={height=12pt}, from=1-3, to=1-1]
\arrow[hook, from=1-1, to=3-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\mathrm{ev}_b}"', curve={height=12pt}, from=3-2, to=1-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\mathbf{y}_b}"', curve={height=12pt}, dotted, from=1-3, to=3-2]
\arrow["\simeq"{description}, draw=none, from=1, to=0]
\arrow["\dashv"{anchor=center, rotate=-30}, draw=none, from=3, to=2]
\end{tikzcd}\]

The Yoneda Lemma will follow as an instance of this result.

Here, for a given $b:B$, the LARI $\yon \defeq \yon_b$ is defined at $d:P\,b$, $x:B$ via cocartesian transport as

\[ (\yon\,d)(x) \defeq \partial_1\,P_!(\emptyset_x,d).\]

A key step is showing that $\yon$ lands in cocartesian sections. This can be shown by interpreting cocartesian lifts as $2$-cells $\chi_d: \cst \,d \rightarrow \yon\,d$, and then concluding by the formal properties of cocartesian arrows that the components of $\yon\,d$ are, in fact, cocartesian arrows.

The type-theoretic Yoneda Lemma for cocartesian families reads as follows.

§.§ Cocartesian sections from initial elements

Recall the definition of an initial element in a type.

Let $B$ be a type. An element $b:B$ is initial if

\[ \prod_{a:B} \isContr(\hom_B(b,a)).\]

We write $\emptyset_a:\hom_B(b,a)$ for the center of contraction if $b:B$ is initial. First, we establish the LARI adjunction result between the sections of the family and the fiber at the initial element.

Let $P: B \to \UU$ be a cocartesian family over a Rezk type $B$. If $b:B$ is initial the evaluation functor $\ev_b: \prod_B P \to P\,b$ has a LARI:

\[
\tikzset{%
every to/.append style={%
edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
\begin{tikzcd}
\prod_B P \ar[rr, bend right = 25, "\ev_b" swap, ""{name=B, below}] && P\,b \ar[ll, bend right = 25, dotted, "\yon" swap, ""{name=A, above}]
\ar[from=B, to=A, symbol=\vdash]
\end{tikzcd}
\]

The candidate for the left adjoint is

\[ \yon: P\,b \to \prod_BP, \quad \yon :\jdeq \lambda d.\lambda x.  \coliftpt{(\emptyset_x)}{d} \jdeq \partial_1 \, \coliftarr{P}{\emptyset_x}{d}. \]

We will show that the map

\[ \varphi: \hom_{\prod_B P}(\yon\,d,\sigma) \to \hom_{P\,b}(d,\sigma \,b), \quad \varphi : \jdeq \lambda \kappa.\kappa \,b \]

is an equivalence.

Since $b$ is initial, for any $x:B$ the hom-type $\hom_B(b,x)$ is contractible with center $\emptyset_x$. Since $P$ is cocartesian, we can define the map

\[ \psi:\hom_{P\,b}(d,\sigma \,b) \to \hom_{\prod_B P}(\yon\,d,\sigma), \psi\defeq \lambda f.\lambda x.\tyfill_{P_!(\emptyset_x,d)}(\sigma(\emptyset_x) \circ f). \]

To illustrate, $\psi$ yields the right-hand vertical arrow in squares of the form:

\[
\begin{tikzcd}
d \ar[rr, "{P_!(\emptyset_x, d)}", cocart]  \ar[d,"f" swap]  \ar[drr] && (\yon  d)x \ar[d, "{\psi(f, x)}", dashed] \\
\sigma b \ar[rr, "{\sigma \emptyset_x}" swap] && \sigma x \\
b \ar[rr, "{\emptyset_x}"] && x
\end{tikzcd}
\]

where $f:\hom_{P\,b}(d,\sigma \,b)$. For the round-trip alongs through $\varphi$ and $\psi$, note that we obtain a path $\varphi(\psi f) = \id_b$ since cocartesian lifts of identities are again identities.

For the other direction, note that as described in <ref> a morphism of sections $\kappa: \hom_{\prod_B P}(\yon\,d,\sigma)$ yields a square

\[
\begin{tikzcd}
d \ar[rr, "{P_!(\emptyset_x, d)}", cocart]  \ar[d,"\kappa b" swap]  \ar[drr] && (\yon  d)x \ar[d, "{\kappa x}", dashed] \\
\sigma b \ar[rr, "{\sigma \emptyset_x}" swap] && \sigma x \\
b \ar[rr, "{\emptyset_x}"] && x
\end{tikzcd}
\]

for every $x:B$.
But this means $\psi(\varphi \kappa)(x) = \kappa(x)$ as desired.

One checks that $(\yon f)(b) = f$, so $\yon$ is indeed a left adjoint right inverse to $\ev_b$.

In fact, the transport map $\yon: P\,b \to \prod_BP$ is valued in cocartesian sections.	We prove this by a kind of $2$-dimensional naturality argument of the cocartesian lifts.

Let $B$ be a Rezk type, $P: B \to \UU$ a cocartesian family and $b:B$ be an initial object. The map

\[ \yon : P\, b \to \prod_B P, \quad \yon :\jdeq \lambda d.\lambda x. \coliftpt{(\emptyset_x)}{d} \]

factors through the subtype of cocartesian sections, ,

\[
\begin{tikzcd}
P\,b \ar[rr, "\yon" swap, bend right = 15] \ar[r, "\yon"] & \prod_B^{\mathrm{cocart}} P \ar[r] & \prod_B P.
\end{tikzcd}
\]

For $d:P\,b$, consider the constant map $\cst(d) :\jdeq \lambda x.d : B \to E$, where $E\defeq \totalty{P}$. The cocartesian lifts w.r.t. $d:P\,b$ give rise to a natural transformation

\[ \chi:\hom_{B \to E}(\cst(d), \yon d) \equiv \prod_{x:B} \hom_E(\cst(d,x), \yon(d,x)), \quad \chi_x :\jdeq \coliftarr{P}{\emptyset_x}{d}. \]

Given $x,x':B$, for any arrow $u:\hom_B(x,x')$ we want to argue that the action of $\chi$ on $u$ yields a cocartesian arrow $\chi_u:\dhom^P_u(\yon dx,\yon dx')$.[We suppress the canonical $2$-cell witnessing composition.] Considering the naturality square

\[
\begin{tikzcd}
d \ar[d, cocart, "{\chi_x}"] \ar[drr, cocart, "{\chi_{x'}}"] \ar[rr, equals] && d \ar[d, cocart, "{\chi_{x'}}"]  \\
\yon(d,x) \ar[rr, "\yon du" swap] && \yon(d,x') \\
b \ar[d,"\emptyset_x" swap, dashed] \ar[drr, "\emptyset_{x'}", dashed] & & \\
x \ar[rr, "u" swap] & & x'
\end{tikzcd}
\]

it follows that $\yon du$ is cocartesian by <ref>(<ref>).

Let $B$ be a Rezk type, $b:B$ an initial object, and $P: B \to \UU$ a cocartesian family. Then evaluation at $b$

\[ \ev_b : \Big(\prod_{B}^{\mathrm{cocart}} P \Big) \to P\,b \]

is an equivalence.

By <ref>, the map $\yon$ restricts to cocartesian sections. By <ref>, $\ev_b\circ \mathbf y = \id_{P\,b}$.

We set $T :\jdeq  \prod_{B}^{\mathrm{cocart}} P$. For the converse direction, we define a natural transformation

\begin{align*}
\varepsilon : \hom_{T \to T}(\yon \circ \ev_b, \id_T) & \equiv \prod_{\sigma:T} \hom_T(\yon(\ev_b)(\sigma), \sigma) \\
& \equiv  \prod_{\sigma:T} \prod_{x: B} \hom_{P\,x}(\yon(\sigma(b))(x), \sigma(x))
\end{align*}

as follows:
For $x:B$, the action of $\sigma$ on $\emptyset_x:\hom_{B}(b,x)$ yields a cocartesian arrow $\sigma(\emptyset_x): \dhom^P_{\emptyset_x}(\sigma(b),\sigma(x))$.

We define $\varepsilon_{\sigma,x}$ as the following filler:

\[
\begin{tikzcd}
& & \sigma(x) \\
\sigma(b) \ar[rru, cocart, "\sigma(\emptyset_x)"]  \ar[rr, cocart, "{\coliftarr{P}{\emptyset_x}{\sigma(b)}}" swap] & & \yon(\sigma(b),x) \ar[u, dashed, "{\varepsilon_{\sigma,x}}" swap]	\\
b \ar[rr, "\emptyset_x"] && x
\end{tikzcd}
\]

By <ref>(<ref>), $\varepsilon_{\sigma,x}$ is cocartesian. As a cocartesian lift of an identity, it is itself an identity. By <cit.>, $\varepsilon:\hom_{T \to T}(\yon \circ \ev_b,\id_T)$ is an identity.

§.§ Dependent and absolute Yoneda Lemma

We now obtain analogues of the (dependent) Yoneda Lemma as in <cit.>, <cit.> for cocartesian families.

Let $B$ be a Segal type. For any element $b:B$, the identity morphism $\id_b:b \downarrow B$ is an initial object.

Let $B$ be a Rezk type, $b:B$ any element, and $Q: b\downarrow B \to \UU$ a cocartesian family. Then evaluation at $\id_b$ as in

\[ \ev_{\id_b} : \Big( \prod_{b \downarrow B}^{\mathrm{cocart}}Q \Big) \to Q(\id_b) \]

is an equivalence.

Because of <ref> (cf. <cit.>) this follows from <ref>.

Let $B$ be a Rezk type, $b:B$ any element, and $P: B \to \UU$ a cocartesian family. Then evaluation at $\id_b$ as in

\[ \ev_{\id_b} : \Big( \prod_{b \downarrow B}^{\mathrm{cocart}} \partial_1^* P \Big) \to P\,b \]

is an equivalence, where

\[ \partial_1\defeq \lambda u.u(1): b \downarrow B \to B.\]

This is an instance of the Dependent Yoneda Lemma <ref> for $Q\defeq \partial_1^*P \jdeq \lambda u.P(u1):b \downarrow B \to B$.

Noting that for a covariant family any section is cocartesian, we recover the discrete versions from <cit.>.

Let $B$ be a Rezk type, $b:B$ any element, and $Q: b\downarrow B \to \UU$ a covariant family. Then evaluation at $\id_b$ as in

\[ \ev_{\id_b} : \Big( \prod_{b \downarrow B}Q \Big) \to Q(\id_b) \]

is an equivalence.

Let $B$ be a Rezk type, $b:B$ any element, and $P: B \to \UU$ a covariant family. Then evaluation at $\id_b$ as in

\[ \ev_{\id_b} : \Big( \prod_{b \downarrow B} \partial_1^* P \Big) \to P\,b \]

is an equivalence, where

\[ \partial_1\defeq \lambda u.u(1): b \downarrow B \to B.\]

§ LAX SQUARES

Since Segal types form an exponential ideal, simplicial type theory in fact captures some of the $2$-dimensional theory of synthetic $\inftyone$-categories, cf. <cit.>. For Rezk types $A,B$ the type $B^A$ is again Rezk, with mapping spaces $\nat{A}{B}(f,g) \jdeq (f \Rightarrow g)$. This invites a treatment of lax squares

\[\begin{tikzcd}
A && B \\
C && D
\arrow["k"', from=1-1, to=2-1]
\arrow["h"', from=2-1, to=2-3]
\arrow["f", from=1-1, to=1-3]
\arrow["g", from=1-3, to=2-3]
\arrow["\sigma", Rightarrow, from=2-1, to=1-3]
\end{tikzcd}\]

which are encoded by $2$-cells

\[ \sigma: hk \Rightarrow gf \simeq \prod_{a:A} (hk)(a) \to (gf)(a).\]

We are mainly interested in some basic results about mates, known from classical $2$-category theory, re-interpreted in the context of higher categories as in <cit.> (cf. op. cit., Appendix B, for the classical setting). These occur in our study of cocartesian functors <ref>.

First, in <ref> we explicitly define pasting operations for lax squares. Then we prove a simple pasting theorem for a specific pasting scheme, which is used in <ref> to establish the mates correspondence for an adjunction.

Alas, in the absence of categorical type universes, a general pasting theorem, possibly along the lines of <cit.>, seems out of reach. Therefore, we will only in an ad hoc manner consider a few very specific pasting schemes relevant to our specific applications, and prove well-definedness of these pastings by manual pasting diagram chases, which is straightforward, though lengthy to spell out.

§.§ Pasting of lax squares

In this subsection, we introduce horizontal and vertical pasting of lax squares of functors between Segal types. We prove that these pasting operations are associative, and establish a certain pasting theorem which will be used to establish the mate correspondence subsequently in <ref>.

* The horizontal pasting of a natural transformations $\alpha:\nat{A}{A'}(hu,u'k)$ with a natural transformation $\alpha':\nat{A'}{A''}(h'u',u''k')$ as indicated in

\[\begin{tikzcd}
{B} & {B'} & {B''} & {} & {B} && {B''} \\
{A} & {A'} & {A''} & {} & {A} && {A''}
\arrow["{u}"', from=1-1, to=2-1]
\arrow["{h}"', from=2-1, to=2-2]
\arrow["{k}", from=1-1, to=1-2]
\arrow["{u'}"', from=1-2, to=2-2]
\arrow[Rightarrow, "{\alpha}", from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow["{h'}"', from=2-2, to=2-3]
\arrow["{u''}", from=1-3, to=2-3]
\arrow["{k'}", from=1-2, to=1-3]
\arrow[Rightarrow, "{\alpha'}", from=2-2, to=1-3, shorten <=3pt, shorten >=3pt]
\arrow["{\rightsquigarrow}" description, from=1-4, to=2-4, phantom, no head]
\arrow["{u}"', from=1-5, to=2-5]
\arrow["{k'k}", from=1-5, to=1-7]
\arrow["{h'h}"', from=2-5, to=2-7]
\arrow["{u''}", from=1-7, to=2-7]
\arrow[Rightarrow, "{\alpha' \hpaste \alpha}", from=2-5, to=1-7, shorten <=7pt, shorten >=7pt]
\end{tikzcd}\]

is defined as:

\[ \alpha' \hpaste \alpha\defeq (\alpha' * \id_k) \circ (\id_{h'} * \alpha):\nat {B}{A''}(h'hu,u''k'k)\]

* The vertical pasting of a natural transformations $\beta:\nat{A}{A'}(f'h,kf)$ with a natural transformation $\beta':\nat{A'}{A''}(f''h',k'f')$ as indicated in

\[\begin{tikzcd}
{A} & {B} && {A} & {B} \\
{A'} & {B'} & {\rightsquigarrow} \\
{A''} & {B''} && {A''} & {B''}
\arrow["{f}", from=1-1, to=1-2]
\arrow["{h}"', from=1-1, to=2-1]
\arrow["{f'}",from=2-1, to=2-2]
\arrow["{h'}"', from=2-1, to=3-1]
\arrow["{f''}"', from=3-1, to=3-2]
\arrow["{k'}", from=2-2, to=3-2]
\arrow[Rightarrow, "{\beta'}", from=3-1, to=2-2, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\beta}", from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow["{f}"', from=1-4, to=1-5]
\arrow["{h'h}"', from=1-4, to=3-4]
\arrow["{k'k}", from=1-5, to=3-5]
\arrow[Rightarrow, "{\beta' \vpaste \beta}", from=3-4, to=1-5, shorten <=6pt, shorten >=6pt]
\arrow["{k}", from=1-2, to=2-2]
\arrow["{f''}"', from=3-4, to=3-5]
\end{tikzcd}\]

is defined as:

\[  \beta' \vpaste \beta :\jdeq (\id_{k'}*\beta) \circ (\beta' * \mathrm{id}_h) : \nat{A}{B''}(f''h'h,k'kf)\]

\[\begin{tikzcd}
{} & B && {A''} & {} & A && {B''}
\arrow[""{name=0, anchor=center, inner sep=0}, "{h'hu}"{description}, curve={height=-60pt}, from=1-2, to=1-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "{h'u'k}"{description}, from=1-2, to=1-4]
\arrow[""{name=2, anchor=center, inner sep=0}, "{u''k'k}"{description}, curve={height=60pt}, from=1-2, to=1-4]
\arrow["{\beta'\vpaste \beta\defeq}"{description}, draw=none, from=1-5, to=1-6]
\arrow["{\alpha' \hpaste \alpha \defeq}"{description}, draw=none, from=1-1, to=1-2]
\arrow[""{name=3, anchor=center, inner sep=0}, "{k'f'h}"{description}, from=1-6, to=1-8]
\arrow[""{name=4, anchor=center, inner sep=0}, "{f''h'h}"{description}, curve={height=-60pt}, from=1-6, to=1-8]
\arrow[""{name=5, anchor=center, inner sep=0}, "{k'kf}"{description}, curve={height=60pt}, from=1-6, to=1-8]
\arrow["{\mathrm{id}_{h'}*\alpha}"{description}, shorten <=3pt, shorten >=3pt, Rightarrow, from=0, to=1]
\arrow["{\alpha'*\mathrm{id}_k}"{description}, shorten <=3pt, shorten >=3pt, Rightarrow, from=1, to=2]
\arrow["{\beta'*\id_h}"{description}, shorten <=4pt, shorten >=4pt, Rightarrow, from=4, to=3]
\arrow["{\id_{k'}*\beta}"{description}, shorten <=4pt, shorten >=4pt, Rightarrow, from=3, to=5]
\end{tikzcd}\]

Horizontal and vertical pasting of squares

For Segal types, consider $2$-cells as given in the diagram:

\[\begin{tikzcd}
{B} & {B'} & {B''} & {B'''} \\
{A} & {A'} & {A''} & {A'''}
\arrow["{u}"', from=1-1, to=2-1]
\arrow["{k}", from=1-1, to=1-2]
\arrow["{h}"', from=2-1, to=2-2]
\arrow["{k'}", from=1-2, to=1-3]
\arrow["{h'}"', from=2-2, to=2-3]
\arrow["{u''}"', from=1-3, to=2-3]
\arrow["{k''}", from=1-3, to=1-4]
\arrow["{h''}"', from=2-3, to=2-4]
\arrow["{u'''}"', from=1-4, to=2-4]
\arrow["{u'}"', from=1-2, to=2-2]
\arrow[Rightarrow, "{\alpha}", from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\alpha'}", from=2-2, to=1-3, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\alpha''}", from=2-3, to=1-4, shorten <=3pt, shorten >=3pt]
\end{tikzcd}\]

This defines a unique pasting $2$-cell $\alpha''':\hom_{B \to A'''}(h''h'hu,u'''k''k'k)$, so in particular there is an identification

\[ (\alpha'' \hpaste \alpha') \hpaste \alpha = \alpha'''= \alpha'' \hpaste (\alpha' \hpaste \alpha).\]

We define $\beta : \hom_{B \to A''}(h'hu,u''k'k)$ as the composition $\beta\defeq \alpha \hpaste \alpha'$, , for all $b:B$:

\[
\begin{tikzcd}
\beta_b : h'hu(b) \ar[rr, "h'\alpha_b"] & & h'u'k(b) \ar[rr, "\alpha'_{kb}"] && u''k'k(b)
\end{tikzcd}
\]

Pasting $\alpha''$ on the right gives the natural transformation $\alpha'' \hpaste \beta \jdeq (\alpha'' * \id_{k'k}) \circ (\id_{h''} * \beta)$:

\[\begin{tikzcd}
{h''h'hu(b)} && {h''u''k'k(b)} && {u'''k''k'k(b)} \\
& {h''h'u'k(b)}
\arrow["{h''\beta_b}", from=1-1, to=1-3]
\arrow["{h''h'\alpha_b}"', from=1-1, to=2-2]
\arrow["{h''\alpha'_{kb}}"', from=2-2, to=1-3]
\arrow["{\alpha''_{k'kb}}", from=1-3, to=1-5]
\end{tikzcd}\]

By symmetry, one can show that for $\gamma : \hom_{B'\to A'''}(h''h'u',u'''k''k')$ defined as $\gamma :\jdeq \alpha'' \hpaste \alpha'$ the composite $\gamma \hpaste \alpha \jdeq (\gamma * \id_{k})\circ (\id_{h''h'}*\alpha)$ coincides with $\alpha'' \hpaste \beta$.

For Segal types, consider $2$-cells as given in the diagram:

\[\begin{tikzcd}
{A} & {B} \\
{A'} & {B'} \\
{A''} & {B''} \\
{A'''} & {B'''}
\arrow["{h}"', from=1-1, to=2-1]
\arrow["{f}", from=1-1, to=1-2]
\arrow["{f'}", from=2-1, to=2-2]
\arrow["{k}", from=1-2, to=2-2]
\arrow["{h'}"', from=2-1, to=3-1]
\arrow["{f''}", from=3-1, to=3-2]
\arrow["{k'}", from=2-2, to=3-2]
\arrow["{h''}"', from=3-1, to=4-1]
\arrow["{f'''}", from=4-1, to=4-2]
\arrow["{k''}", from=3-2, to=4-2]
\arrow[Rightarrow, "{\beta}", from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\beta'}", from=3-1, to=2-2, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\beta''}", from=4-1, to=3-2, shorten <=3pt, shorten >=3pt]
\end{tikzcd}\]

This defines a unique pasting $2$-cell $\beta''':\hom_{B \to A'''}(f'''h''h'h,k''k'kf)$, so in particular there is an identification

\[ (\beta'' \hpaste \beta') \hpaste \beta = \beta'''=\beta'' \hpaste (\beta' \hpaste \beta).\]

The proof is completely analogous to the proof for the horizontal pasting.

To prove the mate correspondence we need the following pasting theorem involving $2$-cells with identity boundaries.

For Segal types, consider the following configuration of natural transformations:

\[\begin{tikzcd}
{A} && {B} && {B} && \\
{A} && {A} && {B} && \\
&& {A'} && {B'} && {B'} \\
&& {A'} && {A'} && {B'}
\arrow["{f'}" description, from=4-5, to=4-7]
\arrow["{u'}"', from=3-5, to=4-5]
\arrow[from=3-5, to=3-7, no head, equals]
\arrow[from=3-7, to=4-7, no head, equals]
\arrow[from=4-3, to=4-5, no head, equals]
\arrow[from=3-3, to=4-3, no head, equals]
\arrow["{f'}" description, from=3-3, to=3-5]
\arrow["{h}"', from=2-3, to=3-3]
\arrow["{f}" description, from=2-3, to=2-5]
\arrow["{k}", from=2-5, to=3-5]
\arrow["{u}"', from=1-3, to=2-3]
\arrow[from=1-3, to=1-5, no head, equals]
\arrow[from=2-1, to=2-3, no head, equals]
\arrow[from=1-1, to=2-1, no head, equals]
\arrow["{f}" description, from=1-1, to=1-3]
\arrow[Rightarrow, "{\varphi}" description, from=2-1, to=1-3, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\psi}" description, from=2-3, to=1-5, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\beta}" description, from=3-3, to=2-5, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\varphi'}" description, from=4-3, to=3-5, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\psi'}" description, from=4-5, to=3-7, shorten <=7pt, shorten >=7pt]
\arrow[from=1-5, to=2-5, no head, equals]
\end{tikzcd}\]

This gives rise to a unique pasting $2$-cell, in particular there is a homotopy

\[ (\psi' \hpaste \varphi') \vpaste \beta \vpaste (\psi \hpaste \varphi) = \psi' \hpaste (\varphi' \vpaste \beta \vpaste \psi) \hpaste \varphi.\]

\[\begin{tikzcd}
&&&&&&&& {A} && {B} \\
{A} && {B} && {B'} && {B'} & {} & {A} && {B} \\
{A} && {A} && {A'} && {B'} & {} & {A'} && {B'} \\
&&&&&&&& {A'} && {B'}
\arrow["{=}" description, from=2-8, to=3-8, phantom, no head, equals]
\arrow["{f}" description, from=1-9, to=1-11]
\arrow[from=1-9, to=2-9, no head, equals]
\arrow["{f}" description, from=2-9, to=2-11]
\arrow[from=1-11, to=2-11, no head, equals]
\arrow["{h}"', from=2-9, to=3-9]
\arrow["{f'}" description, from=3-9, to=3-11]
\arrow["{k}", from=2-11, to=3-11]
\arrow["{f'}" description, from=4-9, to=4-11]
\arrow[from=3-11, to=4-11, no head, equals]
\arrow[Rightarrow, "{\psi\hpaste\varphi}" description, from=2-9, to=1-11, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\beta}" description, from=3-9, to=2-11, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\psi'\hpaste\varphi'}" description, from=4-9, to=3-11, shorten <=7pt, shorten >=7pt]
\arrow[from=3-9, to=4-9, no head, equals]
\arrow["{u'}"', from=2-5, to=3-5]
\arrow[from=2-5, to=2-7, no head, equals]
\arrow[from=2-7, to=3-7, no head, equals]
\arrow["{f'}" description, from=3-5, to=3-7]
\arrow[Rightarrow, "{\psi'}" description, from=3-5, to=2-7, shorten <=7pt, shorten >=7pt]
\arrow["{h}" description, from=3-3, to=3-5]
\arrow["{k}" description, from=2-3, to=2-5]
\arrow["{u}"', from=2-3, to=3-3]
\arrow[from=3-1, to=3-3, no head, equals]
\arrow[Rightarrow, "{\varphi}" description, from=3-1, to=2-3, shorten <=7pt, shorten >=7pt]
\arrow[from=2-1, to=3-1, no head, equals]
\arrow["{f}" description, from=2-1, to=2-3]
\arrow[Rightarrow, "{\varphi'\vpaste\beta\vpaste\psi}" description, from=3-3, to=2-5, shorten <=7pt, shorten >=7pt]
\end{tikzcd}\]

Given a $2$-cell $\beta:f'h \Rightarrow kf$, we spell out the $2$-cells generated by the pastings on either side of the identification. Each time, this is done in two steps, first considering the diagram in the middle, and then pasting the cells on the sides. For the horizontal composite $H \defeq \psi' \hpaste (\varphi' \vpaste \beta \vpaste \psi) \vpaste \varphi$, we find

\[\begin{tikzcd}
{\alpha :\jdeq \varphi'\vpaste\beta\vpaste\psi:} & {hu(b)} && {u'f'hu(b)} && {u'kfu(b)} && {u'k(b)}
\arrow["{\varphi'_{hu(b)}}", from=1-2, to=1-4]
\arrow["{u'\beta_{u(b)}}", from=1-4, to=1-6]
\arrow["{u'k\psi_b}", from=1-6, to=1-8]
\end{tikzcd}\]

which yields the resulting cell:

\[\begin{tikzcd}
{\psi'\hpaste\alpha\hpaste\varphi:} & {f'h(a)} && {f'huf(a)} && {f'u'kf(a)} & {kf(a)} & {} && {} \\
&&& {} \\
&&& {f'u'f'huf(a)} & {} & {f'u'kfuf(a)} & {}
\arrow["{f'h\varphi_a}", from=1-2, to=1-4]
\arrow["{f'\alpha_{f(a)}}", from=1-4, to=1-6]
\arrow["{f'u'\beta_{uf(a)}}"', from=3-4, to=3-6]
\arrow["{f'u'k\psi_{f(a)}}"', from=3-6, to=1-6]
\arrow["{\psi'_{kf(a)}}", from=1-6, to=1-7]
\arrow["{f'\varphi'_{huf(a)}}"', from=1-4, to=3-4]
\end{tikzcd}\]

The vertical composite $V\defeq (\psi' \hpaste \varphi') \vpaste \beta \vpaste (\varphi \hpaste \psi)$ is treated accordingly. In sum, we get the two composites:

\[\begin{tikzcd}
{H:f'h} & {f'huf} & {f'u'f'huf} & {f'u'kfuf} & {f'u'kf} & kf \\
{V:f'h} & {f'u'f'h} & {f'h} & kf & kfuf & kf
\arrow["{f'h\varphi}", Rightarrow, from=1-1, to=1-2]
\arrow["{f'\varphi'h}", Rightarrow, from=2-1, to=2-2]
\arrow["{\psi'f'h}", Rightarrow, from=2-2, to=2-3]
\arrow["\beta", Rightarrow, from=2-3, to=2-4]
\arrow["kf\varphi", Rightarrow, from=2-4, to=2-5]
\arrow["{k\psi f}", Rightarrow, from=2-5, to=2-6]
\arrow["{f'\varphi'huf}", Rightarrow, from=1-2, to=1-3]
\arrow["{f'u'\beta uf}", Rightarrow, from=1-3, to=1-4]
\arrow["{f'u'k\psi f}", Rightarrow, from=1-4, to=1-5]
\arrow["{\psi'kf}", Rightarrow, from=1-5, to=1-6]
\end{tikzcd}\]

We are to show that the composite $2$-cells $H$ and $V$ coincide.

Ultimately, this is established by commutation of the following diagram of natural transformations in $A \to B'$ (which can be checked pointwisely) where the outermost left composite is the $2$-cell $V$, and the outermost right composite is $H$:

\[\begin{tikzcd}
& {f'h} && {f'huf} \\
{f'h} & {f'u'f'h} && {f'u'f'huf} \\
& {f'u'kf} && {f'u'kfuf} && {f'u'kf} \\
& kf && kfuf && kf
\arrow["{f'\varphi'h}"', Rightarrow, from=1-2, to=2-2]
\arrow["{f'h\varphi}"{description}, Rightarrow, from=1-2, to=1-4]
\arrow["{f'u'f'h\varphi}"{description}, Rightarrow, from=2-2, to=2-4]
\arrow["{f'\varphi'huf}", Rightarrow, from=1-4, to=2-4]
\arrow[""{name=0, anchor=center, inner sep=0}, "{f'u'\beta}"', Rightarrow, from=2-2, to=3-2]
\arrow["{f'u'kf\varphi}"{description}, Rightarrow, from=3-2, to=3-4]
\arrow["{\psi'kf}"', Rightarrow, from=3-2, to=4-2]
\arrow["{kf\varphi }"', Rightarrow, from=4-2, to=4-4]
\arrow["{\psi'kfuf}"{description}, Rightarrow, from=3-4, to=4-4]
\arrow["{f'u'\beta uf}", Rightarrow, from=2-4, to=3-4]
\arrow["{f'u'k\psi f}", Rightarrow, from=3-4, to=3-6]
\arrow["{k\psi f}"', Rightarrow, from=4-4, to=4-6]
\arrow["{\psi'kf}", Rightarrow, from=3-6, to=4-6]
\arrow["{f'(\varphi'h*\varphi)}"{description}, Rightarrow, from=1-2, to=2-4]
\arrow["{f'u'(\beta * \varphi)}"{description}, Rightarrow, from=2-2, to=3-4]
\arrow["{\psi'k*\varphi f}"{description}, Rightarrow, from=3-2, to=4-4]
\arrow["{\psi'k*\psi f}"{description}, Rightarrow, from=3-4, to=4-6]
\arrow["{\psi'f'h}"', Rightarrow, from=2-2, to=2-1]
\arrow[""{name=2, anchor=center, inner sep=0}, "\beta"{description}, curve={height=24pt}, Rightarrow, from=2-1, to=4-2]
\arrow["{(*)}"{description, pos=0.4}, Rightarrow, draw=none, from=2, to=0]
\end{tikzcd}\]

Here, the identity $(*)$ is established by:

\[\begin{tikzcd}
{f'u'f'h} && {f'u'kf} \\
{f'h} && {kf}
\arrow["{f'u'\beta}", from=1-1, to=1-3]
\arrow["{\psi'f'h}"', from=1-1, to=2-1]
\arrow["{\beta}"', from=2-1, to=2-3]
\arrow["{\psi'kf}", from=1-3, to=2-3]
\arrow["{\psi*\beta}" description, from=1-1, to=2-3]
\end{tikzcd}\]

In sum, as desired we have constructed a path between the two composites

\[ H \jdeq \psi' \hpaste (\varphi' \vpaste \beta \vpaste \psi) \vpaste \varphi = (\psi' \hpaste \varphi') \vpaste \beta \vpaste (\varphi \hpaste \psi) \jdeq V. \]

§.§ Mates

We are now able to capture the mates correspondence of an adjunction in type theory.

Consider adjunctions and morphisms between Rezk types as follows:

\[\begin{tikzcd}
{B} & {B'} \\
{A} & {A'}
\arrow["{u}"{name=0}, from=1-1, to=2-1]
\arrow["{h}"', from=2-1, to=2-2]
\arrow["{k}", from=1-1, to=1-2]
\arrow["{f}"{name=1}, from=2-1, to=1-1, curve={height=-12pt}]
\arrow["{f'}"{name=2, swap}, from=2-2, to=1-2, curve={height=12pt}]
\arrow["{u'}"{name=3, swap}, from=1-2, to=2-2]
\arrow["\dashv"{rotate=0}, from=1, to=0, phantom]
\arrow["\dashv"{rotate=-180}, from=2, to=3, phantom]
\end{tikzcd}\]

There is an equivalence between types of natural transformations

\[ \Phi: \nat B {A'}(hu,u'k) \equiv \nat A {B'}(f'h,kf) : \Psi\]

traditionally known as the mates correspondence,  <cit.>, given by pasting in the following way[The associativity theorems tell us that the diagrams are well-defined when read as pasting diagrams.]:

\[\begin{tikzcd}
{B} & {B'} & {} &&& {B} & {B'} && {A'} \\
{A} & {A'} & {} & {B} && {A} & {A'} \\
{B} & {B'} & {} & {A} && {B} & {B'} \\
{A} & {A'} & { } & {} && {A} & {A'} && {B'} \\
&&&& {} &&&& {} \\
&&&&&&& {}
\arrow["{k}", from=3-1, to=3-2]
\arrow["{h}"', from=4-1, to=4-2]
\arrow["{u}"', from=3-6, to=4-6]
\arrow["{f}", from=3-4, to=3-6]
\arrow[Rightarrow, ""{name=0, inner sep=0}, from=3-4, to=4-6, shorten <=7pt, shorten >=7pt, no head]
\arrow["{k}", from=3-6, to=3-7]
\arrow["{h}"', from=4-6, to=4-7]
\arrow["{u'}"', from=3-7, to=4-7]
\arrow["{f'}"', from=4-7, to=4-9]
\arrow[Rightarrow, ""{name=1, inner sep=0}, from=4-9, to=3-7, shorten <=7pt, shorten >=7pt, no head]
\arrow[Rightarrow, "{\beta}", from=4-6, to=3-7, shorten <=3pt, shorten >=3pt]
\arrow["{:=}" description, from=3-3, to=4-3, phantom, no head]
\arrow[Rightarrow, "{\alpha_\beta}"', from=4-2, to=3-1, shorten <=3pt, shorten >=3pt]
\arrow["{f}", from=4-1, to=3-1]
\arrow["{f'}"', from=4-2, to=3-2]
\arrow["{u}"', from=1-1, to=2-1]
\arrow["{h}"', from=2-1, to=2-2]
\arrow["{u'}"' swap, from=1-2, to=2-2]
\arrow["{:=}" description, from=1-3, to=2-3, phantom, no head]
\arrow[Rightarrow, "{\beta_\alpha}", from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow["{u}"', from=2-4, to=2-6]
\arrow["{f}", from=2-6, to=1-6]
\arrow["{f'}"', from=2-7, to=1-7]
\arrow["{u'}", from=1-7, to=1-9]
\arrow[Rightarrow, ""{name=2, inner sep=0}, from=2-4, to=1-6, shorten <=7pt, shorten >=7pt, no head]
\arrow["{k}", from=1-6, to=1-7]
\arrow["{h}"', from=2-6, to=2-7]
\arrow[Rightarrow, "{\alpha}"', from=2-7, to=1-6, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, ""{name=3, inner sep=0}, from=1-9, to=2-7, shorten <=7pt, shorten >=7pt, no head]
\arrow["{k}", from=1-1, to=1-2]
\arrow[Rightarrow, "{\varepsilon'}" description, from=4-7, to=1, shorten <=4pt, shorten >=4pt]
\arrow[Rightarrow, "{\eta}" description, from=0, to=3-6, shorten <=4pt, shorten >=4pt]
\arrow[Rightarrow, "{\varepsilon}" description, from=2-6, to=2, shorten <=4pt, shorten >=4pt]
\arrow[Rightarrow, "{\eta'}" description, from=3, to=1-7, shorten <=4pt, shorten >=4pt]
\end{tikzcd}\]

Explicitly, the constructions are given by:

\[\begin{tikzcd}
{} & {\beta_\alpha \defeq \Phi(\alpha) \defeq \Big(f'ha} && {f'hufa} && {f'u'kfa} && {kfa \Big)} \\
& {\alpha_\beta \defeq \Psi(\beta) \defeq \Big( hub} && {u'f'hub} && {u'kfu(b)} && {u'kb\Big)}
\arrow["f'\eta_{ha}", from=1-2, to=1-4]
\arrow["{f'\alpha_{fa}}", from=1-4, to=1-6]
\arrow["{\varepsilon'_{kfa}}", from=1-6, to=1-8]
\arrow["{u'\beta_{ub}}", from=2-4, to=2-6]
\arrow["{u'k\varepsilon_b}", from=2-6, to=2-8]
\arrow["\eta'_{hub}", from=2-2, to=2-4]
\end{tikzcd}\]

Consider the maps

\begin{align*}
\Phi & : \nat B {A'}(hu,u'k) \to \nat B {A'}(f'h,kf), & \Phi(\alpha) :\jdeq \varepsilon' \hpaste \alpha \hpaste \eta \\
\Psi & : \nat A {B'}(f'h,kf) \to \nat B {A'}(hu,u'k), & \Psi(\beta) :\jdeq \eta' \vpaste \beta \vpaste \varepsilon.
\end{align*}

By the previous pasting theorem, we obtain for $\alpha : hu \Rightarrow u'k$ an identification

\[ \Psi(\Phi(\alpha)) = \eta' \vpaste \Phi(\alpha) \vpaste \varepsilon = (\eta' \hpaste \varepsilon') \vpaste \alpha \vpaste (\eta \hpaste \varepsilon) = \alpha \]

invoking witnesses for the triangle identities, via <cit.>.

The round trip in the converse direction is analogous.

Given Rezk types $A,B$ with adjunctions $f \dashv u:B \to A$, $f' \dashv u':B \to A$, consider a $2$-cell $\alpha: u \Rightarrow u'$ and its mate $\alpha': f \Rightarrow f'$. Then $\alpha$ is invertible if and only if $\alpha'$ is:

\[\begin{tikzcd}
{B} & {B} & {} & {B} & {B} \\
{A} & {A} & {} & {A} & {A}
\arrow["{u}"', from=1-1, to=2-1]
\arrow["{=}", from=1-1, to=1-2]
\arrow["{=}"', from=2-1, to=2-2]
\arrow["{u'}", from=1-2, to=2-2]
\arrow["{\leftrightsquigarrow}" description, from=1-3, to=2-3, phantom, no head]
\arrow["{=}", from=1-4, to=1-5]
\arrow["{f}", from=2-4, to=1-4]
\arrow["{f'}"', from=2-5, to=1-5]
\arrow[Rightarrow, "{\alpha}", "{=}" swap, from=2-1, to=1-2, shorten <=3pt, shorten >=3pt]
\arrow[Rightarrow, "{\alpha'}"', "{=}",  from=2-5, to=1-4, shorten <=3pt, shorten >=3pt]
\arrow["{=}"', from=2-4, to=2-5]
\end{tikzcd}\]

By precondition, we have the identification $\alpha:u = u'$. Recall the uniqueness of left adjoints and all the accompanying data <cit.>. Since both $f \dashv u$, $f' \dashv u'$, also $f' \dashv u$, but this implies there is an identification $f=f'$. Furthermore, the counit $\varepsilon'$ can be replaced by $\varepsilon$.

Thus, the mate of $\alpha$ at $a:A$ is homotopic to the composite

\[
\begin{tikzcd}
f'a \ar[rr,"{f \eta_a}"] && fufa \ar[rr,equals, "{f\alpha_{fa}}"] && f'u'fa \ar[rr,"{\varepsilon_{fa}}"] && fa
\end{tikzcd}
\]

which is an isomorphism by one of the triangle identities.

Consider adjunctions between Rezk types as in:

\[\begin{tikzcd}
{B} && {B'} \\
{A} && {A'}
\arrow["{k}"{name=0, description}, from=2-1, to=2-3]
\arrow["{k'}"{name=1, description}, from=1-1, to=1-3]
\arrow["{u'}"{name=2, swap}, from=1-3, to=2-3]
\arrow[Rightarrow, "{\alpha}" description, from=2-1, to=1-3, shorten <=7pt, shorten >=7pt]
\arrow["{f}"{name=3}, from=2-1, to=1-1, curve={height=-18pt}]
\arrow["{\ell'}"{name=4, description}, from=1-3, to=1-1, curve={height=18pt}]
\arrow["{\ell}"{name=5, description}, from=2-3, to=2-1, curve={height=-18pt}]
\arrow["{f'}"{name=6, swap}, from=2-3, to=1-3, curve={height=18pt}]
\arrow["{u}"{name=7}, from=1-1, to=2-1]
\arrow["\dashv"{rotate=-90}, from=4, to=1, phantom]
\arrow["\dashv"{rotate=90}, from=5, to=0, phantom]
\arrow["\dashv"{rotate=0}, from=3, to=7, phantom]
\arrow["\dashv"{rotate=-180}, from=6, to=2, phantom]
\end{tikzcd}\]

Then the mate $\alpha':u \ell' \Rightarrow \ell u'$ w.r.t. the horizontal adjunctions is invertible if and only if the mate $\alpha'':f'h \Rightarrow h'f$ w.r.t. the vertical adjunctions is:

\[\begin{tikzcd}
{B} && {B'} & {} & {B} && {B'} \\
{A} && {A'} & {} & {A} && {A'}
\arrow["{u}"', from=1-1, to=2-1]
\arrow["{u'}", from=1-3, to=2-3]
\arrow["{\leftrightsquigarrow}" description, from=1-4, to=2-4, phantom, no head]
\arrow["{h}" description, from=2-5, to=2-7]
\arrow["{h'}" description, from=1-5, to=1-7]
\arrow["{f'}"', from=2-7, to=1-7]
\arrow["{f}", from=2-5, to=1-5]
\arrow["{\ell'}" description, from=1-3, to=1-1]
\arrow["{\ell}" description, from=2-3, to=2-1]
\arrow[Rightarrow, "{\alpha'}" swap,  "=", from=1-1, to=2-3, shorten <=7pt, shorten >=7pt]
\arrow[Rightarrow, "{\alpha''}" swap,  "=", from=2-7, to=1-5, shorten <=7pt, shorten >=7pt]
\end{tikzcd}\]

This becomes an instance of <ref> after considering the composites of the adjunctions.

§ LARI AND FIBERED ADJUNCTIONS

We complement Riehl–Shulman's theory of adjunctions <cit.> by a treatment of left adjoint right inverse (LARI) adjunctions. Hereby, we assume the types involved to be Rezk.

Specifically, we provide a characterization result <ref> along the lines of <cit.>, as well as various closure properties which imply the closure properties in <ref> and <ref>. In particular, by fibrant replacement, we can identify LARI adjunctions between Rezk types with adjunctions whose left adjoint is a section. As for the stability properties, LARI adjunctions (between Rezk types) are always closed under dependent products, composition and pullback. This in turn implies the same closure properties for LARI fibrations <ref>.

Finally, we briefly discuss fibered adjunctions between isoinner families over a Rezk type. These occur in the characterization theorems of cocartesian families <ref> and functors <ref>.

§.§ Left adjoint right inverse (LARI) adjunctions

After providing a characterization of LARI adjunctions, similar to and relying on <cit.>, we prove a few closure properties. From these we derive corresponding closure properties of $j$-LARI fibrations (hence also cocartesian fibrations) in the main text <ref>.

§.§.§ Characterizations of LARI adjunctions

A transposing left adjoint right inverse adjunction (or LARI adjunction for short) between Rezk types $A,B$ consists of:

* a transposing adjunction, consisting of functors $u:B \to A$, $f:A \to B$, and a family of equivalences $\varphi:\prod_{a:A, b:B} \hom_B(fa,b) \equiv \hom_A(a,ub)$

* such that for all $a:A$ the components $\eta_{\varphi,a} \defeq \varphi_{a,fa}(\id_{fa}) : \hom_A(a,ufa)$ of the unit are isomorphisms.

Given this data, $f$ is called a transposing left adjoint right inverse (or transposing LARI).

A bi-diagrammatic left adjoint right inverse adjunction (or bi-diagrammatic LARI adjunction) between Rezk types $A$ and $B$ consists of:

* functors $u:B \to A$, $f:A \to B$

* a natural isomorphism $\eta:\iso_{A \to A}(\id_A, uf)$

* two natural transformations $\varepsilon, \varepsilon' : \hom_{B \to B}(fu,\id_B)$

* a path $\alpha:u\varepsilon \circ \eta u = \id_u$

* a path $\beta:\varepsilon' f \circ f \eta = \id_f$

Given this data, $f$ is called a bi-diagrammatic left adjoint right inverse (or bi-diagrammatic LARI).

A lifting LARI adjunction between Rezk types $A$ and $B$ consists of  functors $u:B \to A$, $f:A \to B$ with a homotopy $\sigma:u \circ f = \id_A$ such that the following holds: For all $a:A, b:B$ and arrows $\alpha:\hom_A(a,ub)$ there exists uniquely up to homotopy an arrow $\beta:\hom_B(fa,b)$ with $u\circ \beta = \alpha$:

\[
\begin{tikzcd}
\partial \Delta^1 \ar[rr, "{[fa, b]}"] \ar[d] & & B  \ar[d, "u"] \\
\Delta^1 \ar[rr, "\alpha" swap] \ar[rru, dashed, "\beta" description]&& A
\end{tikzcd}
\]

Given this data, $f$ is called a lifting left adjoint right inverse (or lifting LARI).

For a functor $u: B \to A$ between Rezk types the following types are equivalent propositions:

*  The type of transposing LARIs of $u$.

*  The type of lifting LARIs of $u$.

*  The type of functors $f:A \to B$ together with natural isomorphisms $\eta:\iso_{A \to A}(\id_A,uf)$ such that $\varphi_\eta\defeq \lambda k.uk \circ \eta_a:\hom_B(fa,b) \to \hom_A(a,ub)$ is an equivalence for all $a:A$, $b:B$.

*  The type of bi-diagrammatic LARIs of $u$.

Straightening $u$ to be the first projection of a family $P:A \to \UU$
(so that $B \equiv \totalty{P}$),
and strictifying all the occurring data, shows that the types in <ref> and <ref> each are equivalent to the type

\[ \sum_{f:\prod_{a:A} P\,a} \prod_{\substack{x,y:A \\ e:P\,y}} \prod_{\alpha:x \to y} \isContr\big( fx \to_{\alpha}  e\big). \]

By <cit.>, the types of transposing and bi-diagrammatic left adjoints are equivalent to each other and to the type

\[ \sum_{f:A \to B} \sum_{\eta:\id_A \Rightarrow uf} \isEquiv(\varphi_\eta).\]

Hence, the type

\[ \sum_{f:A \to B} \sum_{\eta:\id_A \Rightarrow uf} \isEquiv(\varphi_\eta) \times \isIso(\eta)\]

is equivalent to the type of bi-diagrammatic LARIs of $u$, which establishes equivalences between the types from <ref>. Since the type of bi-diagrammatic left adjoints is a proposition by <cit.>, also the sub-type of bi-diagrammatic LARIs in <ref> is (and consequently, the type in <ref> is as well).

We remark that, in general, given two functors $u : B \to A$ and
$f : A \to B$, whether they determine an adjunction is extra
structure, and not just a proposition, but it is a proposition given
the data that $f$ is a section of $u$ (the proposition being: are the
corresponding transposing maps invertible?).
Similarly, whether $f$ is a section of $u$ is in general extra
structure, but this becomes a proposition when we have the data
of an adjunction (the proposition being: are the units invertible?).

§.§.§ Closure properties of LARI  adjunctions

Let $I:\UU$ be a type, and $A,B:I \to \UU$ families with maps $r_i : B_i \to A_i$.
If there is, for every $i:I$, a (LARI) adjunction

\[
\tikzset{%
every to/.append style={%
edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
\begin{tikzcd}
B(i) \ar[rr, bend right = 25, "r(i)" swap, ""{name=B, below}] && A(i) \ar[ll, bend right = 25, dotted, "\ell(i)" swap, ""{name=A, above}]
\ar[from=B, to=A, symbol=\vdash]
\end{tikzcd}
\]

we get an induced (LARI) adjunction:

\[
\tikzset{%
every to/.append style={%
edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
\begin{tikzcd}
\prod_I B \ar[rr, bend right = 25, "\prod_I r" swap, ""{name=B, below}] && \prod_I A \ar[ll, bend right = 25, dotted, "\prod_I \ell" swap, ""{name=A, above}]
\ar[from=B, to=A, symbol=\vdash]
\end{tikzcd}
\]

By fibrant replacement we consider the straightenings $P_i:A_i \to \UU$, so that $B_i \simeq \widetilde{A_i} \simeq \sum_{a:A_i} P_i(a)$. Writing $\ell_i \defeq \pair{f_i}{L_i}$, the induced map is given by

\[ \prod_i \ell_i : \prod_i A_i \to \prod_i B_i, \quad (\prod_i \ell_i)(\alpha) \jdeq \lambda i. \pair{f_i \, \alpha_i}{L_i \, \alpha_i}.\]

With this, we obtain

\begin{align*}
\hom_{\prod_i B_i}(\prod_i \ell_i \, \alpha, \pair{\alpha'}{\beta'}) & \simeq \prod_i \hom_{B_i}(\ell_i(\alpha_i), \pair{\alpha_i'}{\beta_i'}) \\
& \simeq \prod_i \hom_{B_i}(\pair{f_i \alpha_i}{L_i\alpha_i}, \pair{\alpha_i', \beta_i'}) \\
& \simeq \prod_i \hom_{A_i}(\alpha_i, \alpha_i') \tag{\text{since $\ell_i \dashv r_i$}} \\
& \simeq \hom_{\prod_i A_i}(\alpha, \alpha').
\end{align*}

Thus, adjunctions are closed under taking dependent products. Clearly, this property descends to LARI adjunctions, , the case where $f_i:A_i \to A_i$ is the identity.

LARI adjunctions between Rezk types are stable under pullback, , given a map $r:C \to A$ between Rezk types together with a LARI $\ell: A \to C$ and a map $j: B \to A$ where $B$ is a Rezk type, then the map $r':\jdeq j^*r$ has a LARI as well:

\[\begin{tikzcd}
{D} & {C} \\
{B} & {A}
\arrow[from=1-1, to=1-2]
\arrow["{r'}"{name=0}, from=1-1, to=2-1]
\arrow["{j}"', from=2-1, to=2-2]
\arrow["{r}"{name=1, swap}, from=1-2, to=2-2]
\arrow["{\ell}"{name=2, swap}, from=2-2, to=1-2, curve={height=12pt}, dotted]
\arrow["{\ell'}"{name=3}, from=2-1, to=1-1, curve={height=-12pt}, dotted]
\arrow["\lrcorner"{very near start, rotate=0}, from=1-1, to=2-2, phantom]
\arrow["\dashv"{rotate=-180}, from=2, to=1, phantom]
\arrow["\dashv"{rotate=0}, from=3, to=0, phantom]
\end{tikzcd}\]

We fibrantly replace the square as follows. Denote by $P:A \to \UU$ the family of fibers of the map $j: B \to A$, so that $B \equiv \totalty{P}$, and likewise, $Q:A \to \UU$ the family associated to $r: C \to A$, so that $C \equiv \totalty{Q}$:

\[\begin{tikzcd}
{\sum_{a:A} P\,a \times Q\,a} & {\sum_{a:A}Q\,a} \\
{\sum_{a:A} P\,a} & {A}
\arrow[from=1-1, to=1-2]
\arrow["{r'}"{name=0}, from=1-1, to=2-1]
\arrow["{j}"', from=2-1, to=2-2]
\arrow["{r}"{name=1, swap}, from=1-2, to=2-2]
\arrow["{\ell}"{name=2, swap}, from=2-2, to=1-2, curve={height=12pt}, dotted]
\arrow["{\ell'}"{name=3}, from=2-1, to=1-1, curve={height=-12pt}, dotted]
\arrow["\lrcorner"{very near start, rotate=0}, from=1-1, to=2-2, phantom]
\arrow["\dashv"{rotate=176}, from=2, to=1, phantom]
\arrow["\dashv"{rotate=0}, from=3, to=0, phantom]
\end{tikzcd}\]

The section $\ell'$ is induced by the section $\ell$ by setting $\ell':\jdeq \lambda \pair{a}{e}.\pair{a}{\ell(a)}$.[Here, in the notation we are identifying sections with their “principal parts”.]
The adjunction $\ell \dashv r$ is given by an equivalence

\[ \sum_{\alpha:a \to a'} \ell(a) \to_\alpha e' \equiv \hom_C(\pair{a}{\ell(a)}, \pair{a'}{e'}) \stackrel{\Phi}{\equiv} \hom_A(a,a') \]

giving rise to an equivalence

\begin{align*}
& \sum_{\alpha:a\to a'} (d \to_\alpha d') \times (\ell(a) \to e') \equiv \hom_D(\angled{a,d,\ell(a)}, \angled{a',d',e'}) \\
\stackrel{\Phi'}{\equiv} & \hom_B(\pair{a}{d},\pair{a'}{d'}) \equiv \sum_{\alpha:a \to a'} d \to_\alpha d'
\end{align*}

in sum establishing that $\ell'$ is a left adjoint right inverse of $r'$.

Any two (LARI) adjunctions between Rezk types

\[
\tikzset{%
every to/.append style={%
edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
\begin{tikzcd}
C \ar[rr, bend right = 25, "r'" swap, ""{name=C, below}] && B \ar[ll, bend right = 25, dotted, "\ell'" swap, ""{name=B', above}]
\ar[from=C, to=B', symbol=\vdash]
B \ar[rr, bend right = 25, "r" swap, ""{name=B, below}] && A \ar[ll, bend right = 25, dotted, "\ell" swap, ""{name=A, above}]
\ar[from=B, to=A, symbol=\vdash]
\end{tikzcd}
\]

compose to a (LARI) adjunction:

\[
\tikzset{%
every to/.append style={%
edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
\begin{tikzcd}
C \ar[rr, bend right = 25, "r'r" swap, ""{name=C, below}] && A \ar[ll, bend right = 25, dotted, "\ell'\ell" swap, ""{name=A, above}]
\ar[from=C, to=A, symbol=\vdash]
\end{tikzcd}
\]

By fibrant replacement, we take $r$ and $r'$, resp., to be the projections of families $P:A \to \UU$ and $Q: B \to \UU$, where $B :\jdeq \widetilde{P}$ and $C\defeq \widetilde{Q}$:

\[\begin{tikzcd}
{C} && {B} && {A} \\
{\sum_{\substack{a:A \\ d:P\,a}} Q\,a \, d} && {\sum_{a:A} P\,a}
\arrow["{r'}"{name=0, swap}, from=1-1, to=1-3, curve={height=4pt}]
\arrow["{r}"{name=1, swap}, from=1-3, to=1-5, curve={height=4pt}]
\arrow["{\equiv}" description, from=1-1, to=2-1, phantom, no head]
\arrow["{\equiv}" description, from=1-3, to=2-3, phantom, no head]
\arrow["{\ell'}"{name=2, swap}, from=1-3, to=1-1, curve={height=12pt}]
\arrow["{\ell}"{name=3, swap}, from=1-5, to=1-3, curve={height=12pt}]
\arrow["\dashv"{rotate=-90}, from=2, to=0, phantom]
\arrow["\dashv"{rotate=-90}, from=3, to=1, phantom]
\end{tikzcd}\]

We denote the actions of the maps $\ell$ and $\ell'$ in the following way:

\begin{align*}
\ell \jdeq  \lambda a. &\pair{\ell_0 a}{\ell_1 a} \\
\ell' \jdeq  \lambda \pair{a}{d}.&  \angled{\ell_0' \,a \,d, \ell_1' \,a \,d, \ell_2' \,a \,d}
\end{align*}

The adjunctions $\ell \dashv r$ and $\ell' \dashv r'$ are given by equivalences

\begin{align}
\sum_{\alpha:\ell_0 a \to a'} (\ell_1 a \to_\alpha d') \equiv \hom_B(\ell(a), \pair{a'}{d'}) \stackrel{\Phi}{\equiv} \hom_A(a,a') \label{eq:adj-comp1}
\end{align}

\begin{align}
& \sum_{\substack{\alpha:\ell'_0(a,d) \to a' \\ \beta:\ell_1'(a,d) \to_\alpha d'}}  (\ell'_2(a,d) \to_{\pair{\alpha}{\beta}} e') \equiv \hom_C(\ell'(a,d), \angled{a',d',e'})  \nonumber \\
\stackrel{\Phi'}{\equiv} &  \hom_B(\pair{a}{d}, \pair{a'}{d'}) \equiv \sum_{\alpha:a \to a'} (d \to_\alpha d'), \label{eq:adj-comp2}
\end{align}

The composite of the left adjoints acts as:

\[ \ell''\jdeq \ell' \circ \ell \jdeq \lambda  a. \angled{\ell_0'(\ell_0 a, \ell_1 a),  \ell_1'(\ell_0a, \ell_1a), \ell_2'(\ell_0a, \ell_1a)} \]

This gives rise to an equivalence witnessing the composite adjunction:

\begin{align*}
& \hom_C(\ell''(a), \angled{a',d',e'}) \equiv \sum_{\substack{\alpha:\ell'_0(\ell_0a, \ell_1a) \\ \beta:\ell_1'(\ell_0a, \ell_1a) }} \ell_2'(\ell_0a, \ell_1a) \to_{\pair{\alpha}{\beta}} e' \\
\stackrel{\eqref{eq:adj-comp2}}{\equiv} & \sum_{\alpha:\ell_0a \to a'} \ell_1 a \to_\alpha d' \stackrel{\eqref{eq:adj-comp1}}{\equiv} \hom_A(a,a')
\end{align*}

Furthermore, clearly if both $\ell$ and $\ell'$, resp., happen to be sections of $r$ and $r'$, resp., then $\ell' \circ \ell$ is a section of $r' \circ r$ as can be seen from the above terms defining the functions.

§.§.§ Initial elements in a LARI adjunction

The following lemma is useful in our considerations of cocartesian arrows, in particular in proving their uniqueness up to homotopy ( a fixed source vertex), <ref>.

Recall first the discussion in <ref>.

Suppose $F \dashv U : E \to B$ is a LARI adjunction of Segal types,
and let $b:B$. Then $b$ is initial in $B$ if and only if $F\,b$
is initial in $E$.

The implication from left to right is clear, since
left adjoints preserve initial objects.
[We expect there to be a nice general theory of (co)limits
in simplicial type theory, but here we only need this specific case.]

Conversely, for any $b':B$, since $F$ is fully faithful
we have $\hom_B(b,b') \equiv \hom_E(F\,b, F\,b') \equiv \unit$,
assuming $F\,b$ is initial in $E$.

§.§ Fibered adjunctions

We give a brief treatment of fibered adjunctions which appear in the characterization theorems of cocartesian families and functors, resp., <ref>. We furthermore show that fibered adjunctions over a common base pull back along arbitrary functors, which is used in the main text to show that, for a fibered adjunction between cocartesian fibrations, the fibered left adjoint is always cocartesian, cf. <ref>.

Throughout the subsection, we assume all types to be Rezk.

Let $\pi:E \fibarr B$ and $\xi: F \fibarr A$ be maps. If $\Phi\defeq\pair{k}{\varphi}$ and $\Psi \defeq \pair{m}{\psi}$ each are fibered functors from $\xi$ to $\pi$, then a fibered natural transformation $\Phi$ to $\Psi$ consists of a pair of natural transformations $\mu: k \Rightarrow m$ and $\vartheta: \varphi \Rightarrow \psi$ as indicated in

\[\begin{tikzcd}
F && E \\
\\
A && B
\arrow[""{name=0, anchor=center, inner sep=0}, "\varphi", curve={height=-12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\psi"', curve={height=12pt}, from=1-1, to=1-3]
\arrow["\xi"',from=1-1, to=3-1, two heads]
\arrow[""{name=2, anchor=center, inner sep=0}, "m"', curve={height=12pt}, from=3-1, to=3-3]
\arrow["\pi", from=1-3, to=3-3, two heads]
\arrow[""{name=3, anchor=center, inner sep=0}, "k", curve={height=-12pt}, from=3-1, to=3-3]
\arrow["\vartheta"', shorten <=3pt, shorten >=3pt, Rightarrow, from=0, to=1]
\arrow["\mu"', shorten <=3pt, shorten >=3pt, Rightarrow, from=3, to=2]
\end{tikzcd}\]

together with a witness in

\[ \prod_{a:A, d:Q\,a} \pi(\vartheta_{d}) = \mu_{\xi_{d}}.\]

By fibrant replacement, writing $P\defeq \St_B(\pi)$ and $Q \defeq \St_A(\xi)$, any fibered natural transformation can be presented by the data

* $\mu:\hom_{A \to B}(k,m)$

* $\vartheta:\prod_{\pair{a}{d}:F} \varphi(d) \longrightarrow_{\mu_a}^P \psi(d)$.

We also write shorthand $\vartheta: \varphi \Rightarrow_\mu \psi$.

Over a common base, we obtain that a natural transformation as given in

\[\begin{tikzcd}
F && E \\
\\
& B
\arrow[""{name=0, anchor=center, inner sep=0}, "\varphi", curve={height=-12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\psi"', curve={height=12pt}, from=1-1, to=1-3]
\arrow["\xi"', from=1-1, to=3-2, two heads]
\arrow["\pi", from=1-3, to=3-2, two heads]
\arrow["\vartheta"', shorten <=3pt, shorten >=3pt, Rightarrow, from=0, to=1]
\end{tikzcd}\]

is fibered if and only if all components of $\vartheta$ are vertical arrows (cf. <ref>).

Let $\xi:F \fibarr B$, $\pi:E \fibarr B$ be maps between Rezk types, and fibered functors $\varphi: \xi \to_B \pi$, $\psi: \pi \to_B\xi$. A fibered adjunction (with fibered left adjoint $\psi$ and fibered right adjoint $\varphi$) is an adjunction $\psi \dashv \varphi$ such that for all $\pair{b}{e}:E$, the components $\eta_{b,e}$ of the unit are vertical arrows. We indicate this by writing $\psi \dashv_B \varphi$ or the following diagram:

\[\begin{tikzcd}
F && E \\
\\
& B
\arrow[""{name=0, anchor=center, inner sep=0}, "\psi", curve={height=-12pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "\varphi", curve={height=-12pt}, from=1-3, to=1-1]
\arrow["\xi"', from=1-1, to=3-2, two heads]
\arrow["\pi", from=1-3, to=3-2, two heads]
\arrow["\dashv"{anchor=center, rotate=-90}, draw=none, from=0, to=1]
\end{tikzcd}\]

Given a fibered adjunction $\psi \dashv_B \varphi: F \to_B E$ between cocartesian fibrations $\xi:F \fibarr A$, $\pi:E \fibarr B$, where $P\defeq \St_B(\pi)$, $Q \defeq \St_B(\xi)$, for any map $k:A \to B$ the induced adjunction $\psi' \dashv_B \varphi': k^*F \to_B k^*E$ is again a fibered adjunction:

\[\begin{tikzcd}
{k^*F} & {} && F \\
& {k^*E} &&& E \\
A &&& B
\arrow[""{name=0, anchor=center, inner sep=0}, "\varphi"', curve={height=6pt}, from=1-4, to=2-5]
\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[""{name=1, anchor=center, inner sep=0}, "{\varphi'}"', curve={height=6pt}, dashed, from=1-1, to=2-2]
\arrow["{k^*\xi}"{description}, two heads, from=1-1, to=3-1]
\arrow["k"', from=3-1, to=3-4]
\arrow[from=1-1, to=1-4]
\arrow["{k^*\pi}"{description}, two heads, from=2-2, to=3-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-4]
\arrow[""{name=2, anchor=center, inner sep=0}, "\psi"', curve={height=12pt}, from=2-5, to=1-4]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\psi'}"'{pos=0.4}, curve={height=12pt}, dashed, from=2-2, to=1-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=3-4]
\arrow["\dashv"{anchor=center, rotate=-135}, draw=none, from=2, to=0]
\arrow["\dashv"{anchor=center, rotate=-138}, draw=none, from=3, to=1]
\arrow[from=2-2, to=2-5, crossing over]
\end{tikzcd}\]

Suppose given a fibered adjunction $\psi \dashv_B \varphi$ as indicated with unit

\[ \pair{\id_b}{\eta_{e}}: \pair{b}{e} \to \pair{b}{(\varphi \psi)_b(e)},\]

for $b:B$, $e:P\,b$.
By assumption, for $b':B$, $d':Q\,d'$, this induces an equivalence

\[ \Phi_\eta : \hom_F(\pair{b}{\psi_b(e)}, \pair{b'}{d'}) \to \hom_E(\pair{b}{e}, \pair{b'}{\varphi_b'(d')})\]

\[ \Phi \defeq \Phi_\eta \defeq \lambda u,g.\pair{u}{\varphi_u(g) \circ \eta_e}. \]

For the unit of the adjunction over $A$ we take

\[ \pair{\id_a}{\eta_{e}} : \pair{a}{e} \to \pair{a}{(\psi \varphi)_{ka}(e)}\]

for $a:A$, $e:P(ka)$. This gives rise to the transposing map

\[ \Phi'_\eta : \hom_{k^*F}(\pair{a}{\psi_{ka}(e)}, \pair{a'}{d'}) \to \hom_{k^*E}(\pair{a}{e}, \pair{a'}{\varphi_b'(d')})\]

for $a':A$, $d':Q(ka')$.
Contractibility of the fiber of a pair $\pair{v:a \to a'}{h:e\to_{kv}^P \varphi_b'(d')}$ demands the unique existence of an arrow $g_h:\psi_{ka}(e) \to^P_{v} d'$ such that

\[ \varphi_{kv}(g_h) \circ \eta_{e} = h,\]

which follows from the respective condition for the original map $\Phi$.

§ ACKNOWLEDGEMENTS

The first author acknowledges the support of the Centre for Advanced Study (CAS) at the Norwegian Academy of Science and Letters in Oslo,
Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19. The second author acknowledges the support of CAS and the hospitality of Bjørn Ian Dundas and Marc Bezem on the occasion of several guest visits of the HoTT-UF project during which parts of this work have been carried out.

We wish to greatly thank Steve Awodey, Paolo Capriotti, Denis-Charles Cisinski, Michael Shulman, Thomas Streicher, and Matthew Weaver for many helpful discussions and feedback. We are also thankful to Bastiaan Cnossen who pointed out a flaw in <ref>.

We are particularly grateful to Emily Riehl for numerous continued insightful conversations, and for her hospitality hosting the second author multiple times to discuss this work.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

titleTwo-Level Type Theory and Applications

journaltitleHigher Structures
titleFibrations of $\infty$-categories

Springer International Publishing

booktitle2016 MATRIX Annals
titleFibrations in $\infty$-Category Theory

titleThe stack of higher internal categories and stacks of iterated spans

Cambridge University Press

titleHandbook of Categorical Algebra: Volume 2, Categories and Structures

Springer International Publishing

booktitleReflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts
titleHigher Structures in Homotopy Type Theory

titleUnivalent universes for elegant models of homotopy types

titleLax comma $2$-categories and admissible $2$-functors

Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern

booktitle21st International Conference on Types for Proofs and Programs (TYPES 2015)
seriesLIPIcs. Leibniz Int. Proc. Inform.
titleCubical Type Theory: a constructive interpretation of the univalence axiom

titleSegal objects and the Grothendieck construction

journaltitleDoc. Math.
titleLax Colimits and Free Fibrations in $\infty$-Categories

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleProceedings of the Conference on Categorical Algebra
titleFibred and Cofibred Categories

booktitleRecent Trends in Data Type Specification
titleOn fibred adjunctions and completeness for fibred categories

titleA bicategorical pasting theorem

journaltitleProc. London Math. Soc. (3)
titleOn a topological topos

titleNotes on quasi-categories
.uchicago.edu/ may/IMA/Joyal.pdf

journaltitleJ. Pure Appl. Algebra
noteSpecial volume celebrating the 70th birthday of Professor Max Kelly
titleQuasi-categories and Kan complexes

journaltitleFunct. Anal. Its Appl.
titleYoneda lemma for complete Segal spaces

Cambridge University Press

journaltitleMath. Struct. Comput. Sci.
titleLocal fibred right adjoints are polynomial

noteAgda Formalization
titleMore Fibrations

Princeton University Press

seriesAnnals of Mathematics Studies
titleHigher topos theory

titleA Model for the Higher Category of Higher Categories

titleCartesian Fibrations and Representability

titleCartesian Fibrations of Complete Segal Spaces

titleYoneda Lemma for Simplicial Spaces

journaltitleTrans. Amer. Math. Soc.
titleA model for the homotopy theory of homotopy theory

titleStuff about quasicategories
.illinois.edu/ rezk/quasicats.pdf

noteTalk at the AMS Special Session on Homotopy Type Theory, Joint Mathematics Meetings
titleOn the directed univalence axiom
.jhu.edu/ eriehl/JMM2018-directed-univalence.pdf

journaltitleHigher Structures
titleA type theory for synthetic $\infty$-categories

titleCartesian exponentiation and monadicity

noteBook to appear at Cambridge University Press
titleElements of $\infty$-Category Theory
.jhu.edu/ eriehl/elements.pdf

journaltitleJ. Pure Appl. Algebra
titleFibrations and Yoneda's lemma in an $\infty$-cosmos

journaltitleHigher Structures
titleInfinity category theory from scratch

journaltitleAdvances in Mathematics
titleThe $2$-category theory of quasi-categories

titleClassifying Types, Topics in synthetic homotopy theory

titleIntroduction to Homotopy Type Theory

journaltitleLog. Meth. Comput. Sci.
titleModalities in homotopy type theory
volumeVolume 16, Issue 1

titleAll $(\infty,1)$-toposes have strict univalent universes

journaltitleHomology, Homotopy and Applications
titleThe univalence axiom for elegant Reedy presheaves

booktitleCategory Seminar (Proc. Sem., Sydney, 1972/1973)
titleFibrations and Yoneda's lemma in a $2$-category
pages104133. Lecture Notes in Math.Vol. 420

journaltitleCahiers Topologie Géom. Différentielle
titleFibrations in bicategories

titleFibered Categories à la Jean Benabou
family=Univalent Foundations Program,

Institute for Advanced Study

titleHomotopy Type Theory: Univalent Foundations of Mathematics

Saarbrücken, Germany

Association for Computing Machinery

booktitleProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
seriesLICS '20
titleA Constructive Model of Directed Univalence in Bicubical Sets