jonmsterling.com
this repo has no description
working on intro
+495
-279
+494
-278
nodes/intro.tex
+494
-278
nodes/intro.tex
···
1
1
\input{nodes/conventions}
2
2
3
3
\begin{xsect}{Introduction}
4
-
In the setting of Martin-L\"of's intensional type theory~\citep{nordstrom-peterson-smith:1990}, every type $A$ comes equipped with a type constructor $x:A,y:A\vdash \Id{A}{x}{y}:\TYPE$ that classifies \emph{identifications} between elements of $A$, \ie witnesses that two given elements are ``equal''. Rather than being defined separately for each $A$, the identity type constructor $\IdCon{A}$ is specified generically for all types by means of formation, introduction, elimination, and computation rules:
5
-
%
6
-
\begin{mathparpagebreakable}
7
-
\inferrule[formation]{
8
-
\Gamma\vdash A:\TYPE\\
9
-
\Gamma\vdash u,v:A
10
-
}{
11
-
\Gamma\vdash\Id{A}{u}{v}:\TYPE
12
-
}
13
-
\and
14
-
\inferrule[introduction]{
15
-
\Gamma\vdash A:\TYPE\\
16
-
\Gamma\vdash u:A
17
-
}{
18
-
\Gamma\vdash \Refl : \Id{A}{u}{u}
19
-
}
20
-
\and
21
-
\inferrule[elimination]{
22
-
\Gamma\vdash A:\TYPE\\
23
-
\Gamma,x:A,y:A,p:\Id{A}{x}{y}\vdash C\prn{x,y,p}:\TYPE\\\\
24
-
\Gamma,x:A\vdash c\prn{x} : C\prn{x,x,\Refl}\\
25
-
\Gamma\vdash u,v:A\\
26
-
\Gamma\vdash w:\Id{A}{u}{v}
27
-
}{
28
-
\Gamma\vdash \J{A}{C}{c}{u}{v}{w} : C\prn{u,v,w}
29
-
}
30
-
\and
31
-
\inferrule[computation]{
32
-
\Gamma\vdash A:\TYPE\\
33
-
\Gamma,x:A,y:A,p:\Id{A}{x}{y}\vdash C\prn{x,y,p}:\TYPE\\
34
-
\Gamma,x:A\vdash c\prn{x} : C\prn{x,x,\Refl}\\
35
-
\Gamma\vdash u:A
36
-
}{
37
-
\Gamma\vdash \J{A}{C}{c}{u}{u}{\Refl} \equiv c\prn{u} : C\prn{u,u,\Refl}
38
-
}
39
-
\end{mathparpagebreakable}
40
4
41
-
The formation and introduction rule for the identity type can be thought of as equipping $A$ with the structure of a \emph{reflexive graph}\footnote{In the context of category theory, one uses the term ``graph'' to refer to what combinatorialists would normally refer to as \emph{multigraphs} or \emph{pseudo-graphs}. A graph in the traditional sense would be a graph (in the present generalised sense) in which the type of vertices is a set and the type of edges between two fixed vertices is a proposition; we might refer to such objects as ``locally propositional set-graphs''.} (see \cref{def:reflexive-graph}). The elimination and computation rule then ensure that this reflexive graph structure is the smallest possible one that can be formed with vertices in $A$.
5
+
\begin{xsect}{Martin-L\"of's identity types}
6
+
In the setting of Martin-L\"of's intensional type theory~\citep{nordstrom-peterson-smith:1990}, every type $A$ comes equipped with a type constructor $x:A,y:A\vdash \Id{A}{x}{y}:\TYPE$ that classifies \emph{identifications} between elements of $A$, \ie witnesses that two given elements are ``equal''. Rather than being defined separately for each $A$, the identity type constructor $\IdCon{A}$ is specified generically for all types by means of formation, introduction, elimination, and computation rules:
7
+
%
8
+
\begin{mathparpagebreakable}
9
+
\inferrule[formation]{
10
+
\Gamma\vdash A:\TYPE\\
11
+
\Gamma\vdash u,v:A
12
+
}{
13
+
\Gamma\vdash\Id{A}{u}{v}:\TYPE
14
+
}
15
+
\and
16
+
\inferrule[introduction]{
17
+
\Gamma\vdash A:\TYPE\\
18
+
\Gamma\vdash u:A
19
+
}{
20
+
\Gamma\vdash \Refl : \Id{A}{u}{u}
21
+
}
22
+
\and
23
+
\inferrule[elimination]{
24
+
\Gamma\vdash A:\TYPE\\
25
+
\Gamma,x:A,y:A,p:\Id{A}{x}{y}\vdash C\prn{x,y,p}:\TYPE\\\\
26
+
\Gamma,x:A\vdash c\prn{x} : C\prn{x,x,\Refl}\\
27
+
\Gamma\vdash u,v:A\\
28
+
\Gamma\vdash w:\Id{A}{u}{v}
29
+
}{
30
+
\Gamma\vdash \J{A}{C}{c}{u}{v}{w} : C\prn{u,v,w}
31
+
}
32
+
\and
33
+
\inferrule[computation]{
34
+
\Gamma\vdash A:\TYPE\\
35
+
\Gamma,x:A,y:A,p:\Id{A}{x}{y}\vdash C\prn{x,y,p}:\TYPE\\
36
+
\Gamma,x:A\vdash c\prn{x} : C\prn{x,x,\Refl}\\
37
+
\Gamma\vdash u:A
38
+
}{
39
+
\Gamma\vdash \J{A}{C}{c}{u}{u}{\Refl} \equiv c\prn{u} : C\prn{u,u,\Refl}
40
+
}
41
+
\end{mathparpagebreakable}
42
42
43
-
This universal property of the identity type ensures that identifications between elements of a given type $A$ are automatically respected by any possible construction or predicate.
43
+
The formation and introduction rule for the identity type can be thought of as equipping $A$ with the structure of a \emph{reflexive graph}\footnote{In the context of category theory, one uses the term ``graph'' to refer to what combinatorialists would normally refer to as \emph{multigraphs} or \emph{pseudo-graphs}. A graph in the traditional sense would be a graph (in the present generalised sense) in which the type of vertices is a set and the type of edges between two fixed vertices is a proposition; we might refer to such objects as ``locally propositional set-graphs''.} (see \cref{def:reflexive-graph}). The elimination and computation rule then ensure that this reflexive graph structure is the smallest possible one that can be formed with vertices in $A$. This universal property is most commonly employed in terms of the principle of \emph{identification induction} below.
44
44
45
+
\begin{principle}[{Identification induction}]\label[principle]{principle:identification-induction}
46
+
Given a family of types $x,y:A;p:\Id{A}{x}{y}\vdash C\prn{x,y,p}: \TYPE$, to define a dependent function $x,y:A;p:\Id{A}{x}{y}\vdash f\prn{x,y,p}:C\prn{x,y,p}$ it suffices to specify $x:A\vdash f\prn{x,x,\Refl}:C\prn{x,x,\Refl}$.
47
+
\end{principle}
45
48
46
-
% \begin{xsect}{Using identification induction}
47
-
% As discussed in \S1.12.1 of the HoTT Book~\citep{hottbook}, the primitive elimination and computation rules of the identity type constructor allow for the definition of (dependent) functions on identifications by \emph{induction}.
48
49
49
-
% \begin{principle}[{Identification induction}]\label[principle]{principle:identification-induction}
50
-
% Given a family of types \[x,y:A;p:\Id{A}{x}{y}\vdash C\prn{x,y,p}: \TYPE,\] to define a dependent function \[x,y:A;p:\Id{A}{x}{y}\vdash f\prn{x,y,p}:C\prn{x,y,p}\] it suffices to specify $x:A\vdash f\prn{x,x,\Refl}:C\prn{x,x,\Refl}$.
51
-
% \end{principle}
50
+
\begin{proof}
51
+
To define $x,y,p\vdash f\prn{x,y,p}:C\prn{x,y,p}$ in terms of $x\vdash f\prn{x,x,\Refl}:C\prn{x,x,\Refl}$, we use the elimination rule of the identity type as follows:
52
+
\[
53
+
f\prn{x,y,p} :\equiv
54
+
\J{A}{C}{\Bind{x}f\prn{x,x,\Refl}}{x}{y}{p}
55
+
\qedhere
56
+
\]
57
+
\end{proof}
52
58
53
-
% \begin{proof}
54
-
% To define $x,y,p\vdash f\prn{x,y,p}:C\prn{x,y,p}$ in terms of $x\vdash f\prn{x,x,\Refl}:C\prn{x,x,\Refl}$, we use the elimination rule of the identity type as follows:
55
-
% \[
56
-
% f\prn{x,y,p} :\equiv
57
-
% \J{A}{C}{\Bind{x}f\prn{x,x,\Refl}}{x}{y}{p}
58
-
% \qedhere
59
-
% \]
60
-
% \end{proof}
59
+
A special case of \cref{principle:identification-induction} is \emph{transport}, which materialises identifications $\Id{A}{u}{v}$ as functions $B\prn{u}\to B\prn{v}$ for any family $x:A\vdash B\prn{x}:\TYPE$.
61
60
62
-
% A special case of \cref{principle:identification-induction} is \emph{transport}, which materialises identifications $\Id{A}{u}{v}$ as functions $B\prn{u}\to B\prn{v}$ for any family $x:A\vdash B\prn{x}:\TYPE$.
61
+
\begin{corollary}[Transport]\label[corollary]{cor:transport}
62
+
Given a family of types $x:A\vdash B\prn{x}: \TYPE$, for any $x,y:A$ and $p:\Id{A}{x}{y}$ we may define a mapping $p_*^B\colon B\prn{x} \to B\prn{y}$ such that for all $x : A$ and $b:B\prn{x}$ we have $\Refl_* b \equiv b$.
63
+
\end{corollary}
63
64
64
-
% \begin{corollary}[Transport]\label[corollary]{cor:transport}
65
-
% Given a family of types $x:A\vdash B\prn{x}: \TYPE$, for any $x,y:A$ and $p:\Id{A}{x}{y}$ we may define a mapping $p_*^B\colon B\prn{x} \to B\prn{y}$ such that for all $x : A$ and $b:B\prn{x}$ we have $\Refl_* b \equiv b$.
66
-
% \end{corollary}
65
+
\begin{proof}
66
+
Let $C\prn{x,y,p} :\equiv B\prn{x} \to B\prn{y}$; using \cref{principle:identification-induction} we may define a dependent function $\mathsf{transport}\prn{x,y,p}:C\prn{x,y,p}$ by specifying
67
+
$
68
+
\mathsf{transport}\prn{x,x,\Refl} :\equiv \Lam{b}b
69
+
$. Then for any $p:\Id{A}{x}{y}$ we define $p_*^Bb :\equiv \mathsf{transport}\prn{x,y,p}$.
70
+
\end{proof}
67
71
68
-
% \begin{proof}
69
-
% Let $C\prn{x,y,p} :\equiv B\prn{x} \to B\prn{y}$; using \cref{principle:identification-induction} we may define a dependent function $\mathsf{transport}\prn{x,y,p}:C\prn{x,y,p}$ by specifying
70
-
% $
71
-
% \mathsf{transport}\prn{x,x,\Refl} :\equiv \Lam{b}b
72
-
% $. Then for any $p:\Id{A}{x}{y}$ we define $p_*^Bb :\equiv \mathsf{transport}\prn{x,y,p}$.
73
-
% \end{proof}
72
+
\begin{definition}[Singletons]\label[definition]{def:singleton}
73
+
Given an element $u:A$, we define the \DefEmph{singleton type} at $x$ to be the type $\Singleton{A}{u}$ of elements of $A$ equipped with identifications from $u$:
74
+
\[
75
+
\Singleton{A}{u} :\equiv \Sum{y:A}\Id{A}{u}{y}
76
+
\]
77
+
\end{definition}
74
78
75
-
% \begin{definition}[Singletons]\label[definition]{def:singleton}
76
-
% Given an element $u:A$, we define the \DefEmph{singleton type} at $x$ to be the type $\Singleton{A}{u}$ of elements of $A$ equipped with identifications from $u$:
77
-
% \[
78
-
% \Singleton{A}{u} :\equiv \Sum{y:A}\Id{A}{u}{y}
79
-
% \]
80
-
% \end{definition}
79
+
Of course, the simplest element of $\Singleton{A}{u}$ is the pair $\prn{u,\Refl}$. We can prove using \cref{principle:identification-induction} that $\prn{u,\Refl}$ is the \emph{only} element of $\Singleton{A}{u}$.
81
80
82
-
% Of course, the simplest element of $\Singleton{A}{u}$ is the pair $\prn{u,\Refl}$. We can prove using \cref{principle:identification-induction} that $\prn{u,\Refl}$ is the \emph{only} element of $\Singleton{A}{u}$.
81
+
\begin{corollary}[Contractibility of singletons]\label[corollary]{cor:contractibility-of-singletons}
82
+
For any fixed element $u:A$, we may define a dependent function
83
+
$\Phi_{u} \colon \Prod{q : \Singleton{A}{u}} \Id{\Singleton{A}{u}}{\prn{u,\Refl}}{q}$ witnessing that any element of $\Singleton{A}{u}$ can be identified with $\prn{u,\Refl}$, such that $\Phi_u\,\prn{u,\Refl} \equiv \Refl$.
84
+
\end{corollary}
83
85
84
-
% \begin{corollary}[Contractibility of singletons]\label[corollary]{cor:contractibility-of-singletons}
85
-
% For any fixed element $u:A$, we may define a dependent function
86
-
% $\Phi_{u} \colon \Prod{q : \Singleton{A}{u}} \Id{\Singleton{A}{u}}{\prn{u,\Refl}}{q}$ witnessing that any element of $\Singleton{A}{u}$ can be identified with $\prn{u,\Refl}$, such that $\Phi_u\,\prn{u,\Refl} \equiv \Refl$.
87
-
% \end{corollary}
86
+
\begin{proof}
87
+
We define the following dependent function using \cref{principle:identification-induction}:
88
88
89
-
% \begin{proof}
90
-
% We define the following dependent function using \cref{principle:identification-induction}:
89
+
\iblock{
90
+
\mhang{
91
+
x,y:A;p:\Id{A}{x}{y} \vdash \Phi_x\prn{y,p} :
92
+
\Id{\Singleton{A}{x}}{\prn{x,\Refl}}{\prn{y,q}}
93
+
}{
94
+
\commentrow{by \cref{principle:identification-induction}}
95
+
\mrow{
96
+
x:A\vdash \Phi_x\prn{x,\Refl} : \Id{\Singleton{A}{x}}{\prn{x,\Refl}}{\prn{x,\Refl}}
97
+
}
98
+
\commentrow{by reflexivity}
99
+
\mrow{
100
+
x:A\vdash \Phi_x\prn{x,\Refl} :\equiv \Refl
101
+
}
102
+
\qedhere
103
+
}
104
+
}
105
+
\end{proof}
91
106
92
-
% \iblock{
93
-
% \mhang{
94
-
% x,y:A;p:\Id{A}{x}{y} \vdash \Phi_x\prn{y,p} :
95
-
% \Id{\Singleton{A}{x}}{\prn{x,\Refl}}{\prn{y,q}}
96
-
% }{
97
-
% \commentrow{by \cref{principle:identification-induction}}
98
-
% \mrow{
99
-
% x:A\vdash \Phi_x\prn{x,\Refl} : \Id{\Singleton{A}{x}}{\prn{x,\Refl}}{\prn{x,\Refl}}
100
-
% }
101
-
% \commentrow{by reflexivity}
102
-
% \mrow{
103
-
% x:A\vdash \Phi_x\prn{x,\Refl} :\equiv \Refl
104
-
% }
105
-
% \qedhere
106
-
% }
107
-
% }
108
-
% \end{proof}
109
107
110
-
% There is an alternative, equivalent, formulation of identification induction due to \citet{paulin-mohring:1993}, that fixes an element $u:A$ and allows induction on data of the form $y:A, p:u=y$. This is called ``based identification induction'':
108
+
There is an alternative, equivalent, formulation of identification induction due to \citet{paulin-mohring:1993}, that fixes an element $u:A$ and allows induction on data of the form $y:A, p:u=y$. This is called ``based identification induction'':
111
109
112
-
% \begin{principle}[{Based identification induction}]\label[principle]{principle:based-identification-induction}
113
-
% Given a fixed element $u:A$ and a family of types $y:A,p:\Id{A}{u}{y}\vdash B\prn{y,p}:\TYPE$, to define a dependent function $y:A,p:\Id{A}{u}{y}\vdash f\prn{y,p}:B\prn{y,p}$ it suffices to specify $f\prn{u,\Refl} : B\prn{u,\Refl}$.
114
-
% \end{principle}
115
110
116
-
% %% Typo, but I have to re-understand the math to fix the typo.
117
-
% It is not difficult to \cref{principle:identification-induction} to \cref{principle:based-identification-induction}. The converse direction is slightly more difficult and rests on both \cref{cor:transport,cor:contractibility-of-singletons}; we recall Martin Hofmann's proof below as reported by \citet[Addendum]{streicher:1994}.
111
+
\begin{principle}[{Based identification induction}]\label[principle]{principle:based-identification-induction}
112
+
Given a fixed element $u:A$ and a family of types $y:A,p:\Id{A}{u}{y}\vdash B\prn{y,p}:\TYPE$, to define a dependent function $y:A,p:\Id{A}{u}{y}\vdash f\prn{y,p}:B\prn{y,p}$ it suffices to specify $f\prn{u,\Refl} : B\prn{u,\Refl}$.
113
+
\end{principle}
118
114
119
-
% \begin{proof}
120
-
% Let $q:\Singleton{A}{u}\vdash B^\sharp\prn{u} : \TYPE$ be the family $B^\sharp\prn{\prn{y,p}} :\equiv B\prn{y,p}$. For any $y:A$ and $p:\Id{A}{x}{y}$ we have by the contractiblity of singletons (\cref{cor:contractibility-of-singletons}) an identification $\Phi_{u}\,\prn{y,p}: \Id{\Singleton{A}{u}}{\prn{u,\Refl}}{\prn{y,p}}$. By transport (\cref{cor:transport}), we have $\prn{\Phi_{u}\,\prn{y,p}}_*^{B^\sharp}\colon B\prn{x,\Refl}\to B\prn{y,p}$.
121
-
% %
122
-
% We may therefore define $y,p\vdash f:\prn{y,p}:B\prn{y,p}$ to be
123
-
% $\prn{\Phi_{u}\,\prn{y,p}}_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}$, as we have the following definitional equivalences:
124
-
% \[
125
-
% \prn{\Phi_{u}\,\prn{u,\Refl}}_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}
126
-
% \equiv
127
-
% \Refl_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}
128
-
% \equiv f\prn{u,\Refl}
129
-
% \qedhere
130
-
% \]
131
-
% \end{proof}
115
+
We recall Martin Hofmann's proof below as reported by \citet[Addendum]{streicher:1994}.
132
116
133
-
% Independently, \citet{van-den-berg-garner:2011} and \citet{lumsdaine:2010} have shown that identification induction exhibits a weak globular $\infty$-groupoid structure on each type $A$. In the lowest dimension, this corresponds to the construction of compositors for identifications and associators for the resulting compositions, \etc.
117
+
\begin{proof}
118
+
Let $q:\Singleton{A}{u}\vdash B^\sharp\prn{u} : \TYPE$ be the family $B^\sharp\prn{\prn{y,p}} :\equiv B\prn{y,p}$. For any $y:A$ and $p:\Id{A}{x}{y}$ we have by the contractiblity of singletons (\cref{cor:contractibility-of-singletons}) an identification $\Phi_{u}\,\prn{y,p}: \Id{\Singleton{A}{u}}{\prn{u,\Refl}}{\prn{y,p}}$. By transport (\cref{cor:transport}), we have $\prn{\Phi_{u}\,\prn{y,p}}_*^{B^\sharp}\colon B\prn{x,\Refl}\to B\prn{y,p}$.
119
+
%
120
+
We may therefore define $y,p\vdash f:\prn{y,p}:B\prn{y,p}$ to be
121
+
$\prn{\Phi_{u}\,\prn{y,p}}_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}$, as we have the following definitional equivalences:
122
+
\[
123
+
\prn{\Phi_{u}\,\prn{u,\Refl}}_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}
124
+
\equiv
125
+
\Refl_*^{B^{\sharp}}\prn{f\prn{u,\Refl}}
126
+
\equiv f\prn{u,\Refl}
127
+
\qedhere
128
+
\]
129
+
\end{proof}
134
130
135
-
% \begin{construction}[Unbiased compositor]\label[construction]{con:unbiased-compositor}
136
-
% For each $p:\Id{A}{u}{v}$ and $q:\Id{A}{v}{w}$, we may define an identification $p\ct q:\Id{A}{u}{w}$ in such a way that $\Refl\ct\Refl \equiv \Refl$.
137
-
% \end{construction}
131
+
Independently, \citet{van-den-berg-garner:2011} and \citet{lumsdaine:2010} have shown that identification induction exhibits a weak globular $\infty$-groupoid structure on each type $A$. In the lowest dimension, this corresponds to the construction of compositors for identifications and associators for the resulting compositions, \etc.
138
132
139
-
% \begin{proof}
140
-
% Generalising over all our assumptions, define the following term using \cref{principle:based-identification-induction} followed by \cref{principle:identification-induction}:
133
+
\begin{construction}[Unbiased compositor]\label[construction]{con:unbiased-compositor}
134
+
For each $p:\Id{A}{u}{v}$ and $q:\Id{A}{v}{w}$, we may define an identification $p\ct q:\Id{A}{u}{w}$ in such a way that $\Refl\ct\Refl \equiv \Refl$.
135
+
\end{construction}
141
136
142
-
% \iblock{
143
-
% \mhang{
144
-
% x,y:A; p:\Id{A}{x}{y}, z : A, q : \Id{A}{y}{z}
145
-
% \vdash p\ct q : \Id{A}{x}{z}
146
-
% }{
147
-
% \commentrow{by \cref{principle:based-identification-induction}}
148
-
% \mrow{
149
-
% x,y:A;p:\Id{A}{x}{y} \vdash p \ct\Refl : \Id{A}{x}{y}
150
-
% }
151
-
% \commentrow{by \cref{principle:identification-induction}}
152
-
% \mrow{
153
-
% x:A\vdash \Refl\ct\Refl : \Id{A}{x}{x}
154
-
% }
155
-
% \commentrow{by reflexivity}
156
-
% \mrow{
157
-
% x:A\vdash \Refl\ct\Refl :\equiv \Refl
158
-
% }
159
-
% \qedhere
160
-
% }
161
-
% }
162
-
% \end{proof}
137
+
\begin{proof}
138
+
Generalising over all our assumptions, define the following term using \cref{principle:based-identification-induction} followed by \cref{principle:identification-induction}:
163
139
164
-
% \begin{construction}[Left unitor]
165
-
% For any $p:\Id{A}{u}{v}$, we may define an identification $\mathsf{lunit}_p:\Id{\Id{A}{u}{v}}{\Refl\ct p}{p}$ in such a way that $\mathsf{lunit}_{\Refl} \equiv \Refl$.
166
-
% \end{construction}
167
-
% \begin{proof}
168
-
% We define the following term using \cref{principle:identification-induction}:
140
+
\iblock{
141
+
\mhang{
142
+
x,y:A; p:\Id{A}{x}{y}, z : A, q : \Id{A}{y}{z}
143
+
\vdash p\ct q : \Id{A}{x}{z}
144
+
}{
145
+
\commentrow{by \cref{principle:based-identification-induction}}
146
+
\mrow{
147
+
x,y:A;p:\Id{A}{x}{y} \vdash p \ct\Refl : \Id{A}{x}{y}
148
+
}
149
+
\commentrow{by \cref{principle:identification-induction}}
150
+
\mrow{
151
+
x:A\vdash \Refl\ct\Refl : \Id{A}{x}{x}
152
+
}
153
+
\commentrow{by reflexivity}
154
+
\mrow{
155
+
x:A\vdash \Refl\ct\Refl :\equiv \Refl
156
+
}
157
+
\qedhere
158
+
}
159
+
}
160
+
\end{proof}
169
161
170
-
% \iblock{
171
-
% \mhang{
172
-
% x,y:A;p:\Id{A}{x}{y} \vdash \mathsf{lunit}_p : \Id{\Id{A}{x}{y}}{\Refl\ct p}{p}
173
-
% }{
174
-
% \commentrow{by \cref{principle:identification-induction}}
175
-
% \mrow{
176
-
% x:A\vdash \mathsf{lunit}_\Refl : \Id{\Id{A}{x}{x}}{\Refl\ct \Refl}{\Refl}
177
-
% }
178
-
% \commentrow{by \cref{con:unbiased-compositor}}
179
-
% \mrow{
180
-
% x:A\vdash \mathsf{lunit}_\Refl : \Id{\Id{A}{x}{x}}{\Refl}{\Refl}
181
-
% }
182
-
% \commentrow{by reflexivity}
183
-
% \mrow{
184
-
% x:A\vdash \mathsf{lunit}_\Refl :\equiv \Refl
185
-
% }
186
-
% \qedhere
187
-
% }
188
-
% }
189
-
% \end{proof}
162
+
\begin{construction}[Left unitor]
163
+
For any $p:\Id{A}{u}{v}$, we may define an identification $\mathsf{lunit}_p:\Id{\Id{A}{u}{v}}{\Refl\ct p}{p}$ in such a way that $\mathsf{lunit}_{\Refl} \equiv \Refl$.
164
+
\end{construction}
165
+
\begin{proof}
166
+
We define the following term using \cref{principle:identification-induction}:
190
167
191
-
% \begin{exercise}[Associator]
192
-
% For any identifications $p:\Id{A}{t}{u}$, $q:\Id{A}{u}{v}$, and $r:\Id{A}{v}{w}$, constructor an identification $\alpha_{p,q,r}:\Id{\Id{A}{t}{w}}{\prn{p\ct q}\ct r}{p\ct\prn{q\ct r}}$ in such a way that $\alpha_{\Refl,\Refl,\Refl} \equiv \Refl$.
193
-
% \end{exercise}
168
+
\iblock{
169
+
\mhang{
170
+
x,y:A;p:\Id{A}{x}{y} \vdash \mathsf{lunit}_p : \Id{\Id{A}{x}{y}}{\Refl\ct p}{p}
171
+
}{
172
+
\commentrow{by \cref{principle:identification-induction}}
173
+
\mrow{
174
+
x:A\vdash \mathsf{lunit}_\Refl : \Id{\Id{A}{x}{x}}{\Refl\ct \Refl}{\Refl}
175
+
}
176
+
\commentrow{by \cref{con:unbiased-compositor}}
177
+
\mrow{
178
+
x:A\vdash \mathsf{lunit}_\Refl : \Id{\Id{A}{x}{x}}{\Refl}{\Refl}
179
+
}
180
+
\commentrow{by reflexivity}
181
+
\mrow{
182
+
x:A\vdash \mathsf{lunit}_\Refl :\equiv \Refl
183
+
}
184
+
\qedhere
185
+
}
186
+
}
187
+
\end{proof}
194
188
195
-
% Higher identities relating different ways of composing the associators and unitors can be established in the same way as the above.
189
+
\begin{exercise}[Associator]
190
+
For any identifications $p:\Id{A}{t}{u}$, $q:\Id{A}{u}{v}$, and $r:\Id{A}{v}{w}$, constructor an identification $\alpha_{p,q,r}:\Id{\Id{A}{t}{w}}{\prn{p\ct q}\ct r}{p\ct\prn{q\ct r}}$ in such a way that $\alpha_{\Refl,\Refl,\Refl} \equiv \Refl$.
191
+
\end{exercise}
196
192
197
-
% \begin{construction}[Biased compositors]
198
-
% For each $p:\Id{A}{u}{v}$ and $q:\Id{A}{v}{w}$ we may define identifications $p \ctl q, p \ctr q: \Id{A}{u}{w}$ such that $\Refl \ctl
199
-
% q \equiv q$ and $p\ctr \Refl \equiv p$.
200
-
% \end{construction}
193
+
Higher identities relating different ways of composing the associators and unitors can be established in the same way as the above.
201
194
202
-
% \begin{proof}
203
-
% The right-biased compositor is constructed using \cref{principle:based-identification-induction} like so:
195
+
\begin{construction}[Biased compositors]
196
+
For each $p:\Id{A}{u}{v}$ and $q:\Id{A}{v}{w}$ we may define identifications $p \ctl q, p \ctr q: \Id{A}{u}{w}$ such that $\Refl \ctl
197
+
q \equiv q$ and $p\ctr \Refl \equiv p$.
198
+
\end{construction}
204
199
205
-
% \iblock{
206
-
% \mhang{
207
-
% x,y:A;p:\Id{A}{x}{y},z:A,q:\Id{A}{y}{z} \vdash p \ctr q : \Id{A}{x}{z}
208
-
% }{
209
-
% \commentrow{by \cref{principle:based-identification-induction}}
210
-
% \mrow{
211
-
% x,y:A;p:\Id{A}{x}{y} \vdash p \ctr \Refl : \Id{A}{x}{y}
212
-
% }
213
-
% \commentrow{by hypothesis}
214
-
% \mrow{
215
-
% x,y:A;p:\Id{A}{x}{y}\vdash p\ctr\Refl :\equiv p
216
-
% }
217
-
% }
218
-
% }
200
+
\begin{proof}
201
+
The right-biased compositor is constructed using \cref{principle:based-identification-induction} like so:
219
202
220
-
% The left-biased compositor is constructed using \cref{principle:identification-induction} as follows:
203
+
\iblock{
204
+
\mhang{
205
+
x,y:A;p:\Id{A}{x}{y},z:A,q:\Id{A}{y}{z} \vdash p \ctr q : \Id{A}{x}{z}
206
+
}{
207
+
\commentrow{by \cref{principle:based-identification-induction}}
208
+
\mrow{
209
+
x,y:A;p:\Id{A}{x}{y} \vdash p \ctr \Refl : \Id{A}{x}{y}
210
+
}
211
+
\commentrow{by hypothesis}
212
+
\mrow{
213
+
x,y:A;p:\Id{A}{x}{y}\vdash p\ctr\Refl :\equiv p
214
+
}
215
+
}
216
+
}
221
217
222
-
% \iblock{
223
-
% \mhang{
224
-
% x,y:A;p:\Id{A}{x}{y},z:A,q:\Id{A}{y}{z} \vdash p \ctl q : \Id{A}{x}{z}
225
-
% }{
226
-
% \commentrow{by \cref{principle:identification-induction}}
227
-
% \mrow{
228
-
% x,z:A;q:\Id{A}{x}{z} \vdash \Refl \ctl q : \Id{A}{x}{z}
229
-
% }
230
-
% \commentrow{by hypothesis}
231
-
% \mrow{
232
-
% x,z:A;q:\Id{A}{x}{z}\vdash \Refl\ctl q :\equiv q
233
-
% }
234
-
% \qedhere
235
-
% }
236
-
% }
237
-
% \end{proof}
218
+
The left-biased compositor is constructed using \cref{principle:identification-induction} as follows:
238
219
239
-
% \begin{construction}[Action on identifications]\label[construction]{con:act}
240
-
% Given a function $f\colon A\to B$, to each identification $p:\Id{A}{u}{v}$ we may assign an identification $\Act{f}{p}:\Id{B}{fu}{fv}$ such that $\Act{f}{\Refl} \equiv \Refl$. This assignment is called the \emph{action of $f$ on identifications}.\footnote{Owing to the terminology of the HoTT Book~\citep{hottbook}, $\Act{f}$ is often written as $\mathsf{ap}_f$.}
241
-
% \end{construction}
242
-
% \begin{proof}
243
-
% We may define the action of $f$ on identifications by one application of \cref{principle:identification-induction}.
220
+
\iblock{
221
+
\mhang{
222
+
x,y:A;p:\Id{A}{x}{y},z:A,q:\Id{A}{y}{z} \vdash p \ctl q : \Id{A}{x}{z}
223
+
}{
224
+
\commentrow{by \cref{principle:identification-induction}}
225
+
\mrow{
226
+
x,z:A;q:\Id{A}{x}{z} \vdash \Refl \ctl q : \Id{A}{x}{z}
227
+
}
228
+
\commentrow{by hypothesis}
229
+
\mrow{
230
+
x,z:A;q:\Id{A}{x}{z}\vdash \Refl\ctl q :\equiv q
231
+
}
232
+
\qedhere
233
+
}
234
+
}
235
+
\end{proof}
236
+
237
+
\begin{construction}[Action on identifications]\label[construction]{con:act}
238
+
Given a function $f\colon A\to B$, to each identification $p:\Id{A}{u}{v}$ we may assign an identification $\Act{f}{p}:\Id{B}{fu}{fv}$ such that $\Act{f}{\Refl} \equiv \Refl$. This assignment is called the \emph{action of $f$ on identifications}.\footnote{Owing to the terminology of the HoTT Book~\citep{hottbook}, $\Act{f}$ is often written as $\mathsf{ap}_f$.}
239
+
\end{construction}
240
+
\begin{proof}
241
+
We may define the action of $f$ on identifications by one application of \cref{principle:identification-induction}.
244
242
245
-
% \iblock{
246
-
% \mhang{
247
-
% x,y:A;p:\Id{A}{x}{y} \vdash \Act{f}p : \Id{B}{fx}{fy}
248
-
% }{
249
-
% \commentrow{by \cref{principle:identification-induction}}
250
-
% \mrow{
251
-
% x:A\vdash \Act{f}\Refl : \Id{B}{fx}{fx}
252
-
% }
253
-
% \commentrow{by reflexivity}
254
-
% \mrow{
255
-
% x:A\vdash \Act{f}{\Refl} :\equiv \Refl
256
-
% }
257
-
% \qedhere
258
-
% }
259
-
% }
260
-
% \end{proof}
243
+
\iblock{
244
+
\mhang{
245
+
x,y:A;p:\Id{A}{x}{y} \vdash \Act{f}p : \Id{B}{fx}{fy}
246
+
}{
247
+
\commentrow{by \cref{principle:identification-induction}}
248
+
\mrow{
249
+
x:A\vdash \Act{f}\Refl : \Id{B}{fx}{fx}
250
+
}
251
+
\commentrow{by reflexivity}
252
+
\mrow{
253
+
x:A\vdash \Act{f}{\Refl} :\equiv \Refl
254
+
}
255
+
\qedhere
256
+
}
257
+
}
258
+
\end{proof}
261
259
262
-
% \begin{construction}[Action of the identity map]\label[construction]{con:act-idn}
263
-
% For any identification $p:\Id{A}{u}{v}$, we can define a higher identification $\ActIdn\,p : \Id{\Id{A}{u}{v}}{\Act{1_A}{p}}{p}$ witnessing that the action of the identity function is the identity function on identifications, such that we have $\ActIdn\,\Refl \equiv \Refl$.
264
-
% \end{construction}
265
-
% \begin{proof}
266
-
% We may construct the witness using \cref{principle:identification-induction} as follows:
260
+
\begin{construction}[Action of the identity map]\label[construction]{con:act-idn}
261
+
For any identification $p:\Id{A}{u}{v}$, we can define a higher identification $\ActIdn\,p : \Id{\Id{A}{u}{v}}{\Act{1_A}{p}}{p}$ witnessing that the action of the identity function is the identity function on identifications, such that we have $\ActIdn\,\Refl \equiv \Refl$.
262
+
\end{construction}
263
+
\begin{proof}
264
+
We may construct the witness using \cref{principle:identification-induction} as follows:
267
265
268
-
% \iblock{
269
-
% \mhang{
270
-
% x,y:A; p:\Id{A}{u}{v} \vdash \ActIdn\,p : \Id{\Id{A}{x}{y}}{\Act{1_A}{p}}{p}
271
-
% }{
272
-
% \commentrow{by \cref{principle:identification-induction}}
273
-
% \mrow{
274
-
% x:A \vdash \ActIdn\,\Refl : \Id{\Id{A}{x}{y}}{\Act{1_A}{\Refl}}{p}
275
-
% }
276
-
% \commentrow{by \cref{con:act}}
277
-
% \mrow{
278
-
% x:A \vdash \ActIdn\,\Refl : \Id{\Id{A}{x}{y}}{p}{p}
279
-
% }
280
-
% \commentrow{by reflexivity}
281
-
% \mrow{
282
-
% x:A\vdash \ActIdn\,\Refl :\equiv \Refl
283
-
% }
284
-
% \qedhere
285
-
% }
286
-
% }
287
-
% \end{proof}
266
+
\iblock{
267
+
\mhang{
268
+
x,y:A; p:\Id{A}{u}{v} \vdash \ActIdn\,p : \Id{\Id{A}{x}{y}}{\Act{1_A}{p}}{p}
269
+
}{
270
+
\commentrow{by \cref{principle:identification-induction}}
271
+
\mrow{
272
+
x:A \vdash \ActIdn\,\Refl : \Id{\Id{A}{x}{y}}{\Act{1_A}{\Refl}}{p}
273
+
}
274
+
\commentrow{by \cref{con:act}}
275
+
\mrow{
276
+
x:A \vdash \ActIdn\,\Refl : \Id{\Id{A}{x}{y}}{p}{p}
277
+
}
278
+
\commentrow{by reflexivity}
279
+
\mrow{
280
+
x:A\vdash \ActIdn\,\Refl :\equiv \Refl
281
+
}
282
+
\qedhere
283
+
}
284
+
}
285
+
\end{proof}
286
+
\end{xsect}
288
287
289
-
% \end{xsect}
288
+
\begin{xsect}{Characterising identity types using (displayed) reflexive graphs}
290
289
291
-
% \begin{xsect}{Working with specific identity types}
292
-
% Although Martin-L\"of's identity types exhibit a well-behaved globular structure uniformly across all types, it is not easy to work with identifications in any \emph{specific} type. This is because the rules of the identity types $\Id{A}{u}{v}$ are completely general and not attuned to the specifics of any given type $A$. For this reason, wise practitioners of the formalisation of univalent foundations in homotopy type theory have found it to be essential to \emph{immediately} characterise the identity type of any given type in terms of simpler types.
290
+
The role of the identity type is similar to that of equality in set theory: it expresses a single \emph{global} notion of identification whose rules apply to all types simultaneously.\footnote{Naturally, intensional type theory can speak about more than sets --- but the spirit of having a single global notion of identity is the same in both type theory and set theory.} On the other hand, because the rules of identity types have to apply uniformly to all types, these rules do not reflect any of the specific characteristics of individual types that would, if taken seriously, make it easier to both exhibit and use identifications.
293
291
294
-
% Some of these characterisations are derivable in pure intensional type theory; for example, we can characterise the identity type of a sum $\Sum{x:A}B\prn{x}$ in terms of the identity types of $A$ and of each $B\prn{x}$.
292
+
\begin{remark}
293
+
Everything in this section is derived from prior works, such as the HoTT Book~\citep{hottbook}, Rijke's textbook on homotopy type theory~\citep{rijke:2022}, and the work of \citet{schipp-von-branitz-buchholtz:2021}, although we do impose our own terminological conventions.
294
+
\end{remark}
295
295
296
-
% \begin{proposition}\label[proposition]{prop:id-dsum}
297
-
% The following dependent function defined by identification induction is a family of equivalences:
298
-
% \begin{align*}
299
-
% & f:\Prod{u,v:\DelimProtect{\Sum{x:A}B\prn{x}}} \Id{\Sum{x:A}B\prn{x}}{u}{v} \to \Sum{p:\Id{A}{\pi_1 u}{\pi_1 v}} \Id{B\prn{\pi_1 v}}{p_*^B\prn{\pi_2u}}{\pi_2\prn{v}} \\
300
-
% & f\, u\, u\, \Refl :\equiv \prn{\Refl, \Refl}
301
-
% \end{align*}
302
-
% \end{proposition}
296
+
\begin{xsect}[sec:shallow]{Shallow characterisation of identity types}
297
+
For example, it is very natural to build up an identification of type $\Id{A\times B}{\prn{x,u}}{\prn{y,v}}$ from a pair of identifications $\Id{A}{x}{y}$ and $\Id{B}{u}{v}$. This principle can be formalised by \emph{characterising} the identity type of $A\times B$ in terms of the identity types of $A$ and $B$.
303
298
304
-
% In other words, we have an equivalence between the identity type $\Id{\Sum{x:A}B\prn{x}}{u}{v}$ of a sum, and the sum $\Sum{p:\Id{A}{\pi_1 u}{\pi_1 v}} \Id{B\prn{\pi_1 v}}{p_*^B\prn{\pi_2u}}{\pi_2\prn{v}}$ of identity types.
299
+
\begin{proposition}[Shallow characterisation of the binary product]\label[proposition]{ex:shallow-bin-prod}
300
+
Each of the following functions is an equivalence:
301
+
\begin{align*}
302
+
x,y:A; u,v:B & \vdash \mathsf{splitId}_{A,B} \colon : \Id{A\times B}{\prn{x,u}}{\prn{y,v}} \to \prn{\Id{A}{x}{y}}\times \prn{\Id{B}{u}{v}}
303
+
\\
304
+
x:A, u:B & \vdash \mathsf{splitId}_{A,B} ~\Refl :\equiv \prn{\Refl, \Refl}
305
+
\end{align*}
306
+
\end{proposition}
307
+
\begin{proof}
308
+
We can explicitly construct an inverse to $\mathsf{splitId}_{A,B}$ as follows:
309
+
\begin{align*}
310
+
x,y:A; u,v:B
311
+
& \vdash
312
+
\mathsf{unsplitId}_{A,B} \colon : \prn{\Id{A}{x}{y}}\times \prn{\Id{B}{u}{v}} \to \Id{A\times B}{\prn{x,u}}{\prn{y,v}}
313
+
\\
314
+
x:A, u:V
315
+
& \vdash
316
+
\mathsf{unsplitId}_{A,B}\,\prn{\Refl,\Refl} :\equiv \Refl
317
+
\end{align*}
305
318
319
+
The coherences of the equivalence are given by identification induction.
320
+
\end{proof}
306
321
307
-
% \begin{xsect}{Motivating path objects and displayed path objects}
308
-
% Although \cref{prop:id-dsum} is a fundamental result in intensional type theory, it is inadequate in practice for two reasons.
309
-
% %
310
-
% \begin{enumerate}
311
-
% \item \textbf{What if $A$ and $B$ are complex types?} If $A$ and $B$ are specific complex types (\eg perhaps they are sums themselves), we would want to characterise the identity type of $\Sum{x:A}B\prn{x}$ not in terms of the identity types of $A$ and $B\prn{x}$ but rather in terms of some (other) characterisations of these identity types.
312
-
% \item \textbf{The presence of transports.} Although we have succeeded to decompose identifications in sums $\Sum{x:A}B\prn{x}$ in terms of identifications in $A$ and identifications in $B\prn{x}$, we still have to deal with the presence of the \emph{transport} function $p_*^B\colon B\prn{\pi_1u}\to B\prn{\pi_1v}$ in the latter --- necessitated from the fact that $B\prn{x}$ is dependent on $x:A$. Just as identifications in specific types are not easy to work with because of the generality of the rules, \emph{transports} in specific families are likewise prohibitively difficult to work with.
313
-
% \end{enumerate}
322
+
Of course, although the characterisation of identifications in $A\times B$ in \cref{ex:shallow-bin-prod} is useful, it does not help us directly to characterise identifications in more complex types. For example, we may wish to characterise the identity type of $\prn{A\times B}\times C$ by asserting that the canonical map $\Id{\prn{A\times B}\times C}{\prn{\prn{x,u},m}}{\prn{\prn{y,v},n}}\to \prn{\prn{\Id{A}{x}{y}}\times\prn{\Id{B}{u}{v}}}\times\prn{\Id{C}{m}{n}}$ is an equivalence. This can be established directly in the same way as \cref{ex:shallow-bin-prod}, but this existing lemma does not help do so. Naturally, it would be better to have a toolkit for building up ``deep'' characterisations of identity types piece-by-piece.
314
323
315
-
% To address the first problem, several equivalent type theoretic notions of \emph{path object} have been introduced and employed systematically, \eg in the textbook of \citet{rijke:2022}, the agda-unimath library~\citep{agda-unimath}, or the 1Lab~\citep{1lab}.\footnote{Our terminology of \emph{path object} refers to what the HoTT Book~\citep{hottbook}, \citet{rijke:2022} and many other authors refer to as \emph{identity systems}; they are referred to by \citet{schipp-von-branitz-buchholtz:2021} as \emph{univalent reflexive graphs} and by \citet{rijke:2019} as \emph{discrete reflexive graphs}.} To a first approximation, a path object is a reflexive graph structure that imposes a computationally tractable notion of identification on its vertices --- such that this computationally tractable notion is equivalent to the one provided by the identity type.
324
+
\end{xsect}
316
325
317
-
% To address the problem of transports between components of dependent types, it has been necessary to introduce \emph{displayed} or \emph{heterogeneous} versions of path objects that allow an identification in a family $B\prn{x}$ to span from $B\prn{u}$ to $B\prn{v}$ along some identification from $u$ to $v$.
326
+
\begin{xsect}{Deep characterisation using reflexive graphs}
327
+
A ``deep'' characterisation of the identity type for binary products would take the following form:
318
328
319
-
% \end{xsect}
329
+
\begin{quote}
330
+
If we have characterised the identity type of $A$ and the identity type of $B$, then we may characterise the identity type of $A\times B$.
331
+
\end{quote}
320
332
333
+
\cref{ex:shallow-bin-prod} can be ``deepened'' along these lines by replacing the types $A$ and $B$ with \emph{reflexive graphs} $\gA$ and $\gB$ so that we have the following data:
321
334
322
-
% \begin{xsect}{Disadvantageous of displayed path objects}
323
-
% Displayed path objects have enabled the characterisation of identity types for very complicated dependent types, including (for instance) those of groups, categories, and other sophisticated structures.
324
-
% %
325
-
% On the other hand, because a displayed path object is not just a special kind of path object (or a family of path objects), it has been challenging to develop a toolkit of \emph{composable} results for building up complex path objects in the presence of type dependency.
335
+
\begin{multicols}{2}
336
+
\iblock{
337
+
\mrow{\vrt{\gA} : \TYPE}
338
+
\mrow{{\Edge{\gA}} : \vrt{\gA}\to \vrt{\gA}\to \TYPE}
339
+
\mrow{\Rx{\gA} : \Prod{x:\vrt{\gA}} x\Edge{\gA}x}
340
+
\columnbreak
341
+
\mrow{\vrt{\gB} : \TYPE}
342
+
\mrow{{\Edge{\gB}} : \vrt{\gB}\to \vrt{\gB}\to \TYPE}
343
+
\mrow{\Rx{\gB} : \Prod{x:\vrt{\gB}} x\Edge{\gB}x}
344
+
}
345
+
\end{multicols}
326
346
327
-
% In fact, most displayed path objects that occur in practice arise in a specific way from a family of ordinary path objects --- which we systematise in this paper with the aim of improving compositionality in the practical characterisation of identity types.
328
-
% \end{xsect}
329
-
% \end{xsect}
347
+
These reflexive graph structures follow the pattern of instances of the formation and introduction rules for the identity type. Tentatively, we shall say that a given reflexive graph $\gG$ is \DefEmph{univalent} when the following function is an equivalence:\footnote{See \cref{def:univalent-reflexive-graph}; in fact, our provisional definition of the univalence condition for a reflexive graph is not the most practical one for everyday use, but it is one of several equivalent conditions that we shall expose later.}
348
+
\begin{align*}
349
+
x,y:\vrt{\gG} & \vdash \mathsf{idToEdge}_\gG^{x,y} : \Id{\vrt{\gG}}{x}{y} \to x\Edge{\gG}y
350
+
\\
351
+
x:\vrt{\gG} & \vdash \mathsf{idToEdge}_\gG^{x,x} \Refl :\equiv \Rx{\gG}{x}
352
+
\end{align*}
353
+
354
+
We shall often refer to a univalent reflexive graph as a \DefEmph{path object} for short. With these constructions on reflexive graphs in hand, a \emph{deep} characterisation of the identity type for binary products can be formulated.
355
+
356
+
First we define a new reflexive graph $\gA\times \gB$ as follows:
357
+
\begin{align*}
358
+
\vrt{\gA\times \gB}
359
+
& :\equiv
360
+
\vrt{\gA}\times \vrt{\gB}
361
+
\\
362
+
\prn{x,u} \Edge{\gA\times \gB} \prn{y,v}
363
+
& :\equiv
364
+
\prn{x\Edge{\gA}y}
365
+
\times
366
+
\prn{u\Edge{\gB}v}
367
+
\\
368
+
\Rx{\gA\times\gB}\prn{x,u}
369
+
& :\equiv
370
+
\prn{\Rx{\gA}{x},\Rx{\gB}{u}}
371
+
\end{align*}
372
+
373
+
Then the deep characterisation of binary products amounts saying that path objects (\ie univalent reflexive graphs) are closed under binary products.
374
+
375
+
\begin{proposition}[Deep characterisation of the binary product]\label[proposition]{prop:deep-bin-prod}
376
+
If $\gA$ and $\gB$ are two path objects, then $\gA\times \gB$ is a path object.
377
+
\end{proposition}
378
+
379
+
The compositional character of \cref{prop:deep-bin-prod} allows us to deduce other useful corollaries immediately by iteration. For example, if $\gA,\gB,\gC$ are all univalent reflexive graphs, then $\prn{\gA\times\gB}\times\gC$ is a univalent reflexive graph, \etc
380
+
\end{xsect}
381
+
382
+
\begin{xsect}{Dependent types and displayed reflexive graphs}
383
+
384
+
So far we have described how to give shallow and deep characterisations of \emph{non-dependent} types. Of course, most mathematical structures of any interest (\eg monoids, groups, rings, \etc, or even reflexive graphs themselves!) are described by dependent types, as the types of the operations depend on the carrier types.
385
+
386
+
Given a type $A:\TYPE$ and a family of types $x:A\vdash B\prn{x} : \TYPE$, how can we characterise the identity type of the sum $\Sum{x:A}B\prn{x}$? A shallow characterisation in the style of \cref{sec:shallow} is at least not out of reach.
387
+
388
+
\begin{proposition}[Shallow characterisation of the indexed sum]\label[proposition]{prop:shallow-dependent}
389
+
Each of the following functions is an equivalence:
390
+
391
+
\iblock{
392
+
\mhang{
393
+
x,y:A; u:B\prn{x}, v:B\prn{y} \vdash
394
+
}{
395
+
\mrow{
396
+
\mathsf{dsplitId}_{A,B} \colon \Id{\Sum{x:A}{B\prn{x}}}{\prn{x,u}}{\prn{y,v}}
397
+
\to
398
+
\Sum{p:\Id{A}{x}{y}}
399
+
\Id{B\prn{y}}{p_*^B u}{v}
400
+
}
401
+
\mrow{
402
+
\mathsf{dsplitId}_{A,B}\,\Refl :\equiv \prn{\Refl,\Refl}
403
+
}
404
+
}
405
+
}
406
+
\end{proposition}
407
+
408
+
The shallow characterisation in \cref{prop:shallow-dependent} is more complex than that of \cref{ex:shallow-bin-prod} because the second component of the the sum $\Sum{p:\Id{A}{x}{y}}
409
+
\Id{B\prn{y}}{p_*^B u}{v}$ involves a \emph{transport}. From a higher vantage point, the problem being solved by transport here is that we wish to identify $u:B\prn{x}$ with $v:B\prn{y}$ but these do not have the same type. Transport uses the identification $p:\Id{A}{x}{y}$ to find a common type in which $u$ and $v$ can be compared; but note that the choice of a forward transport $p_*^B\colon B\prn{x}\to B\prn{y}$ is somewhat arbitrary, as we might have also defined a backward transport $p^*_B \colon B\prn{y}\to B\prn{x}$ and compared $u,v$ in $B\prn{x}$.
410
+
411
+
In order to generalise \cref{prop:shallow-dependent} to a \emph{deep} characterisation of the indexed sum, we must naturally generalise the concept of reflexive graph to one in which vertices form a \emph{dependent} type and edges go between different components linked by an edge in the base. This is precisely the purpose of the \emph{displayed reflexive graphs} of \cite{schipp-von-branitz-buchholtz:2021}.
412
+
413
+
In particular, let $\gA$ be a reflexive graph as before and let $\gB$ be a \DefEmph{displayed reflexive graph} over $\gA$ so that we have the following data:
414
+
415
+
\begingroup
416
+
\setlength\columnsep{-4cm}
417
+
\begin{multicols}{2}
418
+
\iblock{
419
+
\mrow{\vrt{\gA} : \TYPE}
420
+
\mrow{{\Edge{\gA}} : \vrt{\gA}\to \vrt{\gA}\to \TYPE}
421
+
\mrow{\Rx{\gA} : \Prod{x:\vrt{\gA}} x\Edge{\gA}x}
422
+
\columnbreak
423
+
\mrow{\vrt{\gB} : \vrt{\gA}\to \TYPE}
424
+
\mrow{{\Edge{\gB}[\bullet]} : \Prod[\brc]{x,y:\vrt{\gA}} x\Edge{\gA}y\to \vrt{\gB}\prn{x}\to \vrt{\gB}\prn{y}\to \TYPE}
425
+
\mrow{\DRx{\gB}{\bullet} : \Prod{x:\vrt{\gA}}\Prod{u:\vrt{\gB}\prn{x}} u\Edge{\gB}[\Rx{\gA}{x}]u}
426
+
}
427
+
\end{multicols}
428
+
\endgroup
429
+
430
+
Any displayed reflexive graph such as $\gB$ gives rise to a family of ordinary reflexive graphs $\gB\prn{x}$ indexed in vertices $x:\vrt{\gA}$.
431
+
\begin{align*}
432
+
\vrt{\gB\prn{x}}
433
+
& :\equiv
434
+
\vrt{\gB}\prn{x}
435
+
\\
436
+
u \Edge{\gB\prn{x}} v
437
+
& :\equiv
438
+
u \Edge{\gB}[\Rx{\gA}{x}] v
439
+
\\
440
+
\Rx{\gB\prn{x}}{u}
441
+
& :\equiv
442
+
\DRx{\gB}{x}{u}
443
+
\end{align*}
444
+
445
+
446
+
A displayed reflexive graph $\gB$ will be called \DefEmph{univalent} (or a displayed path object for short) when each of its components is univalent. We can now define the \DefEmph{total reflexive graph} of $\gB$ with vertices in the sum of $\vrt{\gB}$ over $\vrt{\gA}$ as follows:
447
+
\begin{align*}
448
+
\vrt{\gA.\gB}
449
+
& :\equiv
450
+
\Sum{x:\vrt{\gA}}\vrt{\gB}\prn{x}
451
+
\\
452
+
\prn{x,u} \Edge{\gA.\gB} \prn{y,v}
453
+
& :\equiv
454
+
\Sum{p:x\Edge{\gA}y}
455
+
u\Edge{\gB}[p] v
456
+
\\
457
+
\Rx{\gA.\gB}{\prn{x,u}}
458
+
& :\equiv
459
+
\prn{\Rx{\gA}{x},\DRx{\gB}{x}{u}}
460
+
\end{align*}
461
+
462
+
Then the deep characterisation for indexed sums is exactly the statement that the total reflexive graph of a displayed path object is a path object.
463
+
464
+
\begin{proposition}[Deep characterisation of the indexed sum]\label[proposition]{prop:deep-dependent}
465
+
Let $\gB$ be a displayed path object over a reflexive graph $\gA$. Then the total reflexive graph $\gA.\gB$ is a path object.
466
+
\end{proposition}
467
+
468
+
\end{xsect}
469
+
\end{xsect}
470
+
471
+
472
+
473
+
\begin{xsect}{Characterising \emph{transport} with reflexive graph lenses}
474
+
Everything we have described so far is more or less standard. Path objects (and equivalent concepts such as \emph{torsorial families}) have been used to great effect in a variety of formalised libraries of univalent mathematics, including \texttt{agda-unimath}~\citep{agda-unimath} and the 1Lab~\citep{1lab}. The purpose of the present paper is to give a deeper analysis of a large class of displayed path objects that arise in a particularly simple way, in fact obviating the need to separately prove many univalence lemmas. We return to the shallow characterisation of the identity types of dependent sums from \cref{prop:shallow-dependent}:
475
+
\[
476
+
\Id{\Sum{x:A}B\prn{x}}{\prn{x,u}}{\prn{y,v}} \cong
477
+
\Sum{p:\Id{A}{x}y}
478
+
\Id{B\prn{y}}{p_*^Bu}{v}
479
+
\]
480
+
481
+
In our deep characterisation (\cref{prop:deep-dependent}), we generalised $\Id{A}{x}{y}$ to the edges $x\Edge{\gA}y$ of a reflexive graph $\gA$ and we generalised $\Id{B\prn{y}}{p_*^Bu}{v}$ to the \emph{displayed edges} $u\Edge{\gB}[p]{v}$ of a displayed reflexive graph $\gB$ over $\gA$. This generalisation abstracts away the use of transport to get the vertices $u$ and $v$ to lie in the same component of $B$, at the cost of needing to specify $\gB$ as a displayed reflexive graph rather than as a family of reflexive graphs indexed in $\gA$.
482
+
483
+
Our starting point is to consider a different, less abstract, generalisation of \cref{prop:shallow-dependent} in which we replace $A$ with a reflexive graph $\gA$ as before, but we replace $B$ not with a displayed reflexive graph over $\gA$, but instead with a \emph{family} of reflexive graphs $\gB\prn{x}$ indexed in vertices $x:\vrt{\gA}$ that is equipped with a \emph{transport} or \emph{pushforward} operation to jump from one component to the next. To a first approximation, we have assumed the following data:
484
+
485
+
\iblock{
486
+
\setlength\columnsep{-3cm}
487
+
\begin{multicols}{2}
488
+
\mrow{\vrt{\gA} : \TYPE}
489
+
\mrow{{\Edge{\gA}} : \vrt{\gA}\to \vrt{\gA}\to \TYPE}
490
+
\mrow{\Rx{\gA} : \Prod{x:\vrt{\gA}} x\Edge{\gA}x}
491
+
\columnbreak
492
+
\mrow{\vrt{\gB\prn{-}} : \vrt{\gA}\to \TYPE}
493
+
\mrow{{\Edge{\gB\prn{-}}} : \Prod{x:\vrt{\gA}} \vrt{\gB\prn{x}}\to\vrt{\gB\prn{x}}\to \TYPE}
494
+
\mrow{\Rx{\gB\prn{-}} : \Prod{x:\vrt{\gA}}\Prod{u:\vrt{\gB}\prn{x}} u\Edge{\gB}u}
495
+
\end{multicols}
496
+
\mrow{
497
+
\Push{\gB}{} :
498
+
\Prod[\brc]{x,y:\vrt{\gA}}
499
+
\Prod{p:x\Edge{\gA}y}
500
+
\vrt{\gB\prn{x}}\to \vrt{\gB\prn{y}}
501
+
}
502
+
}
503
+
504
+
With this data in hand, we can define an appropriate displayed reflexive graph $\CovDisp{\gA}{\gB}$ over $\gA$ that mirrors the passage from the shallow characterisation (\cref{prop:shallow-dependent}) to the deep characterisation (\cref{prop:deep-dependent}):
505
+
%
506
+
\begin{align*}
507
+
\vrt{\CovDisp{\gA}{\gB}}\prn{x}
508
+
&:\equiv
509
+
\vrt{\gB\prn{x}}
510
+
\\
511
+
u \Edge{\CovDisp{\gA}{\gB}}[p:x\Edge{\gA}y] v
512
+
&:\equiv
513
+
\Push{\gB}{p}{u}\Edge{\gB\prn{y}} v
514
+
\end{align*}
515
+
516
+
It remains to define the displayed reflexivity datum $\DRx{\CovDisp{\gA}{\gB}}{x}{u} : \Push{\gB}{\Rx{\gA}{x}}{u} \Edge{\gB\prn{x}} u$, but we do not have anything on hand from which to define this. We are therefore led to assert this reflexivity datum as part of the \emph{data} of $\gB$:
517
+
518
+
\iblock{
519
+
\mrow{
520
+
\PushRx{\gB}[\bullet] : \Prod{x:\vrt{\gA}} \Prod{u:\vrt{\gB\prn{x}}} \Push{\gB}{\Rx{\gA}{x}}{u} \Edge{\gB\prn{x}} u
521
+
}
522
+
}
523
+
524
+
Thea above has the appearance of an \emph{oplax unitor} for the pushforward operation. Using this oplax unitor, we may finish defining the displayed reflexive graph $\CovDisp{\gA}{\gB}$:
525
+
%
526
+
\begin{align*}
527
+
\DRx{\CovDisp{\gA}{\gB}}{x}{u}
528
+
&:\equiv
529
+
\PushRx{\gB}[x]{u}
530
+
\end{align*}
531
+
532
+
Altogether, we shall refer to a family of reflexive graphs $\gB$ equipped with $\Push{\gB}{}$ and $\PushRx{\gB}[\bullet]$ as an \DefEmph{oplax covariant lens} of reflexive graphs (see \cref{def:oplax-cov-lens}) over $\gA$ --- \emph{covariant} because $\Push{\gB}{}$ implements a forward transport, and \emph{oplax} because of the orientation of the unitor $\PushRx{\gB}$. The terminology of \emph{lenses} is borrowed from \citep{chollet-et-al:2022:lenses}, who use it to refer to an algebraic generalisation of fibrations in which the chosen lifts are not required to have a universal property but instead satisfy a unit law (strictly, in the case of \opcit).
533
+
534
+
Naturally, we can (and will) introduce a dual notion of \emph{lax contravariant lens} for characterising backward transport in a family of reflexive graphs. When $\gB$ is a lax contravariant lens in this sense (see \cref{def:lax-ctrv-lens}), we can likewise associate a displayed reflexive graph $\CtrvDisp{\gA}{\gB}$ in which a displayed edge $u\Edge{\CtrvDisp{\gA}{\gB}}[p:x\Edge{\gA} y] v$ is given by an edge $u \Edge{\gB\prn{x}} \Pull{\gB}{p}{v}$.
535
+
536
+
537
+
\begin{proposition}[See \cref{lem:cov-disp-po}]
538
+
Let $\gB$ be an oplax covariant (\resp lax contravariant) lens of path objects over a reflexive graph $\gA$. Then the displayed reflexive graph $\CovDisp{\gA}{\gB}$ (\resp $\CtrvDisp{\gA}{\gB}$) is univalent.
539
+
\end{proposition}
540
+
541
+
542
+
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.
543
+
544
+
\end{xsect}
545
+
330
546
\end{xsect}
331
547
332
548