jonmsterling.com
this repo has no description
typos
+7
-7
+1
-1
mscs.tex
+1
-1
mscs.tex
+2
-2
nodes/abstract.tex
+2
-2
nodes/abstract.tex
···
1
-
Martin-L\"of's identity types provide a generic (albeit opaque) notion of identification or ``equality'' between any two elements of the same type, embodied in a canonical reflexive graph structure $(=_A, \mathbf{refl})$ on any type $A$. The miracle of Voevodsky's \emph{univalence principle} is that it ensures, for essentially any naturally occuring structure in mathematics, that this the resultant notion of identification is equivalent to the type of \emph{isomorphisms} in the category of such structures. Characterisations of this kind are not automatic and must be established one-by-one; to this end, several authors have employed \emph{reflexive graphs} and \emph{displayed reflexive graphs} to organise the characterisation of identity types.
1
+
Martin-L\"of's identity types provide a generic (albeit opaque) notion of identification or ``equality'' between any two elements of the same type, embodied in a canonical reflexive graph structure $(=_A, \mathbf{refl})$ on any type $A$. The miracle of Voevodsky's \emph{univalence principle} is that it ensures, for essentially any naturally occurring structure in mathematics, that this the resultant notion of identification is equivalent to the type of \emph{isomorphisms} in the category of such structures. Characterisations of this kind are not automatic and must be established one-by-one; to this end, several authors have employed \emph{reflexive graphs} and \emph{displayed reflexive graphs} to organise the characterisation of identity types.
2
2
%
3
-
We contribute \textbf{reflexive graph lenses}, a new family of intermediate abstractions lying between families of reflexive graphs and displayed reflexive graphs that simplifies the characterisation of identity types for complex structures. Every reflexive graph lens gives rise to a (more complicated) displayed reflexive graph, and our experience suggests that many naturally occuring displayed reflexive graphs arise in this way. Evidence for the utility of reflexive graph lenses is given by means of several case studies, including the theory of reflexive graphs itself as well as that of polynomial type operators. Finally, we exhibit an equivalance between the type of reflexive graph fibrations and the type of \emph{univalent} reflexive graph lenses.
3
+
We contribute \textbf{reflexive graph lenses}, a new family of intermediate abstractions lying between families of reflexive graphs and displayed reflexive graphs that simplifies the characterisation of identity types for complex structures. Every reflexive graph lens gives rise to a (more complicated) displayed reflexive graph, and our experience suggests that many naturally occurring displayed reflexive graphs arise in this way. Evidence for the utility of reflexive graph lenses is given by means of several case studies, including the theory of reflexive graphs itself as well as that of polynomial type operators. Finally, we exhibit an equivalence between the type of reflexive graph fibrations and the type of \emph{univalent} reflexive graph lenses.
+1
-1
nodes/intro.tex
+1
-1
nodes/intro.tex
···
571
571
\end{proposition}
572
572
573
573
574
-
The pay-off of introducing lenses of reflexive graphs is twofold. First of all, many naturally occuring displayed reflexive graphs have the shape of $\CovDisp{\gA}{\gB}$ or $\CtrvDisp{\gA}{\gB}$ already; more importantly, however, it frequently happens that the components of the given displayed reflexive graph arise as a pre-existing family of reflexive graphs for which we have already proved univalence. Therefore, it is advantageous to obtain a displayed path object automatically from a very simple algebraic structure on a pre-existing family of path objects: a pushforward operator and a lax unitor.
574
+
The pay-off of introducing lenses of reflexive graphs is twofold. First of all, many naturally occurring displayed reflexive graphs have the shape of $\CovDisp{\gA}{\gB}$ or $\CtrvDisp{\gA}{\gB}$ already; more importantly, however, it frequently happens that the components of the given displayed reflexive graph arise as a pre-existing family of reflexive graphs for which we have already proved univalence. Therefore, it is advantageous to obtain a displayed path object automatically from a very simple algebraic structure on a pre-existing family of path objects: a pushforward operator and a lax unitor.
575
575
576
576
\end{xsect}
577
577
+1
-1
nodes/lens-of-fibration.tex
+1
-1
nodes/lens-of-fibration.tex
···
140
140
\end{construction}
141
141
142
142
\begin{lemma}[Straightening is an equivalence]\label[lemma]{lem:cov-str-equiv}
143
-
Let $\gB$ be a covariant fibration of reflexive graphs over a reflexive graph $\gA$. Each straightening function $\Str{\gB}[p] : u \Edge{\gB}[p]v \to p_*^\gB u\Edge{\gB\prn{y}} v$ is an equivalance, with the inverse tracked by $\Unstr{\gB}[p] : p_*^\gB u\Edge{\gB\prn{y}} v \to u \Edge{\gB}[p]v$.
143
+
Let $\gB$ be a covariant fibration of reflexive graphs over a reflexive graph $\gA$. Each straightening function $\Str{\gB}[p] : u \Edge{\gB}[p]v \to p_*^\gB u\Edge{\gB\prn{y}} v$ is an equivalence, with the inverse tracked by $\Unstr{\gB}[p] : p_*^\gB u\Edge{\gB\prn{y}} v \to u \Edge{\gB}[p]v$.
144
144
\end{lemma}
145
145
146
146
\begin{proof}
+1
-1
nodes/lenses-of-reflexive-graphs.tex
+1
-1
nodes/lenses-of-reflexive-graphs.tex
···
1
1
\begin{xsect}[sec:lenses]{Lenses of reflexive graphs and path objects}
2
2
3
-
In this section, we are concerned with various kinds of \emph{families} of ordinary reflexive graphs, and how they give rise to certain naturally occuring \emph{displayed} reflexive graphs.
3
+
In this section, we are concerned with various kinds of \emph{families} of ordinary reflexive graphs, and how they give rise to certain naturally occurring \emph{displayed} reflexive graphs.
4
4
5
5
\input{nodes/lenses.tex}
6
6
\input{nodes/bivariant-midpoint-lenses.tex}
+1
-1
nodes/polynomials.tex
+1
-1
nodes/polynomials.tex
···
1
1
\begin{xsect}[sec:polynomials]{Polynomials and partial products of reflexive graphs}
2
2
Any family of types $x:A\vdash B\prn{x} : \TYPE$ induces a \DefEmph{polynomial} type operator $\Poly{A}{B}{C} :\equiv \Sum{x:A}\Prod{u:B\prn{x}}C$; the universal property of $\Poly{A}{B}{C}$ is that of a \emph{partial product}~\citep{dyckhoff-tholen:1987}. In this section, we generalise the construction of polynomials to lenses of reflexive graphs; the definitions of the polynomial reflexive graphs will then mirror the description of \emph{covariant} and \emph{contravariant} partial products in a 2-category~\citep{johnstone:1993,johnstone:2002}. We then show how to specialise the construction of polynomials to obtain suitable path object structures on the \emph{partial map classifier} of a given dominance as in synthetic domain theory~\citep{rosolini:1986}.
3
3
4
-
% Although it is possible to develop a theory of partial products for arbitrary lenses, most naturally occuring examples of partial products seem to be of definitional lenses; as in this case the theory works out more smoothly, we restrict our attention here to definitional lenses.
4
+
% Although it is possible to develop a theory of partial products for arbitrary lenses, most naturally occurring examples of partial products seem to be of definitional lenses; as in this case the theory works out more smoothly, we restrict our attention here to definitional lenses.
5
5
%% Actually, can this even be done without univalence assumptions on the rxgphs?
6
6
7
7
In this section, we assume function extensionality.