···

       
1112
       
1112
       
 
       
  \begin{enumerate}

     

       
1113
       
1113
       
 
       
  \item The type $C$ is Sierpi\'nski complete.

     

       
1114
       
1114
       
 
       
  \item The type $C$ is internally right orthogonal to the comparison map

     

       
1115
       
1115
       
-
       
  \[ \OpenMCyl_{(x:B)}E[x]\to \Lift_{(x:B)}E[x]\] from the geometrical to the logical for each family of $\IsF{1}$-connected types $x:B\vdash E[x]$.

     

       
1115
       
1115
       
+
       
  \[ \OpenMCyl_{(x:B)}E[x]\to \Lift_{(x:B)}E[x]\] from the geometrical to the logical open fibre cylinder for each family of $\IsF{1}$-connected types $x:B\vdash E[x]$.

     

       
1116
       
1116
       
 
       
  \item The type $C$ is internally right orthogonal to the comparison map \[ \OpenMCyl_B(f)\to \Lift_B(f)\] for each $\IsF{1}$-connected function $f\colon E\to B$.

     

       
1117
       
1117
       
 
       
  \end{enumerate}

     

       
1118
       
1118
       
 
       
\end{theorem}