wip f=g aborted clumsy

Author: Marc Bezem

intro-uf.tex

@@ -3609,7 +3609,7 @@ \section{Pointed types}\label{sec:pointedtypes}
                                 \&\& f(\pt_X) \ar[d,eqr,"h(\pt_X)"] \\
   \pt_Y\ar[urr,eqr,"f_\pt"] \ar[rr,eql,"g_\pt"']\&\& g(\pt_X) 
   \end{tikzcd}
-  \caption{$g_\pt \protect\eqto (h(\pt_X)\cdot f_\pt)$ \MB{sic}} 
+  \caption{$g_\pt \protect\eqto (h(\pt_X)\cdot f_\pt)$ \MB{font}} 
 \end{marginfigure}
 Then the map (explained by the diagram in the proof below)
 \begin{align*}
@@ -3640,17 +3640,51 @@ \section{Pointed types}\label{sec:pointedtypes}
 \& \& \&\&\& \ptw(\fst(p))(\pt_X)\cdot f_\pt
   \end{tikzcd}
  \]
-For the inverse equivalence, given  $h:\prod_{x:X}(f(x)\eqto g(x))$ and
+For the inverse function, given  $h:\prod_{x:X}(f(x)\eqto g(x))$ and
 $q: (g_\pt \eqto (h(\pt_X)\cdot f_\pt) )$, we must construct a path
-from $f$ to $g$. The obvious thing to do
-is to consider the path $\inv\ptw(h)$ between the untyped functions $f$
+from $f$ to $g$. The obvious thing to do is to consider the path 
+$\etop h \defeq \inv\ptw(h)$ between the untyped functions $f$
 and $g$. Using \cref{lem:isEq-pair=}, it suffices then to construct a path
-from $f_\pt$ to $g_\pt$ over $\inv\ptw(h)$. For this we can use
-the equivalence $\inv{\po}_{inv\ptw(h)}$, reducing the task to
-constructing a path of type $\trp[T]{\inv\ptw(h)}(f_\pt) \eqto g_\pt$.
-Using $\trptw$, the latter type is equivalent to
-$\ptw\inv\ptw(h)(f_\pt) \eqto g_\pt$. Since $\ptw$ is an equivalence,
-we can simply transport $q$ and get the desired identification.
+from $f_\pt$ to $g_\pt$ over $\etop h$. For this we can use
+the equivalence $\inv{\po}_{\etop h}$, reducing the task to
+constructing a path of type $\trp[T]{\etop h}(f_\pt) \eqto g_\pt$.
+\begin{marginfigure}
+  \begin{tikzcd}[ampersand replacement=\&,column sep=small]
+  \trp[T]{\etop h}(f_\pt)
+     \ar[d,eqr,"{\trptw(\etop h,f_\pt)}"] \\
+  \ptw(\etop h)(\pt_X)\cdot f_\pt 
+     \ar[d,eqr,"{\ap{(\blank\cdot f_\pt)}(\etop u(h)(\pt_X))}"] \\
+  h(\pt_X)\cdot f_\pt 
+     \ar[d,eqr,"{\inv q}"]\\
+  g_\pt
+  \end{tikzcd}
+  \caption{$\trp[T]{\etop h}(f_\pt) \protect\eqto g_\pt$ \MB{font}} 
+\end{marginfigure}
+The latter path is the composite that is illustrated in the margin.
+Since $\ptw$ is an 
+equivalence, we have a path $u(h): \ptw(\inv\ptw(h)) \eqto h$.\footnote{%
+\MB{Doesn't compute, $u$ is unknown. Problem ahead?}}
+We let $\etop u(h)(\pt_X)$ abbreviate the path $\ptw(u(h))(\pt_X)$
+from $\ptw(\etop h)(\pt_X)$ to $h(\pt_X)$. 
+In total we have the following inverse function:
+\[
+(h,q) \mapsto \pathpair{\etop h}
+{\inv\po_{\etop h}(\inv q \cdot \ap{(\blank\cdot f_\pt)}(\etop u(h)(\pt_X))
+\cdot(\trptw(\etop h,f_\pt)))
+}
+\]
+
+It remains to prove equivalence by applying \cref{lem:weq-iso}.
+For the round trip starting with $p: f\eqto g$ we use path induction,
+so that it suffices to consider the case $\refl{f}: f\eqto f$.
+In this case we abbreviate $h\defeq\ptw(\fst(\refl{f}))$ and have
+$h(x)\jdeq\refl{f(x)}$.
+We have $\ptw_*(\refl{f}) \jdeq (h,(\trptw(\fst(\refl{f}),f_\pt))
+\cdot\inv{(\po_{\fst(\refl{f})}(\snd(\refl{f})))})$.
+We also have $\po_{\fst(\refl{f})}(\snd(\refl{f}))\jdeq\refl{f_\pt}$
+and $\trptw(\fst(\refl{f}),f_\pt)\jdeq\refl{f_\pt}$. This means that
+we can apply the inverse equivalence to the pair $(h,\refl{f_\pt})$.
+We compute $\etop h$.... abort clumsy attempt
 \end{proof}
 
 \section{Operations that produce sets}