···

       
1137
       
 
       
  in which we aim to verify that the left-hand map is an equivalence. The upper and lower maps are the dependent currying equivalences, and the eastern map is the functorial action of the \emph{product} functor on the family of equivalences given by the Sierpi\'nski completeness of $C$. By the three-for-two property of equivalences, it follows that the left-hand map is an equivalence.

     

       
1138
       
 
       
\end{proof}

     

       
1139
       
 
       


     

       
1140
       
-
       
The thrust of \cref{thm:sierpinski-completeness-mapping-cylinders} is to say that in any subuniverse in which partial map classifiers exist and satisfy the universal property of the Sierpi\'nski cone, it \emph{also} follows that logical mapping cylinders (if they exist) must satisfy the universal property of (geometrical) mapping cylinders.

     

       
1141
       
 
       


     

       
1142
       
 
       
\subsubsection{From upper Segal to Sierpi\'nski completeness}

     

       
1143
       
 
       


     

···

       
1137
       
 
       
  in which we aim to verify that the left-hand map is an equivalence. The upper and lower maps are the dependent currying equivalences, and the eastern map is the functorial action of the \emph{product} functor on the family of equivalences given by the Sierpi\'nski completeness of $C$. By the three-for-two property of equivalences, it follows that the left-hand map is an equivalence.

     

       
1138
       
 
       
\end{proof}

     

       
1139
       
 
       


     

       
1140
       
+
       
The thrust of \cref{thm:sierpinski-completeness-mapping-cylinders} is to say that in any subuniverse in which partial map classifiers exist and satisfy the universal property of the Sierpi\'nski cone, it \emph{also} follows that logical mapping cylinders (if they exist) must satisfy the universal property of (geometrical) mapping cylinders. Of course, a dual result relating inverted Sierpi\'nski completeness to the \emph{closed} fibre/mapping cylinders follows by considering \cref{thm:sierpinski-completeness-mapping-cylinders} with respect to $\J\Op$.

     

       
1141
       
 
       


     

       
1142
       
 
       
\subsubsection{From upper Segal to Sierpi\'nski completeness}

     

       
1143