natural model si

Notes/natural_model_univ/groupoid_model.tex

@@ -805,27 +805,103 @@ \subsection{$\Pi$ and $\Si$ structure}
 
 \medskip
 
+\begin{defn}[Evaluation]
+  Define the operation of evaluation $\ev{}{}$ to take
+  $\al : \Ga \to \ptgrpd$ and $B : \Ga \cdot U \circ \al \to \grpd$
+  and return $\ev{\al}{B} : \Ga \to \grpd$, described below.
+ % https://q.uiver.app/#q=WzAsOCxbMiwxLCJcXFBvbHlfXFx0cCB7XFxUeXBlfSJdLFsyLDIsIlxcVHlwZSJdLFsxLDEsIlxcVGVybSBcXHRpbWVzX3tcXFR5cGV9IFxcUG9seV9cXHRwIFxcVHlwZSJdLFsxLDIsIlxcVG0iXSxbMCwyLCJcXFRlcm0gXFx0aW1lcyBcXFR5cGUiXSxbMCwzLCJcXFRlcm0iXSxbMSwzLCJcXHRlcm1pbmFsIl0sWzAsMCwiXFxHYSJdLFswLDEsIlxcdHBfKiBcXFRlcm1eKiBcXFR5cGUiXSxbMiwwXSxbMiwzXSxbMywxLCJcXHRwIiwyXSxbMiwxLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbMiw0LCJcXGNvdW5pdCIsMV0sWzQsM10sWzQsNV0sWzUsNl0sWzMsNl0sWzQsNiwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzcsMCwiXFxiZSIsMV0sWzcsMywiXFxhbCIsMSx7ImxhYmVsX3Bvc2l0aW9uIjoyMH1dLFs3LDUsIlxcZXZ7XFxhbH17Qn0iLDEseyJjdXJ2ZSI6NX1dLFs3LDIsIihcXGFsLFxcYmUpIiwxLHsibGFiZWxfcG9zaXRpb24iOjcwfV1d
+\[\begin{tikzcd}
+	\Ga \\
+	& {\Term \times_{\Type} \Poly{\tp} \Type} & {\Poly{\tp} {\Type}} \\
+	{\Term \times \Type} & \Term & \Type \\
+	\Type & \terminal
+	\arrow["{(\al,\be)}"{description, pos=0.7}, from=1-1, to=2-2]
+	\arrow["\be"{description}, bend left, from=1-1, to=2-3]
+	\arrow["\al"{description, pos=0.2}, from=1-1, to=3-2]
+	\arrow["{\ev{\al}{B}}"{description}, dashed, bend right = 50, from=1-1, to=4-1]
+	\arrow[from=2-2, to=2-3]
+	\arrow["\counit"{description}, from=2-2, to=3-1]
+	\arrow[from=2-2, to=3-2]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
+	\arrow["{\tp_* \Term^* \Type}", from=2-3, to=3-3]
+	\arrow[from=3-1, to=3-2]
+	\arrow[from=3-1, to=4-1]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=3-1, to=4-2]
+	\arrow["\tp"', from=3-2, to=3-3]
+	\arrow[from=3-2, to=4-2]
+	\arrow[from=4-1, to=4-2]
+\end{tikzcd}\]
+  The input data corresponds to
+  $\al : \Ga \to \Term$ and
+  and some $\be : \Ga \to \Poly{\tp}{\Type}$ such that
+  \[\tp_{*}\Term^{*} \Type \circ \be = \tp \circ \al\]
+  This in turn corresponds to a map into the fiber product
+  \[(\al, \be) : \Ga \to \tp \times_{\Type} \tp_{*}\Term^{*} \Type\]
+  We then compose this the counit of the adjunction $\tp^{*} \dashv \tp_{*}$
+  to get
+  \[\counit \circ (\al, \be) : \Ga \to \tp \times_{\Type} \tp_{*} \Type\]
+  then extract the type by composing with the projection to $\Type$
+  \[\Type^{*} \Term \circ \counit \circ (\al, \be) : \Ga \to \Type\]
+  Finally, this corresponds to a unique map
+  $\ev{\al}{B} : \Ga \to \grpd$.
+\end{defn}
+
+\medskip
+
+\begin{defn}[Classifier for dependent pairs]
+  Recall the following definition of composition of polynomial endofunctors,
+  specialized to our situation
+% https://q.uiver.app/#q=WzAsMTEsWzMsMCwiXFxQb2x5e1xcdHB9IHtcXFR5cGV9Il0sWzMsMSwiXFxUeXBlIl0sWzIsMF0sWzIsMSwiXFxUZXJtIl0sWzEsMSwiXFxUZXJtIFxcdGltZXMgXFxUeXBlIl0sWzEsMiwiXFxUeXBlIl0sWzIsMiwiXFx0ZXJtaW5hbCJdLFswLDEsIlxcVGVybSBcXHRpbWVzIFxcVGVybSJdLFswLDIsIlxcVGVybSJdLFsxLDBdLFswLDAsIlEiXSxbMCwxLCJcXHRwXyogXFxUZXJtXiogXFxUeXBlIl0sWzIsMF0sWzIsM10sWzMsMSwiXFx0cCIsMl0sWzIsMSwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzQsM10sWzQsNV0sWzUsNl0sWzMsNl0sWzQsNiwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzcsNF0sWzcsOF0sWzgsNSwiXFx0cCIsMl0sWzcsNSwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzEwLDddLFsxMCw0LCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbOSwyLCJcXFRlcm0gXFx0aW1lc197XFxUeXBlfSBcXFBvbHl7XFx0cH0gXFxUeXBlIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzEwLDldLFs5LDQsIlxcY291bml0IiwxXSxbMTAsMCwiXFx0cCBcXHRyaWFuZ2xlbGVmdCBcXHRwIiwxLHsiY3VydmUiOi0zfV1d
+\[\begin{tikzcd}
+	Q & {} & {} & {\Poly{\tp} {\Type}} \\
+	{\Term \times \Term} & {\Term \times \Type} & \Term & \Type \\
+	\Term & \Type & \terminal
+	\arrow[from=1-1, to=1-2]
+	\arrow["{\tp \triangleleft \tp}"{description}, bend left, from=1-1, to=1-4]
+	\arrow[from=1-1, to=2-1]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+	\arrow["{\Term \times_{\Type} \Poly{\tp} \Type}"{description}, draw=none, from=1-2, to=1-3]
+	\arrow["\counit"{description}, from=1-2, to=2-2]
+	\arrow[from=1-3, to=1-4]
+	\arrow[from=1-3, to=2-3]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4]
+	\arrow["{\tp_* \Term^* \Type}", from=1-4, to=2-4]
+	\arrow[from=2-1, to=2-2]
+	\arrow[from=2-1, to=3-1]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2]
+	\arrow[from=2-2, to=2-3]
+	\arrow[from=2-2, to=3-2]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3]
+	\arrow["\tp"', from=2-3, to=2-4]
+	\arrow[from=2-3, to=3-3]
+	\arrow["\tp"', from=3-1, to=3-2]
+	\arrow[from=3-2, to=3-3]
+\end{tikzcd}\]
+  Then $Q$ classifies the data of a pair of dependent terms $(a, b)$,
+  and $\tp \triangleleft \tp$
+  extracts the underlying type and dependent type $(A, B)$.
+\end{defn}
+
+\medskip
+
 \begin{defn}[Interpretation of $\Si$]
-  Sketch: we define the natural transformation
+  We define the natural transformation
   $\Si : \Poly{\tp} \Type \to \Type$
-  by first taking some small groupoid $\Ga$ and defining
-  \[\Si_{\Ga} : \Pshgrpd(\Ga, \Poly{\tp} \Type) \to \Pshgrpd(\Ga, \Type)\]
-  Again,
-  this amounts to taking a pair of composable groupoid fibrations
-  to a single groupoid fibration on the codomain
-  % https://q.uiver.app/#q=WzAsNixbMCwxLCJcXEdhIFxcY2RvdCBBIl0sWzAsMCwiXFxHYSBcXGNkb3QgQSBcXGNkb3QgQiJdLFsxLDEsIlxcR2EiXSxbMywwLCJcXEdhIFxcY2RvdCBcXFNpX0EgQiJdLFszLDEsIlxcR2EiXSxbMiwwLCJcXG1hcHN0byJdLFsxLDAsIlxcZGlzcHtCfSIsMix7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFswLDIsIlxcZGlzcHtBfSIsMix7InN0eWxlIjp7ImhlYWQiOnsibmFtZSI6ImVwaSJ9fX1dLFszLDQsIihcXGRpc3B7QX0pXyEgXFxkaXNwe0J9IiwwLHsic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoiZXBpIn19fV1d
-  \[\begin{tikzcd}
-    {\Ga \cdot A \cdot B} && \mapsto & {\Ga \cdot \Si_A B} \\
-    {\Ga \cdot A} & \Ga && \Ga
-    \arrow["{\disp{B}}"', two heads, from=1-1, to=2-1]
-    \arrow["{(\disp{A})_! \disp{B}}", two heads, from=1-4, to=2-4]
-    \arrow["{\disp{A}}"', two heads, from=2-1, to=2-2]
-  \end{tikzcd}\]
-  As indicated in the diagram, we take this to be the composition of
-  $\disp{B}$ and $\disp{A}$,
-  recalling that fibrations are closed under composition.
+  as that which is induced (\cref{BC_iff_nat_trans}) by the $\Si$-former operation (\cref{pi_classifier_op}).
 
-  TODO: define $\pair$.
+  Define $\pair : Q \to \Term$ such that TODO.
+
+  $\Si$ and $\pair$ combine to give us a pullback square
+% https://q.uiver.app/#q=WzAsNCxbMCwwLCJRIl0sWzAsMSwiXFxQb2x5e1xcdHB9e1xcVHlwZX0iXSxbMSwwLCJcXFRlcm0iXSxbMSwxLCJcXFR5cGUiXSxbMCwxLCJcXHRwIFxcdHJpYW5nbGVsZWZ0IFxcdHAiLDJdLFswLDIsIlxccGFpciJdLFsyLDMsIlxcdHAiXSxbMSwzLCJcXFNpIiwyXSxbMCwzLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0=
+\[\begin{tikzcd}
+	Q & \Term \\
+	{\Poly{\tp}{\Type}} & \Type
+	\arrow["\pair", from=1-1, to=1-2]
+	\arrow["{\tp \triangleleft \tp}"', from=1-1, to=2-1]
+	\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
+	\arrow["\tp", from=1-2, to=2-2]
+	\arrow["\Si"', from=2-1, to=2-2]
+\end{tikzcd}\]
 \end{defn}
 \begin{proof}
   TODO: naturality.

Notes/natural_model_univ/main.tex

@@ -64,8 +64,10 @@
 \newcommand{\E}{\mathsf{E}}
 \newcommand{\El}{\mathsf{El}}
 \newcommand{\Poly}[1]{\mathsf{Poly}_{#1}}
-\newcommand{\pair}{\textsf{pair}}
-\newcommand{\fst}{\textsf{fst}}
+\newcommand{\pair}{\mathsf{pair}}
+\newcommand{\fst}{\mathsf{fst}}
+\newcommand{\ev}[2]{\mathsf{ev}_{#1} \, #2}
+\newcommand{\counit}{\mathsf{counit}}
 
 \newcommand{\Fib}{\mathsf{Fib}}
 \newcommand{\lift}[2]{\mathsf{lift} \, #1 \, #2}