-
Notifications
You must be signed in to change notification settings - Fork 1
/
macros.tex
249 lines (181 loc) · 8.32 KB
/
macros.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SPA and SPB
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\SPA}{\ensuremath{\mathsf{SP}_{\mathrm{A}}}}
\newcommand{\SPB}{\ensuremath{\mathsf{SP}_{\mathrm{B}}}}
\newcommand{\nilA}{\ensuremath{\mathsf{nil}}}
\newcommand{\nilB}{\nilA}
\newcommand{\nonindA}{\ensuremath{\mathsf{non}\text{-}\mathsf{ind}}}
\newcommand{\nonindB}{\nonindA}
\newcommand{\AindA}{\ensuremath{\mathsf{A}\text{-}\mathsf{ind}}}
\newcommand{\AindB}{\AindA}
\newcommand{\BindA}{\ensuremath{\mathsf{B}\text{-}\mathsf{ind}}}
\newcommand{\BindB}{\BindA}
\newcommand{\hindex}{\ensuremath{h_{\mathrm{index}}}}
\newcommand{\Aref}{\ensuremath{A_{\mathrm{ref}}}}
\newcommand{\Bref}{\ensuremath{B_{\mathrm{ref}}}}
\newcommand{\Xref}{\ensuremath{X_{\mathrm{ref}}}}
\newcommand{\Yref}{\ensuremath{Y_{\mathrm{ref}}}}
\newcommand{\A}{\ensuremath{X}}
\newcommand{\B}{\ensuremath{Y}}
\newcommand{\ArgA}{\ensuremath{\mathsf{Arg}_{\mathrm{A}}}}
\newcommand{\ArgB}{\ensuremath{\mathsf{Arg}_{\mathrm{B}}}}
\newcommand{\IndexB}{\ensuremath{\mathsf{Index}_{\mathrm{B}}}}
\newcommand{\repA}{\ensuremath{\mathsf{rep}_{\mathrm{X}}}}
\newcommand{\repIndex}{\ensuremath{\mathsf{rep}_{\mathrm{index}}}}
\newcommand{\repB}{\ensuremath{\mathsf{rep}_{\mathrm{Y}}}}
\newcommand{\plOP}{\ensuremath{+_{\mathsf{SP}}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% SPA and SPB when Aref = Bref = 0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\SPAp}{\ensuremath{\mathsf{SP}^{0}_{\mathrm{A}}}}
\newcommand{\SPBp}{\ensuremath{\mathsf{SP}^{0}_{\mathrm{B}}}}
\newcommand{\ArgAp}{\ensuremath{\mathsf{Arg}^{0}_{\mathrm{A}}}}
\newcommand{\ArgBp}{\ensuremath{\mathsf{Arg}^{0}_{\mathrm{B}}}}
\newcommand{\IndexBp}{\ensuremath{\mathsf{Index}^{0}_{\mathrm{B}}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Towards SPB
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Aterm}{\ensuremath{\mathsf{A}\text{-}\mathsf{Term}}}
\newcommand{\Bterm}{\ensuremath{\mathsf{B}\text{-}\mathsf{Term}}}
\newcommand{\termAref}{\ensuremath{\mathsf{a}_{\mathrm{ref}}}}
\newcommand{\termBref}{\ensuremath{\mathsf{b}_{\mathrm{ref}}}}
\newcommand{\termArg}{\ensuremath{\mathsf{arg}}}
\newcommand{\repAbar}{\ensuremath{\overline{\mathsf{rep}_{\mathrm{A}}}}}
\newcommand{\repBbar}{\ensuremath{\overline{\mathsf{rep}_{\mathrm{B}}}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Abbreviations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\gammaA}{\ensuremath{\gamma_{\mathrm{A}}}}
\newcommand{\gammaB}{\ensuremath{\gamma_{\mathrm{B}}}}
\newcommand{\gammaAB}{\gammaA, \gammaB}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% intro and elim
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\introA}{\ensuremath{\mathsf{intro}_{\mathrm{A}}}}
\newcommand{\introB}{\ensuremath{\mathsf{intro}_{\mathrm{B}}}}
\newcommand{\intro}[1]{\ensuremath{\mathsf{intro}_{#1}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The logical framework
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Set}{\ensuremath{\mathsf{Set}}}
\newcommand{\TYPE}{\ensuremath{\mathsf{Type}}}
\newcommand{\zero}{\ensuremath{\mathbf{0}}}
\newcommand{\magic}[1]{\ensuremath{!_{#1}}}
\newcommand{\magicOmit}[1]{\ensuremath{!}}
\newcommand{\one}{\ensuremath{\mathbf{1}}}
\newcommand{\oneelt}{\ensuremath{\star}}
\newcommand{\two}{\ensuremath{\mathbf{2}}}
\newcommand{\twott}{\ensuremath{\mathsf{tt}}}
\newcommand{\twoff}{\ensuremath{\mathsf{ff}}}
\newcommand{\IF}{\ensuremath{\mathsf{if}}}
\newcommand{\THEN}{\ensuremath{\mathsf{then}}}
\newcommand{\ELSE}{\ensuremath{\mathsf{else}}}
\newcommand{\inl}{\ensuremath{\mathsf{inl}}}
\newcommand{\inr}{\ensuremath{\mathsf{inr}}}
\newcommand{\pair}[2]{\ensuremath{\langle #1 , #2\rangle}}
\newcommand{\id}{\ensuremath{\mathsf{id}}}
\newcommand{\Nat}{\ensuremath{\mathbb{N}}}
%%%%%%%%%%
% W-types
%%%%%%%%%%
\newcommand{\Wsup}{\ensuremath{\mathsf{sup}}}
%%%%%%%%%%
% Finite sets
%%%%%%%%%%
\newcommand{\Fin}{\ensuremath{\mathsf{Fin}}}
\newcommand{\finzero}[1]{\ensuremath{\mathsf{z}_{#1}}}
\newcommand{\finzeroBare}{\ensuremath{\mathsf{z}}}
\newcommand{\finsucc}[2]{\ensuremath{\mathsf{s}_{#1}(#2)}}
\newcommand{\finsuccBare}{\ensuremath{\mathsf{s}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Vectors
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Vecind}{\ensuremath{\mathsf{Nonempty}_{\text{ind}}}}
\newcommand{\Vecrec}{\ensuremath{\mathsf{Nonempty}_{\text{rec}}}}
\newcommand{\Vecbare}{\ensuremath{\mathsf{Nonempty}}}
\newcommand{\singleVec}[1]{\ensuremath{[#1]}}
\newcommand{\consVecbare}{\ensuremath{\mathsf{cons}}}
\newcommand{\consVec}[2]{\ensuremath{\consVecbare(#1, #2)}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Contexts and types
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Ctxt}{\ensuremath{\mathsf{Ctxt}}}
\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}
\newcommand{\emptyCtxt}{\ensuremath{\varepsilon}}
\newcommand{\consCtxtbare}{\ensuremath{\triangleright}}
\newcommand{\consCtxt}[2]{\ensuremath{#1 \consCtxtbare #2}}
\newcommand{\baseTybare}{\ensuremath{\iota}}
\newcommand{\baseTy}[1]{\ensuremath{\baseTybare_{#1}}}
\newcommand{\piTybare}{\ensuremath{\Pi}}
\newcommand{\piTy}[3]{\ensuremath{\piTybare_{#1}(#2, #3)}}
\newcommand{\ArgCtxt}{\ensuremath{\mathsf{Arg}_{\Ctxt}}}
\newcommand{\ArgType}{\ensuremath{\mathsf{Arg}_{\Ty}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Sorted lists
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\SortedList}{\ensuremath{\mathsf{SortedList}}}
\newcommand{\lessList}{\ensuremath{\leq_{\text{L}}}}
\newcommand{\nilList}{\ensuremath{\mathsf{nil}}}
\newcommand{\consListbare}{\ensuremath{\mathsf{cons}}}
\newcommand{\consList}[3]{\ensuremath{\consListbare(#1, #2, #3)}}
\newcommand{\nilLess}[1]{\ensuremath{\mathsf{triv}_{#1}}}
%\newcommand{\consLess}[6]{\ensuremath{\ll #5, #6\gg_{#4, #1, #2, #3}}}
\newcommand{\consLess}[6]{\ensuremath{\ll #5, #6\gg}}
\newcommand{\consLessbare}{\ensuremath{\ll \cdot \gg}}
\newcommand{\ArgSList}{\ensuremath{\mathsf{Arg}_{\text{SList}}}}
\newcommand{\ArglessList}{\ensuremath{\mathsf{Arg}_{\lessList}}}
\newcommand{\Listinsert}{\ensuremath{\mathsf{insert}}}
\newcommand{\lessListtrans}[2]{\ensuremath{\mathsf{tra}_{\lessList}(#1, #2)}}
\newcommand{\lessListtransbare}{\ensuremath{\mathsf{tra}_{\lessList}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Surreal numbers
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Sur}{\ensuremath{\mathsf{Surreal}}}
\newcommand{\Surleq}{\ensuremath{\leq}}
\newcommand{\Surnleq}{\ensuremath{\not\leq}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Eliminators
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\elim}{\ensuremath{\mathsf{elim}}}
\newcommand{\stepind}[1]{\ensuremath{\mathsf{step}_{#1}}}
\newcommand{\stepindarg}[1]{\ensuremath{\widetilde{#1}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Pretending to be Agda
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\SHED}{\raisebox{0in}[0in][0in]{\colorbox[rgb]{0.5,1,0.5}{\(\{?\}\)}}}
\newcommand{\SHEDARG}[1]{\colorbox[rgb]{0.5,1,0.5}{\(\{#1\}\)}}
% Omitted arguments
\newcommand{\omitt}{\ensuremath{\_}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Set theoretic model
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\sem}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\newcommand{\cardz}{\ensuremath{\mathfrak{i}_0}}
\newcommand{\cardi}{\ensuremath{\mathfrak{i}_1}}
\newcommand{\rhoextend}[2]{\ensuremath{\rho_{[#1 \mapsto #2]}}}
\newcommand{\colonsimeq}{\ensuremath{\mathrel{\mathop:}\simeq}}
\newcommand{\tstile}{{\ensuremath{\vdash}}} %\sststile{}{}}}
\newcommand{\rst}[1]{\ensuremath{{\mathbin\upharpoonright}%
\raise-.5ex\hbox{#1}}}
\newcommand{\abs}[1]{\ensuremath{\left| #1 \right|}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Theorem environments
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\blackqed}{\hfill\ensuremath{\blacksquare}}
\renewcommand{\qedsymbol}{\ensuremath{\square}}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Example}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "indInd_model"
%%% End: