diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index f02f011..e5300da 100644 Binary files a/blueprint/print/print.pdf and b/blueprint/print/print.pdf differ diff --git a/blueprint/src/groupoid_model.tex b/blueprint/src/groupoid_model.tex index dc65a9f..759c608 100644 --- a/blueprint/src/groupoid_model.tex +++ b/blueprint/src/groupoid_model.tex @@ -580,20 +580,20 @@ \subsection{Classifying type dependency} \quad \quad B : \Ga \cdot A \to X \] - which by Yoneda corresponds to the data in $\Cat$ of + The special case of when $X$ is also $\Type$ gives us a + classifier for dependent types; + by Yoneda the above corresponds to the data in $\Cat$ of \[ A : \Ga \to \grpd \quad \quad \text{ and } \quad \quad - B : \Ga \cdot A \to X + B : \Ga \cdot A \to \grpd \] - The special case of when $X$ is also $\Type$ gives us a - classifier for dependent types. - Furthermore, if $\si : \De \to \Ga$ were a representable map, - then we have -% https://q.uiver.app/#q=WzAsNCxbMiwxLCJcXFBvbHl7XFx0cH0gWCJdLFswLDFdLFsxLDEsIlxcR2EiXSxbMSwwLCJcXERlIl0sWzMsMiwiXFxzaSIsMl0sWzMsMCwiKEFcXGNpcmMgXFxzaSwgQiBcXGNpcmMgXFx0cF4qIFxcc2kpIl0sWzIsMCwiKEEsIEIpIiwyXV0= + Furthermore, precomposition by a substitution $\si : \De \to \Ga$ acts on + such a pair by + % https://q.uiver.app/#q=WzAsNCxbMiwxLCJcXFBvbHl7XFx0cH0gWCJdLFswLDFdLFsxLDEsIlxcR2EiXSxbMSwwLCJcXERlIl0sWzMsMiwiXFxzaSIsMl0sWzMsMCwiKEFcXGNpcmMgXFxzaSwgQiBcXGNpcmMgXFx0cF4qIFxcc2kpIl0sWzIsMCwiKEEsIEIpIiwyXV0= \[\begin{tikzcd} & \De \\ {} & \Ga & {\Poly{\tp} X} @@ -700,35 +700,42 @@ \subsection{Pi and Sigma structure} %% TODO fix subsection title The square commutes and is a pullback if and only it pointwise commutes and pointwise gives pullbacks, i.e. for each groupoid $\Ga$ - % https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXFBvbHl7XFx0cH17XFxUZXJtfSBcXEdhIl0sWzAsMSwiXFxQb2x5e1xcdHB9e1xcVHlwZX0gXFxHYSJdLFsxLDAsIltcXEdhLFxccHRncnBkXSJdLFsxLDEsIltcXEdhLFxcZ3JwZF0iXSxbMCwxLCJcXFBvbHl7XFx0cH17XFx0cH1fXFxHYSIsMl0sWzAsMiwiXFxsYV9cXEdhIl0sWzIsMywiVSBcXGNpcmMgLSJdLFsxLDMsIlxcUGlfXFxHYSIsMl0sWzAsMywiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d +% https://q.uiver.app/#q=WzAsOSxbMSwxLCJcXFBzaGdycGQoXFxHYSxcXFBvbHl7XFx0cH17XFxUZXJtfSkiXSxbMSwyLCJcXFBzaGdycGQoXFxHYSxcXFBvbHl7XFx0cH17XFxUeXBlfSkiXSxbMiwxLCJbXFxHYSxcXHB0Z3JwZF0iXSxbMiwyLCJbXFxHYSxcXGdycGRdIl0sWzAsMCwiKEEsXFxiZSkiXSxbMCwzLCIoQSxVXFxjaXJjIFxcYmUpIl0sWzMsMCwiXFxsYV9BIFxcYmUiXSxbMywzLCJVIFxcY2lyYyBcXGxhX0EgXFxiZSJdLFsyLDMsIlxcUGlfXFxHYSBVIFxcY2lyYyBcXGJlIl0sWzAsMSwiXFxQc2hncnBkKFxcR2EsIFxcUG9seXtcXHRwfXtcXHRwfSkiLDJdLFswLDIsIlxcbGFfXFxHYSJdLFsyLDMsIlUgXFxjaXJjIC0iXSxbMSwzLCJcXFBpX1xcR2EiLDJdLFswLDMsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDUsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbNCw2LCIiLDIseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV0sWzYsNywiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs1LDgsIiIsMCx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1hcHMgdG8ifX19XSxbOCw3LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ== \[\begin{tikzcd} - {\Poly{\tp}{\Term} \, \Ga} & {[\Ga,\ptgrpd]} \\ - {\Poly{\tp}{\Type} \, \Ga} & {[\Ga,\grpd]} - \arrow["{\la_\Ga}", from=1-1, to=1-2] - \arrow["{\Poly{\tp}{\tp}_\Ga}"', from=1-1, to=2-1] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] - \arrow["{U \circ -}", from=1-2, to=2-2] - \arrow["{\Pi_\Ga}"', from=2-1, to=2-2] -\end{tikzcd}\] - -by \cref{tp_classifies} this holds if and only if -% https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXFNpX3tBIFxcaW4gW1xcR2EsXFxncnBkXX0gIFtcXEdhLkEsXFxwdGdycGRdIl0sWzAsMSwiXFxTaV97QSBcXGluIFtcXEdhLFxcZ3JwZF19ICBbXFxHYS5BLFxcZ3JwZF0iXSxbMSwwLCJbXFxHYSxcXHB0Z3JwZF0iXSxbMSwxLCJbXFxHYSxcXGdycGRdIl0sWzAsMSwiKC0gXFxjaXJjIFxcc2ksLSBcXGNpcmMgXFxzaV9BKSIsMl0sWzAsMiwiXFxsYSJdLFsyLDMsIlUgXFxjaXJjIC0iXSxbMSwzLCJcXFBpIiwyXSxbMCwzLCIiLDAseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0= -\[\begin{tikzcd} - {\Si_{A \in [\Ga,\grpd]} [\Ga.A,\ptgrpd]} & {[\Ga,\ptgrpd]} \\ - {\Si_{A \in [\Ga,\grpd]} [\Ga.A,\grpd]} & {[\Ga,\grpd]} - \arrow["\la", from=1-1, to=1-2] - \arrow["{(- \circ \si,- \circ \si_A)}"', from=1-1, to=2-1] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] - \arrow["{U \circ -}", from=1-2, to=2-2] - \arrow["\Pi"', from=2-1, to=2-2] + {(A,\be)} &&& {\la_A \be} \\ + & {\Pshgrpd(\Ga,\Poly{\tp}{\Term})} & {[\Ga,\ptgrpd]} \\ + & {\Pshgrpd(\Ga,\Poly{\tp}{\Type})} & {[\Ga,\grpd]} \\ + {(A,U\circ \be)} && {\Pi_\Ga U \circ \be} & {U \circ \la_A \be} + \arrow[maps to, from=1-1, to=1-4] + \arrow[maps to, from=1-1, to=4-1] + \arrow[maps to, from=1-4, to=4-4] + \arrow["{\la_\Ga}", from=2-2, to=2-3] + \arrow["{\Pshgrpd(\Ga, \Poly{\tp}{\tp})}"', from=2-2, to=3-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] + \arrow["{U \circ -}", from=2-3, to=3-3] + \arrow["{\Pi_\Ga}"', from=3-2, to=3-3] + \arrow[maps to, from=4-1, to=4-3] + \arrow[Rightarrow, no head, from=4-3, to=4-4] \end{tikzcd}\] + where we have used \cref{tp_classifies}. + That this commutes follows from the definitions of $\Pi$ and $\la$. + + To show it is pullback it suffices to note that for any $f : \Ga \to \ptgrpd$ + and $(A,B) : \Ga \to \Poly{\tp} \Type$ such that $U \circ f = \Pi_{A} B$, + there exists a unique $(A, \be) : \Ga \to \Poly{\tp} \Term$ such that + $U \circ \be = B$ and $\la_{A} \be = f$. + Indeed $\be$ is fully determined by the above conditions to be + \begin{align*} + \be : \Ga \cdot A & \to \ptgrpd \\ + (x, a) & \mapsto (B(x,a), f \, x \, a) + \end{align*} -which follows from the definitions of $\Pi$ and $\la$. \end{proof} \medskip -\begin{lemma}\label{R_classifies} +\begin{lemma}\label{R_classifies_tp} + This is a specialization of \cref{R_classifies}. Use $R$ to denote the fiber product % https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXFBvbHl7XFx0cH0ge1xcVHlwZX0iXSxbMSwxLCJcXFR5cGUiXSxbMCwwLCJSIl0sWzAsMSwiXFxUZXJtIl0sWzAsMSwiXFx0cF8qIFxcVGVybV4qIFxcVHlwZSJdLFsyLDAsIlxccmhvX1xcUG9seXt9Il0sWzIsMywiXFx0cF4qIFxcdHBfKiBcXFRlcm1eKiBcXFR5cGU9IFxccmhvX1xcVGVybSIsMl0sWzMsMSwiXFx0cCIsMl0sWzIsMSwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d \[\begin{tikzcd} @@ -762,8 +769,15 @@ \subsection{Pi and Sigma structure} %% TODO fix subsection title \arrow["\tp"', from=3-2, to=3-3] \end{tikzcd}\] - Precomposition by a substitution $\si : \De \to \Ga$ then act on such a pair by - \[ (\al, B) \mapsto (\al \circ \si, B \circ \si_{U \circ \al})\] + Precomposition by a substitution $\si : \De \to \Ga$ then acts on such a pair by +% https://q.uiver.app/#q=WzAsNCxbMiwxLCJSIl0sWzAsMV0sWzEsMSwiXFxHYSJdLFsxLDAsIlxcRGUiXSxbMywyLCJcXHNpIiwyXSxbMywwLCIoXFxhbCBcXGNpcmMgXFxzaSwgQiBcXGNpcmMgXFx0cF4qXFxzaSkiXSxbMiwwLCIoXFxhbCwgQikiLDJdXQ== +\[\begin{tikzcd} + & \De \\ + {} & \Ga & R + \arrow["\si"', from=1-2, to=2-2] + \arrow["{(\al \circ \si, B \circ \tp^*\si)}", from=1-2, to=2-3] + \arrow["{(\al, B)}"', from=2-2, to=2-3] +\end{tikzcd}\] \end{lemma} \medskip @@ -827,90 +841,94 @@ \subsection{Pi and Sigma structure} %% TODO fix subsection title \end{tikzcd}\] \end{lemma} \begin{proof} - Since $\counit = (\ev{}{}, \rho_{\Term}) : R \to \Type$, - it suffices to find out how the counit computes. - The adjunction $\tp^{*} \dashv \tp_{*}$ - suggests that we use the way - \[ \widetilde{\counit} = \id_{\Poly{\tp}\Type}\] - computes. Namely for any $A : \Ga \to \grpd$ and $B : \Ga \cdot A \to \grpd$ - \begin{equation} - \widetilde{\counit} \circ (A, B) = (A, B) : \Ga \to \Poly{\tp}\Type - \label{evaluation_computation_equation1} - \end{equation} - - Working on both sides of \cref{evaluation_computation_equation1} we get - \begin{align*} - & (\ev{\var_{A}}{B} \circ U^{*}\disp{A}, \var_{A}) \\ - = \, & (\ev{}{}, \rho_{\Type}) \circ (\var_{A}, B \circ U^{*}(\disp{A})) \\ - = \, & (\ev{}{}, \rho_{\Type}) \circ \tp^{*} (A, B) - & \cref{evaluation_computation_diagram1} \\ - = \, & \counit \circ \tp^{*} (A, B) \\ - = \, & \overline{\widetilde{\counit} \circ (A, B)} \\ - = \, & \overline{(A, B)} \\ - = \, & (B, \var_{A}) - \end{align*} - Hence we know that evaluation of $B$ - (weakened to the context $\Ga \cdot A \cdot A$) - on a variable of type $A$ - is just $B$. - \[ \ev{\var_{A}}{B} \circ U^{*}\disp{A} = B\] - % diagrams TODO - - Then the naturality square for the natural transformation - $\ev{}{} : R \to \Type$ on $a : \Ga \to \Ga \cdot A$ - tells us that - \begin{align*} - & \ev{\al}{B} \\ - = \, & \ev{\Ga}{} (\al, B) \\ - = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} (\id_{\Ga}) \\ - = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} (\disp{A} \circ a)) \\ - = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} \disp{A} \circ U^{*} a) \\ - = \, & \ev{\Ga}{} ((\var_{A}, B \circ \U^{*} \disp{A}) \circ a) \\ - = \, & (\ev{\Ga \cdot A}{} (\var_{A}, B \circ \U^{*} \disp{A}) \circ a - & \text{by naturality}\\ - = \, & (\ev{\var_{A}}{B \circ \U^{*} \disp{A}}) \circ a \\ - = \, & B \circ a - \end{align*} - - - \begin{figure} -\centering -\begin{subfigure}{.5\textwidth} - \centering -% https://q.uiver.app/#q=WzAsNixbMSwxLCJcXFBvbHl7XFx0cH0ge1xcVHlwZX0iXSxbMSwyLCJcXFR5cGUiXSxbMCwxLCJSIl0sWzAsMiwiXFxUZXJtIl0sWzEsMCwiXFxHYSJdLFswLDAsIlxcR2EgXFxjZG90IEEiXSxbMCwxLCJcXHRwXyogXFxUZXJtXiogXFxUeXBlIiwxXSxbMiwwLCJcXHJob197XFxQb2x5e319Il0sWzIsMywiXFxyaG9fXFxUZXJtIiwxXSxbMywxLCJcXHRwIiwyXSxbMiwxLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbNCwwLCIoQSxCKSIsMV0sWzUsNCwiXFxkaXNwe0F9Il0sWzUsMiwiXFx0cF4qKEEsQikiLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNSwzLCJcXHZhcl9BIiwyLHsiY3VydmUiOjR9XSxbNCwxLCJBIiwwLHsiY3VydmUiOi00fV1d -\begin{tikzcd} - {\Ga \cdot A} & \Ga \\ - R & {\Poly{\tp} {\Type}} \\ - \Term & \Type - \arrow["{\disp{A}}", from=1-1, to=1-2] - \arrow["{\tp^*(A,B)}"{description}, dashed, from=1-1, to=2-1] - \arrow["{\var_A}"', bend right = 60, from=1-1, to=3-1] - \arrow["{(A,B)}"{description}, from=1-2, to=2-2] - \arrow["A", bend left = 60, from=1-2, to=3-2] - \arrow["{\rho_{\Poly{}}}", from=2-1, to=2-2] - \arrow["{\rho_\Term}"{description}, from=2-1, to=3-1] - \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] - \arrow["{\tp_* \Term^* \Type}"{description}, from=2-2, to=3-2] - \arrow["\tp"', from=3-1, to=3-2] -\end{tikzcd} - \caption{$\tp^{*}(A,B)$} -\end{subfigure}% -\begin{subfigure}{.5\textwidth} - \centering - \begin{align*} - & \rho_{\Poly{}} \circ \tp^*(A,B) \\ - = \, & (A, B) \circ \disp{A} \\ - = \, & (A \circ \disp{A}, B \circ U^{*}\disp{A}) \\ - \text{Hence} - \end{align*} - \caption{$\tp^{*}(A,B) = (\var_{A}, B \circ U^{*}\disp{A})$} - \label{evaluation_computation_diagram1} -\end{subfigure} -\end{figure} - % (\var_{A}, B \circ \tp^* \disp_A) - - + This is a specialization of \cref{evaluation} + with liberal applications of Yoneda. \end{proof} +% \begin{proof} +% Since $\counit = (\ev{}{}, \rho_{\Term}) : R \to \Type$, +% it suffices to find out how the counit computes. +% The adjunction $\tp^{*} \dashv \tp_{*}$ +% suggests that we use the way +% \[ \widetilde{\counit} = \id_{\Poly{\tp}\Type}\] +% computes. Namely for any $A : \Ga \to \grpd$ and $B : \Ga \cdot A \to \grpd$ +% \begin{equation} +% \widetilde{\counit} \circ (A, B) = (A, B) : \Ga \to \Poly{\tp}\Type +% \label{evaluation_computation_equation1} +% \end{equation} + +% Working on both sides of \cref{evaluation_computation_equation1} we get +% \begin{align*} +% & (\ev{\var_{A}}{B} \circ U^{*}\disp{A}, \var_{A}) \\ +% = \, & (\ev{}{}, \rho_{\Type}) \circ (\var_{A}, B \circ U^{*}(\disp{A})) \\ +% = \, & (\ev{}{}, \rho_{\Type}) \circ \tp^{*} (A, B) +% & \cref{evaluation_computation_diagram1} \\ +% = \, & \counit \circ \tp^{*} (A, B) \\ +% = \, & \overline{\widetilde{\counit} \circ (A, B)} \\ +% = \, & \overline{(A, B)} \\ +% = \, & (B, \var_{A}) +% \end{align*} +% Hence we know that evaluation of $B$ +% (weakened to the context $\Ga \cdot A \cdot A$) +% on a variable of type $A$ +% is just $B$. +% \[ \ev{\var_{A}}{B} \circ U^{*}\disp{A} = B\] +% % diagrams TODO + +% Then the naturality square for the natural transformation +% $\ev{}{} : R \to \Type$ on $a : \Ga \to \Ga \cdot A$ +% tells us that +% \begin{align*} +% & \ev{\al}{B} \\ +% = \, & \ev{\Ga}{} (\al, B) \\ +% = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} (\id_{\Ga}) \\ +% = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} (\disp{A} \circ a)) \\ +% = \, & \ev{\Ga}{} (\var_{A} \circ a, B \circ \U^{*} \disp{A} \circ U^{*} a) \\ +% = \, & \ev{\Ga}{} ((\var_{A}, B \circ \U^{*} \disp{A}) \circ a) \\ +% = \, & (\ev{\Ga \cdot A}{} (\var_{A}, B \circ \U^{*} \disp{A}) \circ a +% & \text{by naturality}\\ +% = \, & (\ev{\var_{A}}{B \circ \U^{*} \disp{A}}) \circ a \\ +% = \, & B \circ a +% \end{align*} + + +% \begin{figure} +% \centering +% \begin{subfigure}{.5\textwidth} +% \centering +% % https://q.uiver.app/#q=WzAsNixbMSwxLCJcXFBvbHl7XFx0cH0ge1xcVHlwZX0iXSxbMSwyLCJcXFR5cGUiXSxbMCwxLCJSIl0sWzAsMiwiXFxUZXJtIl0sWzEsMCwiXFxHYSJdLFswLDAsIlxcR2EgXFxjZG90IEEiXSxbMCwxLCJcXHRwXyogXFxUZXJtXiogXFxUeXBlIiwxXSxbMiwwLCJcXHJob197XFxQb2x5e319Il0sWzIsMywiXFxyaG9fXFxUZXJtIiwxXSxbMywxLCJcXHRwIiwyXSxbMiwxLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbNCwwLCIoQSxCKSIsMV0sWzUsNCwiXFxkaXNwe0F9Il0sWzUsMiwiXFx0cF4qKEEsQikiLDEseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNSwzLCJcXHZhcl9BIiwyLHsiY3VydmUiOjR9XSxbNCwxLCJBIiwwLHsiY3VydmUiOi00fV1d +% \begin{tikzcd} +% {\Ga \cdot A} & \Ga \\ +% R & {\Poly{\tp} {\Type}} \\ +% \Term & \Type +% \arrow["{\disp{A}}", from=1-1, to=1-2] +% \arrow["{\tp^*(A,B)}"{description}, dashed, from=1-1, to=2-1] +% \arrow["{\var_A}"', bend right = 60, from=1-1, to=3-1] +% \arrow["{(A,B)}"{description}, from=1-2, to=2-2] +% \arrow["A", bend left = 60, from=1-2, to=3-2] +% \arrow["{\rho_{\Poly{}}}", from=2-1, to=2-2] +% \arrow["{\rho_\Term}"{description}, from=2-1, to=3-1] +% \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=3-2] +% \arrow["{\tp_* \Term^* \Type}"{description}, from=2-2, to=3-2] +% \arrow["\tp"', from=3-1, to=3-2] +% \end{tikzcd} +% \caption{$\tp^{*}(A,B)$} +% \end{subfigure}% +% \begin{subfigure}{.5\textwidth} +% \centering +% \begin{align*} +% & \rho_{\Poly{}} \circ \tp^*(A,B) \\ +% = \, & (A, B) \circ \disp{A} \\ +% = \, & (A \circ \disp{A}, B \circ U^{*}\disp{A}) \\ +% \text{Hence} +% \end{align*} +% \caption{$\tp^{*}(A,B) = (\var_{A}, B \circ U^{*}\disp{A})$} +% \label{evaluation_computation_diagram1} +% \end{subfigure} +% \end{figure} +% % (\var_{A}, B \circ \tp^* \disp_A) + + +% \end{proof} \medskip diff --git a/blueprint/src/polynomial.tex b/blueprint/src/polynomial.tex index 57e4124..4b4e803 100644 --- a/blueprint/src/polynomial.tex +++ b/blueprint/src/polynomial.tex @@ -74,7 +74,7 @@ \quad \quad \text{ and } \quad \quad \begin{tikzcd} - {B_! t^*\al} && Y + {\Ga \cdot \al := B_! t^*\al} && Y \arrow["{\beta}", dashed, from=1-1, to=1-3] \end{tikzcd}\] @@ -82,8 +82,8 @@ \[ (\al, \be) : \Ga \to \Poly{t} Y\] for this map, since it is uniquely determined by this data. - We also have that for any $\si : \De \to \Ga$, - the following triangle commutes + Furthermore, precomposition by $\si : \De \to \Ga$, + acts on such a pair by % https://q.uiver.app/#q=WzAsNCxbMiwxLCJcXFBvbHl7dH0gWSJdLFswLDFdLFsxLDEsIlxcR2EiXSxbMSwwLCJcXERlIl0sWzMsMiwiXFxzaSIsMl0sWzMsMCwiKFxcYWwgXFxjaXJjIFxcc2ksIFxcYmUgXFxjaXJjIHReKiBcXHNpKSJdLFsyLDAsIihcXGFsLCBcXGJlKSIsMl1d \[\begin{tikzcd} & \De \\ @@ -95,3 +95,220 @@ \end{prop} \medskip + +\begin{lemma}\label{R_classifies} + Use $R$ to denote the fiber product +% https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXFBvbHl7dH0ge1l9Il0sWzEsMSwiQSJdLFswLDAsIlIiXSxbMCwxLCJCIl0sWzAsMSwidF8qIEJeKiBZIl0sWzIsMCwiXFxyaG9fe1xcUG9seXt9fSJdLFsyLDMsInReKiB0X3sqfSBCXiogWT0gXFxyaG9fXFxUZXJtIiwyXSxbMywxLCJ0IiwyXSxbMiwxLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0= +\[\begin{tikzcd} + R & {\Poly{t} {Y}} \\ + B & A + \arrow["{\rho_{\Poly{}}}", from=1-1, to=1-2] + \arrow["{t^* t_{*} B^* Y= \rho_\Term}"', from=1-1, to=2-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] + \arrow["{t_* B^* Y}", from=1-2, to=2-2] + \arrow["t"', from=2-1, to=2-2] +\end{tikzcd}\] + + By the universal property of pullbacks + and \cref{polynomial_endofunctor_property}, + The data of a map $\Ga \to R$ + corresponds to the data of + $\be : \Ga \to B$ and $(t \circ \be,y) : \Ga \to \Poly{t}{Y}$, + or just $\be : \Ga \to B$ and $y : \Ga \cdot t \circ \be \to Y$ +% https://q.uiver.app/#q=WzAsNSxbMiwxLCJcXFBvbHl7dH0ge1l9Il0sWzIsMiwiQSJdLFsxLDEsIlIiXSxbMSwyLCJCIl0sWzAsMCwiXFxHYSJdLFswLDEsInRfKiBCXiogWSJdLFsyLDAsIlxccmhvX3tcXFBvbHl7fX0iXSxbMiwzLCJcXHJob19cXFRlcm0iLDFdLFszLDEsInQiLDJdLFsyLDEsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDMsIlxcYmUiLDJdLFs0LDIsIihcXGJlLCB5KSIsMV0sWzQsMCwiKHQgXFxjaXJjIFxcYmUseSkiXV0= +\[\begin{tikzcd} + \Ga \\ + & R & {\Poly{t} {Y}} \\ + & B & A + \arrow["{(\be, y)}"{description}, from=1-1, to=2-2] + \arrow["{(t \circ \be,y)}", bend left, from=1-1, to=2-3] + \arrow["\be"', bend right, from=1-1, to=3-2] + \arrow["{\rho_{\Poly{}}}", from=2-2, to=2-3] + \arrow["{\rho_\Term}"{description}, from=2-2, to=3-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] + \arrow["{t_* B^* Y}", from=2-3, to=3-3] + \arrow["t"', from=3-2, to=3-3] +\end{tikzcd}\] + + By uniqueness in the universal property of pullbacks and \cref{polynomial_endofunctor_property}, + Precomposition by a map $\si : \De \to \Ga$ acts on such a pair by +% https://q.uiver.app/#q=WzAsNCxbMiwxLCJSIl0sWzAsMV0sWzEsMSwiXFxHYSJdLFsxLDAsIlxcRGUiXSxbMywyLCJcXHNpIiwyXSxbMywwLCIoXFxiZVxcY2lyYyBcXHNpLCB5IFxcY2lyYyB0XiogXFxzaSkiXSxbMiwwLCIoXFxiZSwgeSkiLDJdXQ== +\[\begin{tikzcd} + & \De \\ + {} & \Ga & R + \arrow["\si"', from=1-2, to=2-2] + \arrow["{(\be\circ \si, y \circ t^* \si)}", from=1-2, to=2-3] + \arrow["{(\be, y)}"', from=2-2, to=2-3] +\end{tikzcd}\] +\end{lemma} + +\medskip + +\begin{lemma}[Evaluation] \label{evaluation} + Suppose $(\be,y) : \Ga \to R$, as in \cref{R_classifies} + \[ \be : \Ga \to B \quad \text{ and } \quad y : \Ga \cdot t \circ \be \to Y\] + Then the evaluation of $y$ at $\be$ can be described in the following two ways + \[ y \circ b = \pi_{Y} \circ \counit \circ (\be, y)\] + where +% https://q.uiver.app/#q=WzAsNSxbMSwyLCJcXEdhIl0sWzIsMiwiQSJdLFsyLDEsIkIiXSxbMSwxLCJcXEdhIFxcY2RvdCB0IFxcY2lyYyBcXGJlIl0sWzAsMCwiXFxHYSJdLFswLDEsInQgXFxjaXJjIFxcYmUiLDJdLFsyLDEsInQiXSxbMywwXSxbMywyXSxbNCwzLCJiIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzQsMCwiIiwxLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNCwyLCJcXGJlIiwxXSxbMywxLCIiLDAseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0= +\[\begin{tikzcd} + \Ga \\ + & {\Ga \cdot t \circ \be} & B \\ + & \Ga & A + \arrow["b"{description}, dashed, from=1-1, to=2-2] + \arrow["\be"{description}, bend left, from=1-1, to=2-3] + \arrow[Rightarrow, bend right, no head, from=1-1, to=3-2] + \arrow["v"', from=2-2, to=2-3] + \arrow["d", from=2-2, to=3-2] + \arrow["t", from=2-3, to=3-3] + \arrow["{t \circ \be}"', from=3-2, to=3-3] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=3-3] +\end{tikzcd}\] + and +% https://q.uiver.app/#q=WzAsNyxbMywxLCJcXFBvbHl7dH0ge1l9Il0sWzMsMiwiQSJdLFsyLDEsIlIiXSxbMiwyLCJCIl0sWzEsMiwiWSBcXHRpbWVzIEIiXSxbMSwwLCJcXEdhIl0sWzAsMiwiWSJdLFswLDEsInRfKiBCXiogWSJdLFsyLDBdLFsyLDNdLFszLDEsInQiLDJdLFsyLDEsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFsyLDQsIlxcY291bml0IiwxXSxbNCwzLCJcXHBpX0IiLDJdLFs1LDAsIih0IFxcY2lyYyBcXGJlLHkpIiwxLHsiY3VydmUiOi0yfV0sWzUsMiwiKFxcYmUseSkiLDFdLFs1LDQsIih5IFxcY2lyYyBiLFxcYmUpIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzUsNiwieSBcXGNpcmMgYiIsMSx7ImN1cnZlIjoyLCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCw2LCJcXHBpX1kiXV0= +\[\begin{tikzcd} + & \Ga \\ + && R & {\Poly{t} {Y}} \\ + Y & {Y \times B} & B & A + \arrow["{(\be,y)}"{description}, from=1-2, to=2-3] + \arrow["{(t \circ \be,y)}"{description}, bend left, from=1-2, to=2-4] + \arrow["{y \circ b}"{description}, bend right, dashed, from=1-2, to=3-1] + \arrow["{(y \circ b,\be)}"{description}, dashed, from=1-2, to=3-2] + \arrow[from=2-3, to=2-4] + \arrow["\counit"{description}, from=2-3, to=3-2] + \arrow[from=2-3, to=3-3] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-3, to=3-4] + \arrow["{t_* B^* Y}", from=2-4, to=3-4] + \arrow["{\pi_Y}", from=3-2, to=3-1] + \arrow["{\pi_B}"', from=3-2, to=3-3] + \arrow["t"', from=3-3, to=3-4] +\end{tikzcd}\] +\end{lemma} +\begin{proof} + It suffices to show + $(\counit \circ (\be, y)) = (y \circ b , \be)$ instead. + \begin{align*} + & \, \counit \circ (\be, y) \\ + = & \, \counit \circ (v \circ b, y \circ t^{*} d \circ t^{*} b) + & \cref{evaluation_computation_diagram1} \\ + = & \, \counit \circ (v, y \circ t^{*} d) \circ b + & \cref{R_classifies,evaluation_computation_diagram2}\\ + = & \, \counit \circ t^{*} (t \circ \be, y) \circ b + & \cref{evaluation_computation_diagram3}\\ + % = & \, \overline{\widetilde{\counit} \circ (t \circ \be, y)} \circ b \\ + = & \, \overline{(t \circ \be, y)} \circ b + & \cref{evaluation_computation_diagram4}\\ + = & \, (y, v) \circ b + & \cref{evaluation_computation_diagram5} \\ + = & \, (y \circ b, v \circ b)\\ + = & \, (y \circ b, \be)\\ + \end{align*} + +\begin{figure}[h] + \centering% https://q.uiver.app/#q=WzAsOCxbMSwxLCJcXEdhIFxcY2RvdCB0IFxcY2lyYyBcXGJlIl0sWzIsMSwiXFxHYSJdLFswLDEsIlxcR2EiXSxbMiwwLCJcXEdhIFxcY2RvdCB0IFxcY2lyYyBcXGJlIl0sWzEsMCwiXFxHYSBcXGNkb3QgdCBcXGNpcmMgXFxiZSBcXGNkb3QgdCBcXGNpcmMgXFxiZSJdLFszLDAsIkIiXSxbMywxLCJBIl0sWzAsMCwiXFxHYSBcXGNkb3QgdCBcXGNpcmMgXFxiZSJdLFswLDEsImQiLDJdLFsyLDAsImIiLDJdLFszLDEsImQiXSxbMiwxLCIiLDAseyJjdXJ2ZSI6MywibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNCwwXSxbNCwzLCJ0XiogZCIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDUsInYiXSxbNSw2LCJ0Il0sWzEsNiwidCBcXGNpcmMgXFxiZSIsMl0sWzcsNCwidF4qIGIiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNywyLCJkIl0sWzcsMywiIiwwLHsiY3VydmUiOi00LCJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszLDYsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDEsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs3LDAsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ== +\[\begin{tikzcd} + {\Ga \cdot t \circ \be} & {\Ga \cdot t \circ \be \cdot t \circ \be} & {\Ga \cdot t \circ \be} & B \\ + \Ga & {\Ga \cdot t \circ \be} & \Ga & A + \arrow["{t^* b}", dashed, from=1-1, to=1-2] + \arrow[bend left, Rightarrow, no head, from=1-1, to=1-3] + \arrow[bend right, Rightarrow, no head, from=2-1, to=2-3] + \arrow["d", from=1-1, to=2-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] + \arrow["{t^* d}", dashed, from=1-2, to=1-3] + \arrow[from=1-2, to=2-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] + \arrow["v", from=1-3, to=1-4] + \arrow["d", from=1-3, to=2-3] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-3, to=2-4] + \arrow["t", from=1-4, to=2-4] + \arrow["b"', from=2-1, to=2-2] + \arrow["d"', from=2-2, to=2-3] + \arrow["{t \circ \be}"', from=2-3, to=2-4] +\end{tikzcd}\] + \caption{$t^{*} d \circ t^{*} b = \id_{\Ga \cdot t \circ \be}$} + \label{evaluation_computation_diagram1} +\end{figure} + +\begin{figure}[h] +% https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXEdhIl0sWzAsMSwiXFxHYSBcXGNkb3QgdCBcXGNpcmMgXFxiZSJdLFsxLDEsIlIiXSxbMCwxLCJiIiwyXSxbMSwyLCIodiwgeSBcXGNpcmMgdF57Kn0gZCkiLDJdLFswLDIsIih2IFxcY2lyYyBiLCB5IFxcY2lyYyB0XnsqfSBkIFxcY2lyYyB0XnsqfSBiKSJdXQ== +\[\begin{tikzcd} + \Ga \\ + {\Ga \cdot t \circ \be} & R + \arrow["b"', from=1-1, to=2-1] + \arrow["{(v \circ b, y \circ t^{*} d \circ t^{*} b)}", from=1-1, to=2-2] + \arrow["{(v, y \circ t^{*} d)}"', from=2-1, to=2-2] +\end{tikzcd}\] + \caption{$(v, y \circ t^{*} d) \circ b = (v \circ b, y \circ t^{*} d \circ t^{*} b)$} + \label{evaluation_computation_diagram2} +\end{figure} + +\begin{figure}[h] +% https://q.uiver.app/#q=WzAsNixbMSwwLCJSIl0sWzIsMCwiQiJdLFsxLDEsIlxcUG9seXt0fXtZfSJdLFsyLDEsIkEiXSxbMCwwLCJcXEdhIFxcY2RvdCB0IFxcY2lyYyBcXGJlIl0sWzAsMSwiXFxHYSJdLFswLDFdLFswLDJdLFsxLDMsInQiXSxbMiwzLCJ0XyogQl4qIFkiLDJdLFswLDMsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDAsIih2LHkgXFxjaXJjIHReKiBkKSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs0LDUsImQiLDFdLFs1LDIsIih0IFxcY2lyYyBcXGJlLCB5KSIsMl0sWzUsMywidCBcXGNpcmMgXFxiZSIsMSx7Im9mZnNldCI6MywiY3VydmUiOjN9XSxbNCwxLCJ2IiwxLHsib2Zmc2V0IjotMywiY3VydmUiOi0zfV0sWzQsMiwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d +\[\begin{tikzcd} + {\Ga \cdot t \circ \be} & R & B \\ + \Ga & {\Poly{t}{Y}} & A + \arrow["{(v,y \circ t^* d)}", dashed, from=1-1, to=1-2] + \arrow["v"{description}, shift left=3, bend left, from=1-1, to=1-3] + \arrow["d"{description}, from=1-1, to=2-1] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] + \arrow[from=1-2, to=1-3] + \arrow[from=1-2, to=2-2] + \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3] + \arrow["t", from=1-3, to=2-3] + \arrow["{(t \circ \be, y)}"', from=2-1, to=2-2] + \arrow["{t \circ \be}"{description}, shift right=3, bend right, from=2-1, to=2-3] + \arrow["{t_* B^* Y}"', from=2-2, to=2-3] +\end{tikzcd} \quad + % https://q.uiver.app/#q=WzAsMyxbMSwxLCJcXFBvbHl7dH17WX0iXSxbMCwxLCJcXEdhIl0sWzAsMCwiXFxHYSBcXGNkb3QgdCBcXGNpcmMgXFxiZSJdLFsxLDAsIih0IFxcY2lyYyBcXGJlLCB5KSIsMl0sWzIsMSwiZCIsMl0sWzIsMCwiKHQgXFxjaXJjIFxcYmUgXFxjaXJjIGQsIHkgXFxjaXJjIHReKiBkKSJdXQ== +\begin{tikzcd} + {\Ga \cdot t \circ \be} \\ + \Ga & {\Poly{t}{Y}} + \arrow["d"', from=1-1, to=2-1] + \arrow["{(t \circ \be \circ d, y \circ t^* d)}", from=1-1, to=2-2] + \arrow["{(t \circ \be, y)}"', from=2-1, to=2-2] +\end{tikzcd} +\quad \text{ using \cref{polynomial_endofunctor_property,R_classifies}} +\] + + \caption{$t^{*}(t \circ \be, y) = (v, y \circ t^{*}d)$} + \label{evaluation_computation_diagram3} +\end{figure} + +\begin{figure}[h] +% https://q.uiver.app/#q=WzAsOCxbMCwwLCJ0XioodCBcXGNpcmMgXFxiZSkiXSxbMCwxLCJ0XiogdF8qIEJeKiBZIl0sWzEsMSwiQl4qWSJdLFsyLDBdLFsyLDFdLFszLDAsInQgXFxjaXJjIFxcYmUiXSxbMywxLCJ0XyogQl4qIFkiXSxbNCwxLCJ0XyogQl4qWSJdLFswLDEsInReKiAodCBcXGNpcmMgXFxiZSwgeSkiLDJdLFsxLDIsIlxcY291bml0IiwyXSxbMCwyLCJcXG92ZXJsaW5leyh0IFxcY2lyYyBcXGJlLHkpfSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFszLDQsIiIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzYsNywiXFx3aWRldGlsZGV7XFxjb3VuaXR9IiwyLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNSw2LCIodCBcXGNpcmMgXFxiZSwgeSkiLDJdLFs1LDcsIih0IFxcY2lyYyBcXGJlLHkpIl1d +\[\begin{tikzcd} + {t^*(t \circ \be)} && {} & {t \circ \be} \\ + {t^* t_* B^* Y} & {B^*Y} & { t^{*} \dashv t_{*}} & {t_* B^* Y} & {t_* B^*Y} + \arrow["{t^* (t \circ \be, y)}"', from=1-1, to=2-1] + \arrow["{\overline{(t \circ \be,y)}}", dashed, from=1-1, to=2-2] + \arrow[Rightarrow, no head, from=1-3, to=2-3] + \arrow["{(t \circ \be, y)}"', from=1-4, to=2-4] + \arrow["{(t \circ \be,y)}", from=1-4, to=2-5] + \arrow["\counit"', from=2-1, to=2-2] + \arrow["{\widetilde{\counit}}"', Rightarrow, no head, from=2-4, to=2-5] +\end{tikzcd} +\] + \caption{$\counit \circ t^{*} (t \circ \be, y) = \overline{(t \circ \be, y)}$} + \label{evaluation_computation_diagram4} +\end{figure} + +\begin{figure}[h] +% https://q.uiver.app/#q=WzAsOCxbMCwwLCJcXEdhIFxcY2RvdCB0IFxcY2lyYyBcXGJlIl0sWzAsMSwiQiJdLFsxLDAsIlkgXFx0aW1lcyBCIl0sWzIsMF0sWzIsMSwidF4qIFxcZGFzaHYgdF8qIl0sWzMsMCwiXFxHYSJdLFszLDEsIkEiXSxbNCwwLCJcXFBvbHl7dH17WX0iXSxbMCwxLCJ2ID0gdF4qICh0IFxcY2lyYyBcXGJlKSIsMl0sWzAsMiwiKHksdikiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMyw0LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs1LDYsInQgXFxjaXJjIFxcYmUiLDJdLFs1LDcsIih0IFxcY2lyYyBcXGJlLHkpIl0sWzcsNiwidF8qQl4qWSJdLFsyLDEsIkJeKlkiXV0= +\[\begin{tikzcd} + {\Ga \cdot t \circ \be} & {Y \times B} & {} & \Ga & {\Poly{t}{Y}} \\ + B && {t^* \dashv t_*} & A + \arrow["{(y,v)}", dashed, from=1-1, to=1-2] + \arrow["{v = t^* (t \circ \be)}"', from=1-1, to=2-1] + \arrow["{B^*Y}", from=1-2, to=2-1] + \arrow[Rightarrow, no head, from=1-3, to=2-3] + \arrow["{(t \circ \be,y)}", from=1-4, to=1-5] + \arrow["{t \circ \be}"', from=1-4, to=2-4] + \arrow["{t_*B^*Y}", from=1-5, to=2-4] +\end{tikzcd}\] + \caption{$\overline{(t \circ \be, y)} = (y,v)$} + \label{evaluation_computation_diagram5} +\end{figure} + +\end{proof} + +\medskip