Compare commits
2 commits
cbf61d6a96
...
4b5cd69a66
| Author | SHA1 | Date | |
|---|---|---|---|
| 4b5cd69a66 | |||
| 9bedfd5aaa |
18 changed files with 9998 additions and 8 deletions
3
.editorconfig
Normal file
3
.editorconfig
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
[*]
|
||||
indent_size = 2
|
||||
indent_style = space
|
||||
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -1 +1,2 @@
|
|||
*.agdai
|
||||
.DS_Store
|
||||
4
Makefile
4
Makefile
|
|
@ -1,7 +1,7 @@
|
|||
GENDIR := html/src/generated
|
||||
|
||||
build-to-html:
|
||||
find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
|
||||
find src \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
|
||||
| rust-parallel -0 agda \
|
||||
--html \
|
||||
--html-dir=$(GENDIR) \
|
||||
|
|
@ -17,6 +17,6 @@ refresh-book: build-to-html
|
|||
mdbook serve html
|
||||
|
||||
deploy: build-book
|
||||
rsync -azrP html/book/ root@veil:/home/blogDeploy/public/hott-book
|
||||
rsync -azrP html/book/ root@veil:/home/blogDeploy/public/research
|
||||
|
||||
.PHONY: build-book build-to-html deploy
|
||||
|
|
@ -13,12 +13,16 @@ macros = "./macros.txt"
|
|||
[preprocessor.chapter-zero]
|
||||
levels = [0]
|
||||
|
||||
[preprocessor.graphviz]
|
||||
command = "mdbook-graphviz"
|
||||
output-to-file = false
|
||||
|
||||
[output.html]
|
||||
additional-js = [
|
||||
# "theme/pagetoc.js"
|
||||
# "theme/pagetoc.js"
|
||||
]
|
||||
additional-css = [
|
||||
"Agda.css",
|
||||
"style.css",
|
||||
# "theme/pagetoc.css"
|
||||
"Agda.css",
|
||||
"style.css",
|
||||
# "theme/pagetoc.css"
|
||||
]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,9 @@
|
|||
# Summary
|
||||
|
||||
- [Front](./front.md)
|
||||
|
||||
# HoTT Book
|
||||
|
||||
- [Chapter 1](./generated/HottBook.Chapter1.md)
|
||||
- [Exercises](./generated/HottBook.Chapter1Exercises.md)
|
||||
- [Chapter 2](./generated/HottBook.Chapter2.md)
|
||||
|
|
@ -16,3 +19,6 @@
|
|||
- [Definition 3.3.1](./generated/HottBook.Chapter3Definition331.md)
|
||||
- [Lemma 3.3.3](./generated/HottBook.Chapter3Lemma333.md)
|
||||
|
||||
# Van Doorn Dissertation
|
||||
|
||||
- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md)
|
||||
|
|
@ -1,6 +1,24 @@
|
|||
# Homotopy Type Theory
|
||||
# Research
|
||||
|
||||
I'm recreating a formalization for the Homotopy Type Theory book as I'm working through it to help me learn.
|
||||
This book tracks my current research goals and progress.
|
||||
|
||||
- [Source](https://git.mzhang.io/school/type-theory)
|
||||
|
||||
```dot process
|
||||
digraph {
|
||||
rankdir="BT"
|
||||
|
||||
subgraph cluster_exploration {
|
||||
label = "random cloud of exploration" {
|
||||
mayconcise [label="concise course" URL="https://git.mzhang.io/school/type-theory/raw/branch/master/resources/MayConcise/ConciseRevised.pdf"]
|
||||
hott [label = "hott book" URL="https://hott.github.io/book/hott-ebook.pdf.html"]
|
||||
}
|
||||
}
|
||||
|
||||
subgraph cluster_thesis {
|
||||
label = "thesis" {
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
3
html/src/hott-front.md
Normal file
3
html/src/hott-front.md
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
# Homotopy Type Theory
|
||||
|
||||
I'm recreating a formalization for the Homotopy Type Theory book as I'm working through it to help me learn.
|
||||
BIN
resources/MayConcise/ConciseRevised.pdf
vendored
BIN
resources/MayConcise/ConciseRevised.pdf
vendored
Binary file not shown.
3
resources/VanDoornDissertation/.gitignore
vendored
Normal file
3
resources/VanDoornDissertation/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
*.aux
|
||||
*.log
|
||||
*.toc
|
||||
1726
resources/VanDoornDissertation/amsalphaurl.bst
vendored
Normal file
1726
resources/VanDoornDissertation/amsalphaurl.bst
vendored
Normal file
File diff suppressed because it is too large
Load diff
395
resources/VanDoornDissertation/dissertation.bbl
vendored
Normal file
395
resources/VanDoornDissertation/dissertation.bbl
vendored
Normal file
|
|
@ -0,0 +1,395 @@
|
|||
\newcommand{\etalchar}[1]{$^{#1}$}
|
||||
\providecommand{\bysame}{\leavevmode\hbox to3em{\hrulefill}\thinspace}
|
||||
\providecommand{\MR}{\relax\ifhmode\unskip\space\fi MR }
|
||||
% \MRhref is called by the amsart/book/proc definition of \MR.
|
||||
\providecommand{\MRhref}[2]{%
|
||||
\href{http://www.ams.org/mathscinet-getitem?mr=#1}{#2}
|
||||
}
|
||||
\providecommand{\href}[2]{#2}
|
||||
\begin{thebibliography}{dMKA{\etalchar{+}}15}
|
||||
|
||||
\bibitem[AB04]{awodey2004Propositions}
|
||||
Steve Awodey and Andrej Bauer, \emph{Propositions as [{T}ypes]}, Journal of
|
||||
Logic and Computation \textbf{14} (2004), no.~4, 447--471.
|
||||
|
||||
\bibitem[AC10]{asperti2010itp}
|
||||
Andrea Asperti and Claudio~Sacerdoti Coen, \emph{Some considerations on the
|
||||
usability of interactive provers}, International Conference on Intelligent
|
||||
Computer Mathematics, Springer, 2010, pp.~147--156.
|
||||
|
||||
\bibitem[ACD{\etalchar{+}}16]{altenkirch2016qiits}
|
||||
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik
|
||||
Nordvall~Forsberg, \emph{{Quotient inductive-inductive types}}, ArXiv
|
||||
e-prints (2016), \href {http://arxiv.org/abs/1612.02346}
|
||||
{\path{arXiv:1612.02346}}.
|
||||
|
||||
\bibitem[AH61]{atiyah1961spectral}
|
||||
Michael~F Atiyah and Friedrich Hirzebruch, \emph{Vector bundles and homogeneous
|
||||
spaces}, Differential geometry, Proceedings of Symposia in Pure Mathematics,
|
||||
no.~3, 1961, pp.~7--38.
|
||||
|
||||
\bibitem[AHW17]{angiuli2017computational}
|
||||
Carlo Angiuli, Robert Harper, and Todd Wilson, \emph{Computational
|
||||
higher-dimensional type theory}, POPL '17: Proceedings of the 44th Annual ACM
|
||||
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, 2017,
|
||||
\href {http://dx.doi.org/10.1145/3009837.3009861}
|
||||
{\path{doi:10.1145/3009837.3009861}}.
|
||||
|
||||
\bibitem[AKL15]{avigad2015limits}
|
||||
Jeremy Avigad, Chris Kapulkin, and Peter~LeFanu Lumsdaine, \emph{Homotopy
|
||||
limits in type theory}, Mathematical Structures in Computer Science
|
||||
\textbf{25} (2015), no.~05, 1040--1070.
|
||||
|
||||
\bibitem[AW09]{awodey2009homotopy}
|
||||
Steve Awodey and Michael~A. Warren, \emph{Homotopy theoretic models of identity
|
||||
types}, Math. Proc. Camb. Phil. Soc., vol. 146, Cambridge Univ Press, 2009,
|
||||
pp.~45--55.
|
||||
|
||||
\bibitem[BCH14]{bezem2014cubicalsets}
|
||||
Marc Bezem, Thierry Coquand, and Simon Huber, \emph{A model of type theory in
|
||||
cubical sets}, 19th International Conference on Types for Proofs and Programs
|
||||
(TYPES 2013), vol.~26, 2014, pp.~107--128.
|
||||
|
||||
\bibitem[BGLL{\etalchar{+}}16]{bauer2016coqhott}
|
||||
Andrej Bauer, Jason Gross, Peter~LeFanu LeFanu~Lumsdaine, Michael Shulman,
|
||||
Matthieu Sozeau, and Bas Spitters, \emph{{The HoTT Library: A formalization
|
||||
of homotopy type theory in Coq}}, ArXiv e-prints (2016), \href
|
||||
{http://arxiv.org/abs/1610.04591} {\path{arXiv:1610.04591}}.
|
||||
|
||||
\bibitem[BH18]{buchholtz2018cellular}
|
||||
Ulrik Buchholtz and Kuen-Bang {Hou (Favonia)}, \emph{{Cellular Cohomology in
|
||||
Homotopy Type Theory}}, ArXiv e-prints (2018), \href
|
||||
{http://arxiv.org/abs/1802.02191} {\path{arXiv:1802.02191}}.
|
||||
|
||||
\bibitem[BHC{\etalchar{+}}]{hottagda}
|
||||
Guillaume Brunerie, Kuen-Bang {Hou (Favonia)}, Evan Cavallo, Eric Finster,
|
||||
Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et~al.,
|
||||
\emph{Homotopy type theory in {A}gda},
|
||||
\url{https://github.com/HoTT/HoTT-Agda}.
|
||||
|
||||
\bibitem[Bla79]{blass1979injectivity}
|
||||
Andreas Blass, \emph{Injectivity, projectivity, and the axiom of choice},
|
||||
Transactions of the American Mathematical Society \textbf{255} (1979),
|
||||
31--59.
|
||||
|
||||
\bibitem[BR16]{buchholtz2016cayleydickson}
|
||||
Ulrik Buchholtz and Egbert Rijke, \emph{The {C}ayley-{D}ickson construction in
|
||||
{H}omotopy {T}ype {T}heory}, ArXiv e-prints (2016), \href
|
||||
{http://arxiv.org/abs/1610.01134} {\path{arXiv:1610.01134}}.
|
||||
|
||||
\bibitem[Bru16]{brunerie2016spheres}
|
||||
Guillaume Brunerie, \emph{On the homotopy groups of spheres in homotopy type
|
||||
theory}, Ph.D. thesis, University of Nice Sophia Antipolis, 2016,
|
||||
\url{https://arxiv.org/abs/1606.05916}.
|
||||
|
||||
\bibitem[BvDR18]{buchholtz2018groups}
|
||||
Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke, \emph{{Higher Groups in
|
||||
Homotopy Type Theory}}, ArXiv e-prints (2018), \href
|
||||
{http://arxiv.org/abs/1802.04315} {\path{arXiv:1802.04315}}.
|
||||
|
||||
\bibitem[Car18]{carneiro2018leantheory}
|
||||
Mario Carneiro, \emph{The type theory of {L}ean}, 2018, online,
|
||||
\url{https://github.com/digama0/lean-type-theory/releases}.
|
||||
|
||||
\bibitem[Cav15]{cavallo2015cohomology}
|
||||
Evan Cavallo, \emph{Synthetic cohomology in homotopy type theory}, Master's
|
||||
thesis, Carnegie Mellon University, 2015,
|
||||
\url{http://www.cs.cmu.edu/~ecavallo/works/thesis.pdf}.
|
||||
|
||||
\bibitem[CCHM]{cubicaltt}
|
||||
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M{\"o}rtberg,
|
||||
\emph{Cubical type theory}, code library,
|
||||
\url{https://github.com/mortberg/cubicaltt}.
|
||||
|
||||
\bibitem[CCHM16]{cohen2016cubical}
|
||||
\bysame, \emph{Cubical type theory: a constructive interpretation of the
|
||||
univalence axiom}, November 2016, \href {http://arxiv.org/abs/1611.02108}
|
||||
{\path{arXiv:1611.02108}}.
|
||||
|
||||
\bibitem[CF58]{curry1958combinatorylogic}
|
||||
Haskell~B. Curry and Robert Feys, \emph{Combinatory logic vol. i}.
|
||||
|
||||
\bibitem[Cis14]{cisinski2014models}
|
||||
Denis-Charles Cisinski, \emph{Univalent universes for elegant models of
|
||||
homotopy types}, ArXiv preprint arXiv:1406.0058 (2014).
|
||||
|
||||
\bibitem[dMKA{\etalchar{+}}15]{moura2015lean}
|
||||
Leonardo de~Moura, Soonho Kong, Jeremy Avigad, Floris {van Doorn}, and Jakob
|
||||
{von Raumer}, \emph{{The {Lean} Theorem Prover (system description)}},
|
||||
CADE-25 (2015), 378--388.
|
||||
|
||||
\bibitem[Dyb94]{dybjer1994inductive}
|
||||
Peter Dybjer, \emph{Inductive families}, Formal aspects of computing \textbf{6}
|
||||
(1994), no.~4, 440--465.
|
||||
|
||||
\bibitem[EK66]{eilenberg1966closedcategories}
|
||||
Samuel Eilenberg and G.~Max Kelly, \emph{Closed categories}, Proceedings of the
|
||||
Conference on Categorical Algebra, Springer, 1966, pp.~421--562.
|
||||
|
||||
\bibitem[EM45]{eilenberg1945spaces}
|
||||
Samuel Eilenberg and Saunders MacLane, \emph{Relations between homology and
|
||||
homotopy groups of spaces}, Annals of mathematics (1945), 480--509.
|
||||
|
||||
\bibitem[EUR{\etalchar{+}}17]{ebner2017metaprogramming}
|
||||
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo
|
||||
de~Moura, \emph{A metaprogramming framework for formal verification}, Proc.
|
||||
ACM Program. Lang. \textbf{1} (2017), no.~ICFP, 34:1--34:29, \href
|
||||
{http://dx.doi.org/10.1145/3110278} {\path{doi:10.1145/3110278}}.
|
||||
|
||||
\bibitem[G{\etalchar{+}}13]{gonthier2013oddorder}
|
||||
Georges Gonthier et~al., \emph{A machine-checked proof of the odd order
|
||||
theorem}, pp.~163--179, Springer, 2013, \href
|
||||
{http://dx.doi.org/10.1007/978-3-642-39634-2_14}
|
||||
{\path{doi:10.1007/978-3-642-39634-2_14}}.
|
||||
|
||||
\bibitem[Gir72]{girard1972paradox}
|
||||
Jean-Yves Girard, \emph{Interpr{\'e}tation fonctionelle et {\'e}limination des
|
||||
coupures de l’arithm{\'e}tique d’ordre sup{\'e}rieur}, Ph.D. thesis,
|
||||
Universit{\'e} Paris Diderot, 1972.
|
||||
|
||||
\bibitem[GMM06]{goguen2006eliminating}
|
||||
Healfdene Goguen, Conor McBride, and James McKinna, \emph{Eliminating dependent
|
||||
pattern matching}, Algebra, Meaning, and Computation (2006), 521--540.
|
||||
|
||||
\bibitem[Gon05]{gonthier2005fourcolour}
|
||||
Georges Gonthier, \emph{A computer-checked proof of the four colour theorem}.
|
||||
|
||||
\bibitem[Gra17]{graham2017homology}
|
||||
Robert Graham, \emph{{Synthetic Homology in Homotopy Type Theory}}, ArXiv
|
||||
e-print 1706.01540 (2017), \url{https://arxiv.org/abs/1706.01540}.
|
||||
|
||||
\bibitem[H{\etalchar{+}}]{hollight}
|
||||
John Harrison et~al., \emph{The hol light theorem prover},
|
||||
\url{https://github.com/jrh13/hol-light}.
|
||||
|
||||
\bibitem[H{\etalchar{+}}17]{hales2017kepler}
|
||||
Thomas Hales et~al., \emph{A formal proof of the {K}epler conjecture}, Forum of
|
||||
Mathematics, Pi \textbf{5} (2017), \href
|
||||
{http://dx.doi.org/10.1017/fmp.2017.1} {\path{doi:10.1017/fmp.2017.1}}.
|
||||
|
||||
\bibitem[Hat04]{hatcher2004spectral}
|
||||
Allen Hatcher, \emph{Spectral sequences in algebraic topology}, Unpublished
|
||||
book, 2004, \url{https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html}.
|
||||
|
||||
\bibitem[HFLL16]{favonia2016blakersmassey}
|
||||
Kuen-Bang {Hou (Favonia)}, Eric Finster, Daniel~R. Licata, and Peter~LeFanu
|
||||
Lumsdaine, \emph{A mechanization of the {Blakers-Massey} connectivity theorem
|
||||
in {Homotopy Type Theory}}, Proceedings of the 31st Annual ACM/IEEE Symposium
|
||||
on Logic in Computer Science, ACM, 2016, pp.~565--574.
|
||||
|
||||
\bibitem[{Hou}17]{favonia2017thesis}
|
||||
Kuen-Bang {Hou (Favonia)}, \emph{Higher-dimensional types in the mechanization
|
||||
of homotopy theory}, Ph.D. thesis, Carnegie Mellon University, 2017.
|
||||
|
||||
\bibitem[How80]{howard1980formulae}
|
||||
William~A. Howard, \emph{The formulae-as-types notion of construction}, To H.B.
|
||||
Curry: essays on combinatory logic, lambda calculus and formalism \textbf{44}
|
||||
(1980), 479--490.
|
||||
|
||||
\bibitem[HP13]{holmbergperoux2014models}
|
||||
Maximilien Holmberg-Péroux, \emph{The serre spectral sequence}, preprint
|
||||
(2013), \url{http://homepages.math.uic.edu/~mholmb2/serre.pdf}.
|
||||
|
||||
\bibitem[HS98]{hofmann1998groupoid}
|
||||
Martin Hofmann and Thomas Streicher, \emph{The groupoid interpretation of type
|
||||
theory}, Twenty-five years of constructive type theory ({V}enice, 1995),
|
||||
Oxford Logic Guides, vol.~36, Oxford Univ. Press, New York, 1998,
|
||||
pp.~83--111.
|
||||
|
||||
\bibitem[HS16]{favonia2016seifert}
|
||||
Kuen-Bang {Hou (Favonia)} and Michael Shulman, \emph{The {S}eifert-van {K}ampen
|
||||
theorem in homotopy type theory}, 25th EACSL Annual Conference on Computer
|
||||
Science Logic (CSL 2016), Leibniz International Proceedings in Informatics
|
||||
(LIPIcs), vol.~62, 2016, pp.~22:1--22:16, \href
|
||||
{http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22}
|
||||
{\path{doi:10.4230/LIPIcs.CSL.2016.22}}.
|
||||
|
||||
\bibitem[KECA14]{kraus2014anonymousexistence}
|
||||
Nicolai Kraus, Mart{\'\i}n Escard{\'o}, Thierry Coquand, and Thorsten
|
||||
Altenkirch, \emph{Notions of anonymous existence in {Martin-L{\"o}f} type
|
||||
theory}, Submitted to the special issue of TLCA'13 (2014).
|
||||
|
||||
\bibitem[KL12]{kapulkin2012simplicialnew}
|
||||
Chris Kapulkin and Peter~LeFanu Lumsdaine, \emph{{The Simplicial Model of
|
||||
Univalent Foundations (after Voevodsky)}}, ArXiv e-prints (2012), \href
|
||||
{http://arxiv.org/abs/1211.2851} {\path{arXiv:1211.2851}}.
|
||||
|
||||
\bibitem[Kra15]{kraus2014universalproperty}
|
||||
Nicolai Kraus, \emph{The general universal property of the propositional
|
||||
truncation}, 20th International Conference on Types for Proofs and Programs
|
||||
(TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs),
|
||||
vol.~39, 2015, pp.~111--145, \href
|
||||
{http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.111}
|
||||
{\path{doi:10.4230/LIPIcs.TYPES.2014.111}}.
|
||||
|
||||
\bibitem[Kra16]{kraus2016hits}
|
||||
\bysame, \emph{Constructions with non-recursive higher inductive types},
|
||||
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer
|
||||
Science, ACM, 2016, pp.~595--604.
|
||||
|
||||
\bibitem[LF14]{licata2014em}
|
||||
Daniel~R. Licata and Eric Finster, \emph{{E}ilenberg-{M}ac{L}ane spaces in
|
||||
homotopy type theory}, Proceedings of the Joint Meeting of the Twenty-Third
|
||||
EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth
|
||||
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), ACM, 2014,
|
||||
p.~66.
|
||||
|
||||
\bibitem[Lic11]{licata2011trick}
|
||||
Daniel~R. Licata, \emph{Running circles around (in) your proof assistant; or,
|
||||
quotients that compute}, blog post, April 2011,
|
||||
\url{http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/}.
|
||||
|
||||
\bibitem[LS13]{licatashulman2013}
|
||||
Daniel~R. Licata and Michael Shulman, \emph{Calculating the fundamental group
|
||||
of the circle in homotopy type theory}, 2013 28th {A}nnual {ACM}/{IEEE}
|
||||
{S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS} 2013), IEEE Computer
|
||||
Soc., Los Alamitos, CA, 2013, pp.~223--232.
|
||||
|
||||
\bibitem[LS17]{lumsdaine2017HITsemantics}
|
||||
Peter~LeFanu Lumsdaine and Michael Shulman, \emph{{Semantics of higher
|
||||
inductive types}}, ArXiv e-prints (2017), \href
|
||||
{http://arxiv.org/abs/1705.07088} {\path{arXiv:1705.07088}}.
|
||||
|
||||
\bibitem[Lum11]{lumsdaine2011hits}
|
||||
Peter~LeFanu Lumsdaine, \emph{Higher inductive types: a tour of the menagerie},
|
||||
blog post, April 2011,
|
||||
\url{https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/}.
|
||||
|
||||
\bibitem[Luo12]{luo2012universes}
|
||||
Zhaohui Luo, \emph{Notes on universes in type theory}, preprint, 2012,
|
||||
\url{http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf}.
|
||||
|
||||
\bibitem[Mas52]{massey1952exactcouple}
|
||||
William~S Massey, \emph{Exact couples in algebraic topology (parts i and ii)},
|
||||
Annals of Mathematics \textbf{56} (1952), no.~2, 363--396.
|
||||
|
||||
\bibitem[McL06]{mclaughlin2006interpretation}
|
||||
Sean McLaughlin, \emph{An interpretation of {Isabelle/HOL} in {HOL Light}},
|
||||
International Joint Conference on Automated Reasoning, Springer, 2006,
|
||||
pp.~192--204.
|
||||
|
||||
\bibitem[ML75]{martinlof1975typetheory}
|
||||
Per Martin-L{\"o}f, \emph{An intuitionistic theory of types: Predicative part},
|
||||
Studies in Logic and the Foundations of Mathematics, vol.~80, Elsevier, 1975,
|
||||
pp.~73--118.
|
||||
|
||||
\bibitem[ML84]{martinlof1984typetheory}
|
||||
\bysame, \emph{Intuitionistic type theory}, Bibliopolis, 1984, Notes by
|
||||
Giovanni Sambin of a series of lectures given in Padova.
|
||||
|
||||
\bibitem[Rez14]{rezk2014blakersmassey}
|
||||
Charles Rezk, \emph{Proof of the blakers-massey theorem}, 2014,
|
||||
\url{http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-massey.pdf}.
|
||||
|
||||
\bibitem[Rij17]{rijke2017join}
|
||||
Egbert Rijke, \emph{{The join construction}}, ArXiv (2017), \href
|
||||
{http://arxiv.org/abs/1701.07538} {\path{arXiv:1701.07538}}.
|
||||
|
||||
\bibitem[RSS17]{rijke2017modalities}
|
||||
Egbert Rijke, Michael Shulman, and Bas Spitters, \emph{Modalities in homotopy
|
||||
type theory}, ArXiv e-prints (2017), \href {http://arxiv.org/abs/1706.07526}
|
||||
{\path{arXiv:1706.07526}}.
|
||||
|
||||
\bibitem[S{\etalchar{+}}11]{shulman2011spectrification}
|
||||
Michael Shulman et~al., \emph{{higher inductive type}}, 2011, nLab article,
|
||||
\url{https://ncatlab.org/nlab/revision/higher+inductive+type/31}.
|
||||
|
||||
\bibitem[Ser51]{serre1951homology}
|
||||
Jean-Pierre Serre, \emph{Homologie singuli{\`e}re des espaces fibr{\'e}s},
|
||||
Annals of Mathematics (1951), 425--505.
|
||||
|
||||
\bibitem[Shu11a]{shulman2011pi1S1}
|
||||
Michael Shulman, \emph{A formal proof that $\pi_1(s^1)=\mathbb{Z}$}, blog post,
|
||||
April 2011,
|
||||
\url{https://homotopytypetheory.org/2011/04/29/a-formal-proof-that-pi1s1-is-z/}.
|
||||
|
||||
\bibitem[Shu11b]{shulman2011HoTThits}
|
||||
\bysame, \emph{Homotopy type theory, vi}, forum post, April 2011,
|
||||
\url{https://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html}.
|
||||
|
||||
\bibitem[Shu11c]{shulman2011intervalimpliesfunext}
|
||||
\bysame, \emph{An interval type implies function extensionality}, blog post,
|
||||
April 2011,
|
||||
\url{https://homotopytypetheory.org/2011/04/04/an-interval-type-implies-function-extensionality/}.
|
||||
|
||||
\bibitem[Shu13]{shulman2013spectral}
|
||||
\bysame, \emph{{Spectral sequences in HoTT}}, blog posts, August 2013,
|
||||
\url{https://ncatlab.org/homotopytypetheory/revision/spectral+sequences/5}.
|
||||
|
||||
\bibitem[Shu17]{shulman2017topos}
|
||||
\bysame, \emph{Elementary $(\infty,1)$-topoi}, blog post, April 2017,
|
||||
\url{https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html}.
|
||||
|
||||
\bibitem[Sna81]{snaith1981ktheory}
|
||||
Victor Snaith, \emph{Localized stable homotopy of some classifying spaces},
|
||||
Mathematical Proceedings of the Cambridge Philosophical Society, vol.~89,
|
||||
Cambridge University Press, 1981, pp.~325--330.
|
||||
|
||||
\bibitem[Str14]{streicher2014simplicial}
|
||||
Thomas Streicher, \emph{A model of type theory in simplicial sets: A brief
|
||||
introduction to {V}oevodsky's homotopy type theory}, Journal of Applied Logic
|
||||
\textbf{12} (2014), no.~1, 45 -- 49, Logic Categories Semantics, \href
|
||||
{http://dx.doi.org/https://doi.org/10.1016/j.jal.2013.04.001}
|
||||
{\path{doi:https://doi.org/10.1016/j.jal.2013.04.001}}.
|
||||
|
||||
\bibitem[{The}18]{redprl}
|
||||
{The RedPRL Development Team}, \emph{{RedPRL} -- the {P}eople's {R}efinement
|
||||
{L}ogic}, 2018, \url{http://www.redprl.org/}.
|
||||
|
||||
\bibitem[{Uni}13]{hottbook}
|
||||
The {Univalent Foundations Program}, \emph{Homotopy type theory: Univalent
|
||||
foundations of mathematics}, \url{http://homotopytypetheory.org/book},
|
||||
Institute for Advanced Study, 2013.
|
||||
|
||||
\bibitem[VAG{\etalchar{+}}]{unimath}
|
||||
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et~al., \emph{{U}ni{M}ath
|
||||
--- {U}nivalent {M}athematics}, code library,
|
||||
\url{https://github.com/UniMath}.
|
||||
|
||||
\bibitem[vD16]{vandoorn2016proptrunc}
|
||||
Floris van Doorn, \emph{Constructing the propositional truncation using
|
||||
non-recursive hits}, Proceedings of the 5th ACM SIGPLAN Conference on
|
||||
Certified Programs and Proofs, ACM, 2016, pp.~122--129.
|
||||
|
||||
\bibitem[vDvRB17]{vandoorn2017leanhott}
|
||||
Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz, \emph{Homotopy type
|
||||
theory in lean}, pp.~479--495, Springer, 2017, \href
|
||||
{http://dx.doi.org/10.1007/978-3-319-66107-0_30}
|
||||
{\path{doi:10.1007/978-3-319-66107-0_30}}.
|
||||
|
||||
\bibitem[vG12]{berg2010models}
|
||||
Benno {van den Berg} and Richard Garner, \emph{{Topological and simplicial
|
||||
models of identity types}}, ACM transactions on computational logic (TOCL)
|
||||
\textbf{13} (2012), no.~1, 3.
|
||||
|
||||
\bibitem[Voe06]{voevodsky2006}
|
||||
Vladimir Voevodsky, \emph{A very short note on the homotopy
|
||||
{$\lambda$}-calculus}, online, 2006,
|
||||
\url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf}.
|
||||
|
||||
\bibitem[Voe09]{voevodsky2009typesystems}
|
||||
\bysame, \emph{Notes on type systems}, online, 2009,
|
||||
\url{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current_1.pdf}.
|
||||
|
||||
\bibitem[Voe14]{voevodsky2014univalence}
|
||||
\bysame, \emph{{The equivalence axiom and univalent models of type theory.
|
||||
(Talk at CMU on February 4, 2010)}}, \href {http://arxiv.org/abs/1402.5556}
|
||||
{\path{arXiv:1402.5556}}.
|
||||
|
||||
\bibitem[Voe15]{voevodsky2015lecture}
|
||||
\bysame, \emph{Oxford lectures on {U}ni{M}ath}, filmed by Kohei Kishida,
|
||||
available at \url{https://www.math.ias.edu/vladimir/Lectures}, 2015.
|
||||
|
||||
\bibitem[vR16]{raumer2016doublegroupoids}
|
||||
Jakob von Raumer, \emph{Formalizing double groupoids and cross modules in the
|
||||
lean theorem prover}, Mathematical Software -- ICMS 2016, Springer
|
||||
International Publishing, 2016, pp.~28--33.
|
||||
|
||||
\bibitem[Zha17]{zhan2017auto2}
|
||||
Bohua Zhan, \emph{Formalization of the fundamental group in untyped set theory
|
||||
using auto2}, International Conference on Interactive Theorem Proving,
|
||||
Springer, Springer, 2017, pp.~514--530, \href
|
||||
{http://dx.doi.org/10.1007/978-3-319-66107-0_32}
|
||||
{\path{doi:10.1007/978-3-319-66107-0_32}}.
|
||||
|
||||
\end{thebibliography}
|
||||
BIN
resources/VanDoornDissertation/dissertation.pdf
vendored
Normal file
BIN
resources/VanDoornDissertation/dissertation.pdf
vendored
Normal file
Binary file not shown.
6617
resources/VanDoornDissertation/dissertation.tex
vendored
Normal file
6617
resources/VanDoornDissertation/dissertation.tex
vendored
Normal file
File diff suppressed because it is too large
Load diff
293
resources/VanDoornDissertation/lstlean.tex
vendored
Normal file
293
resources/VanDoornDissertation/lstlean.tex
vendored
Normal file
|
|
@ -0,0 +1,293 @@
|
|||
% Listing style definition for the Lean Theorem Prover.
|
||||
% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
|
||||
% Unicode replacements taken from Olivier Verdier's unixode.sty
|
||||
|
||||
\lstdefinelanguage{lean} {
|
||||
|
||||
% Anything betweeen $ becomes LaTeX math mode
|
||||
mathescape=true,
|
||||
% Comments may or not include Latex commands
|
||||
texcl=false,
|
||||
|
||||
% keywords, list taken from lean-syntax.el
|
||||
morekeywords=[1]{
|
||||
import, prelude, tactic_hint, protected, private, noncomputable, definition, renaming,
|
||||
hiding, exposing, parameter, parameters, begin, begin+, proof, qed, conjecture, constant, constants,
|
||||
hypothesis, lemma, corollary, variable, variables, premise, premises, theory,
|
||||
print, theorem, proposition, example, abbreviation, abstract,
|
||||
open, as, export, override, axiom, axioms, inductive, with, structure, record, universe, universes,
|
||||
alias, help, environment, options, precedence, reserve,
|
||||
match, infix, infixl, infixr, notation, postfix, prefix,
|
||||
tactic_infix, tactic_infixl, tactic_infixr, tactic_notation, tactic_postfix, tactic_prefix,
|
||||
eval, check, coercion, end, reveal, this, suppose,
|
||||
using, namespace, section, fields, find_decl,
|
||||
attribute, local, set_option, extends, include, omit, classes,
|
||||
instances, coercions, metaclasses, raw, migrate, replacing,
|
||||
calc, have, obtains, show, suffices, by, by+, in, at, let, forall, Pi, fun,
|
||||
exists, if, dif, then, else, assume, assert, take,
|
||||
obtain, from, aliases
|
||||
},
|
||||
|
||||
% Sorts
|
||||
morekeywords=[2]{Type, Prop},
|
||||
|
||||
% tactics, list taken from lean-syntax.el
|
||||
morekeywords=[3]{
|
||||
Cond, or_else, then, try, when, assumption, eassumption, rapply,
|
||||
apply, fapply, eapply, rename, intro, intros, all_goals, fold, focus, focus_at,
|
||||
generalize, generalizes, clear, clears, revert, reverts, back, beta, done, exact, rexact,
|
||||
refine, repeat, whnf, rotate, rotate_left, rotate_right, inversion, cases, rewrite,
|
||||
xrewrite, krewrite, blast, simp, esimp, unfold, change, check_expr, contradiction,
|
||||
exfalso, split, existsi, constructor, fconstructor, left, right, injection, congruence, reflexivity,
|
||||
symmetry, transitivity, state, induction, induction_using, fail, append,
|
||||
substvars, now, with_options, with_attributes, with_attrs, note
|
||||
},
|
||||
|
||||
% modifiers, taken from lean-syntax.el
|
||||
% note: 'otherkeywords' is needed because these use a different symbol.
|
||||
% this command doesn't allow us to specify a number -- they are put with [1]
|
||||
otherkeywords={
|
||||
[persistent], [notation], [visible], [instance], [trans_instance],
|
||||
[class], [parsing-only], [coercion], [unfold_full], [constructor],
|
||||
[reducible], [irreducible], [semireducible], [quasireducible], [wf],
|
||||
[whnf], [multiple_instances], [none], [decl], [declaration],
|
||||
[relation], [symm], [subst], [refl], [trans], [simp], [congr],
|
||||
[backward], [forward], [no_pattern], [begin_end], [tactic], [abbreviation],
|
||||
[reducible], [unfold], [alias], [eqv], [intro], [intro!], [elim], [grinder],
|
||||
[localrefinfo], [recursor]
|
||||
},
|
||||
|
||||
% Various symbols
|
||||
literate=
|
||||
{α}{{\ensuremath{\mathrm{\alpha}}}}1
|
||||
{β}{{\ensuremath{\mathrm{\beta}}}}1
|
||||
{γ}{{\ensuremath{\mathrm{\gamma}}}}1
|
||||
{δ}{{\ensuremath{\mathrm{\delta}}}}1
|
||||
{ε}{{\ensuremath{\mathrm{\varepsilon}}}}1
|
||||
{ζ}{{\ensuremath{\mathrm{\zeta}}}}1
|
||||
{η}{{\ensuremath{\mathrm{\eta}}}}1
|
||||
{θ}{{\ensuremath{\mathrm{\theta}}}}1
|
||||
{ι}{{\ensuremath{\mathrm{\iota}}}}1
|
||||
{κ}{{\ensuremath{\mathrm{\kappa}}}}1
|
||||
{μ}{{\ensuremath{\mathrm{\mu}}}}1
|
||||
{ν}{{\ensuremath{\mathrm{\nu}}}}1
|
||||
{ξ}{{\ensuremath{\mathrm{\xi}}}}1
|
||||
{π}{{\ensuremath{\mathrm{\mathnormal{\pi}}}}}1
|
||||
{ρ}{{\ensuremath{\mathrm{\rho}}}}1
|
||||
{σ}{{\ensuremath{\mathrm{\sigma}}}}1
|
||||
{τ}{{\ensuremath{\mathrm{\tau}}}}1
|
||||
{φ}{{\ensuremath{\mathrm{\varphi}}}}1
|
||||
{χ}{{\ensuremath{\mathrm{\chi}}}}1
|
||||
{ψ}{{\ensuremath{\mathrm{\psi}}}}1
|
||||
{ω}{{\ensuremath{\mathrm{\omega}}}}1
|
||||
|
||||
{Γ}{{\ensuremath{\mathrm{\Gamma}}}}1
|
||||
{Δ}{{\ensuremath{\mathrm{\Delta}}}}1
|
||||
{Θ}{{\ensuremath{\mathrm{\Theta}}}}1
|
||||
{Λ}{{\ensuremath{\mathrm{\Lambda}}}}1
|
||||
{Σ}{{\ensuremath{\mathrm{\Sigma}}}}1
|
||||
{Φ}{{\ensuremath{\mathrm{\Phi}}}}1
|
||||
{Ξ}{{\ensuremath{\mathrm{\Xi}}}}1
|
||||
{Ψ}{{\ensuremath{\mathrm{\Psi}}}}1
|
||||
{Ω}{{\ensuremath{\mathrm{\Omega}}}}1
|
||||
|
||||
{ℵ}{{\ensuremath{\aleph}}}1
|
||||
|
||||
{≤}{{\ensuremath{\leq}}}1
|
||||
{≥}{{\ensuremath{\geq}}}1
|
||||
{≠}{{\ensuremath{\neq}}}1
|
||||
{≈}{{\ensuremath{\approx}}}1
|
||||
{≡}{{\ensuremath{\equiv}}}1
|
||||
{≃}{{\ensuremath{\simeq}}}1
|
||||
|
||||
{≤}{{\ensuremath{\leq}}}1
|
||||
{≥}{{\ensuremath{\geq}}}1
|
||||
|
||||
{∂}{{\ensuremath{\partial}}}1
|
||||
{∆}{{\ensuremath{\triangle}}}1 % or \laplace?
|
||||
|
||||
{∫}{{\ensuremath{\int}}}1
|
||||
{∑}{{\ensuremath{\mathrm{\Sigma}}}}1
|
||||
{Π}{{\ensuremath{\mathrm{\Pi}}}}1
|
||||
|
||||
{⊥}{{\ensuremath{\perp}}}1
|
||||
{∞}{{\ensuremath{\infty}}}1
|
||||
{∂}{{\ensuremath{\partial}}}1
|
||||
|
||||
{∓}{{\ensuremath{\mp}}}1
|
||||
{±}{{\ensuremath{\pm}}}1
|
||||
{×}{{\ensuremath{\times}}}1
|
||||
|
||||
{⊕}{{\ensuremath{\oplus}}}1
|
||||
{⊗}{{\ensuremath{\otimes}}}1
|
||||
{⊞}{{\ensuremath{\boxplus}}}1
|
||||
|
||||
{∇}{{\ensuremath{\nabla}}}1
|
||||
{√}{{\ensuremath{\sqrt}}}1
|
||||
|
||||
{⬝}{{\ensuremath{\cdot}}}1
|
||||
{•}{{\ensuremath{\cdot}}}1
|
||||
{∘}{{\ensuremath{\circ}}}1
|
||||
{`}{{\ensuremath{{}^\backprime}}}1
|
||||
{'}{{\ensuremath{{}^\prime}}}1
|
||||
|
||||
%{⁻}{{\ensuremath{^{\textup{\kern1pt\rule{2pt}{0.3pt}\kern-1pt}}}}}1
|
||||
{⁻}{{\ensuremath{^{-}}}}1
|
||||
{▸}{{\ensuremath{\mathsmaller\blacktriangleright}}}1 %% requires package relsize
|
||||
|
||||
{∧}{{\ensuremath{\wedge}}}1
|
||||
{∨}{{\ensuremath{\vee}}}1
|
||||
{¬}{{\ensuremath{\neg}}}1
|
||||
{⊢}{{\ensuremath{\vdash}}}1
|
||||
|
||||
%{⟨}{{\ensuremath{\left\langle}}}1
|
||||
%{⟩}{{\ensuremath{\right\rangle}}}1
|
||||
{⟨}{{\ensuremath{\langle}}}1
|
||||
{⟩}{{\ensuremath{\rangle}}}1
|
||||
|
||||
{↦}{{\ensuremath{\mapsto}}}1
|
||||
{→}{{\ensuremath{\rightarrow}}}1
|
||||
{↔}{{\ensuremath{\leftrightarrow}}}1
|
||||
{⇒}{{\ensuremath{\Rightarrow}}}1
|
||||
{⟹}{{\ensuremath{\Longrightarrow}}}1
|
||||
{⇐}{{\ensuremath{\Leftarrow}}}1
|
||||
{⟸}{{\ensuremath{\Longleftarrow}}}1
|
||||
|
||||
{∩}{{\ensuremath{\cap}}}1
|
||||
{∪}{{\ensuremath{\cup}}}1
|
||||
{⊂}{{\ensuremath{\subseteq}}}1
|
||||
{⊆}{{\ensuremath{\subseteq}}}1
|
||||
{⊄}{{\ensuremath{\nsubseteq}}}1
|
||||
{⊈}{{\ensuremath{\nsubseteq}}}1
|
||||
{⊃}{{\ensuremath{\supseteq}}}1
|
||||
{⊇}{{\ensuremath{\supseteq}}}1
|
||||
{⊅}{{\ensuremath{\nsupseteq}}}1
|
||||
{⊉}{{\ensuremath{\nsupseteq}}}1
|
||||
{∈}{{\ensuremath{\in}}}1
|
||||
{∉}{{\ensuremath{\notin}}}1
|
||||
{∋}{{\ensuremath{\ni}}}1
|
||||
{∌}{{\ensuremath{\notni}}}1
|
||||
{∅}{{\ensuremath{\emptyset}}}1
|
||||
|
||||
{∖}{{\ensuremath{\setminus}}}1
|
||||
{†}{{\ensuremath{\dag}}}1
|
||||
|
||||
{ℕ}{{\ensuremath{\mathbb{N}}}}1
|
||||
{ℤ}{{\ensuremath{\mathbb{Z}}}}1
|
||||
{ℝ}{{\ensuremath{\mathbb{R}}}}1
|
||||
{ℚ}{{\ensuremath{\mathbb{Q}}}}1
|
||||
{ℂ}{{\ensuremath{\mathbb{C}}}}1
|
||||
{⌞}{{\ensuremath{\llcorner}}}1
|
||||
{⌟}{{\ensuremath{\lrcorner}}}1
|
||||
{⦃}{{\ensuremath{\{\!|}}}1
|
||||
{⦄}{{\ensuremath{|\!\}}}}1
|
||||
|
||||
{₁}{{\ensuremath{_1}}}1
|
||||
{₂}{{\ensuremath{_2}}}1
|
||||
{₃}{{\ensuremath{_3}}}1
|
||||
{₄}{{\ensuremath{_4}}}1
|
||||
{₅}{{\ensuremath{_5}}}1
|
||||
{₆}{{\ensuremath{_6}}}1
|
||||
{₇}{{\ensuremath{_7}}}1
|
||||
{₈}{{\ensuremath{_8}}}1
|
||||
{₉}{{\ensuremath{_9}}}1
|
||||
{₀}{{\ensuremath{_0}}}1
|
||||
|
||||
{¹}{{\ensuremath{^1}}}1
|
||||
{²}{{\ensuremath{^2}}}1
|
||||
{³}{{\ensuremath{^3}}}1
|
||||
{⁴}{{\ensuremath{^4}}}1
|
||||
{⁵}{{\ensuremath{^5}}}1
|
||||
{⁶}{{\ensuremath{^6}}}1
|
||||
{⁷}{{\ensuremath{^7}}}1
|
||||
{⁸}{{\ensuremath{^8}}}1
|
||||
{⁹}{{\ensuremath{^9}}}1
|
||||
{⁰}{{\ensuremath{^0}}}1
|
||||
|
||||
|
||||
{ᵒ}{{\textsuperscript{o}}}1
|
||||
{ᵖ}{{\textsuperscript{p}}}1
|
||||
|
||||
|
||||
{ₙ}{{\ensuremath{_n}}}1
|
||||
{ₘ}{{\ensuremath{_m}}}1
|
||||
{↑}{{\ensuremath{\uparrow}}}1
|
||||
{↓}{{\ensuremath{\downarrow}}}1
|
||||
|
||||
% {▸}{{\ensuremath{\triangleright}}}1
|
||||
|
||||
{Σ}{{\color{symbolcolor}\ensuremath{\mathrm{\Sigma}}}}1
|
||||
{Π}{{\color{symbolcolor}\ensuremath{\mathrm{\Pi}}}}1
|
||||
{∀}{{\color{symbolcolor}\ensuremath{\forall}}}1
|
||||
{∃}{{\color{symbolcolor}\ensuremath{\exists}}}1
|
||||
{λ}{{\color{symbolcolor}\ensuremath{\mathrm{\lambda}}}}1
|
||||
{Ω}{{\color{symbolcolor}\ensuremath{\mathrm{\Omega}}}}1
|
||||
|
||||
{:=}{{\color{symbolcolor}:=}}1
|
||||
{=}{{\color{symbolcolor}=}}1
|
||||
{<}{{\color{symbolcolor}<}}1
|
||||
{+}{{\color{symbolcolor}+}}1
|
||||
{*}{{\color{symbolcolor}\ensuremath{{}^{*}}}}1,
|
||||
|
||||
% Comments
|
||||
%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
|
||||
morecomment=[s][\color{commentcolor}]{/-}{-/},
|
||||
morecomment=[l][\itshape \color{commentcolor}]{--},
|
||||
|
||||
% Spaces are not displayed as a special character
|
||||
showstringspaces=false,
|
||||
|
||||
% keep spaces
|
||||
keepspaces=true,
|
||||
|
||||
% String delimiters
|
||||
morestring=[b]",
|
||||
morestring=[d],
|
||||
|
||||
% Size of tabulations
|
||||
tabsize=3,
|
||||
|
||||
% Enables ASCII chars 128 to 255
|
||||
extendedchars=false,
|
||||
|
||||
% Case sensitivity
|
||||
sensitive=true,
|
||||
|
||||
% Automatic breaking of long lines
|
||||
breaklines=true,
|
||||
|
||||
% Default style fors listingsred
|
||||
basicstyle=\ttfamily,
|
||||
|
||||
% Position of captions is bottom
|
||||
captionpos=b,
|
||||
|
||||
% Full flexible columns
|
||||
columns=[l]fullflexible,
|
||||
|
||||
|
||||
% Style for (listings') identifiers
|
||||
identifierstyle={\ttfamily\color{black}},
|
||||
% Note : highlighting of Coq identifiers is done through a new
|
||||
% delimiter definition through an lstset at the begining of the
|
||||
% document. Don't know how to do better.
|
||||
|
||||
% Style for declaration keywords
|
||||
keywordstyle=[1]{\ttfamily\color{keywordcolor}},
|
||||
|
||||
% Style for sorts
|
||||
keywordstyle=[2]{\ttfamily\color{sortcolor}},
|
||||
|
||||
% Style for tactics keywords
|
||||
keywordstyle=[3]{\ttfamily\color{tacticcolor}},
|
||||
|
||||
% Style for attributes
|
||||
keywordstyle=[4]{\ttfamily\color{attributecolor}},
|
||||
|
||||
% Style for strings
|
||||
stringstyle=\ttfamily,
|
||||
|
||||
% Style for comments
|
||||
% commentstyle={\ttfamily\footnotesize },
|
||||
|
||||
}
|
||||
783
resources/VanDoornDissertation/macros.tex
vendored
Normal file
783
resources/VanDoornDissertation/macros.tex
vendored
Normal file
|
|
@ -0,0 +1,783 @@
|
|||
%%%% MACROS FOR NOTATION %%%%
|
||||
% Use these for any notation where there are multiple options.
|
||||
% Slightly modified by Floris van Doorn
|
||||
|
||||
%%% Notes and exercise sections
|
||||
\makeatletter
|
||||
\newcommand{\sectionNotes}{\phantomsection\section*{Notes}\addcontentsline{toc}{section}{Notes}\markright{\textsc{\@chapapp{} \thechapter{} Notes}}}
|
||||
\newcommand{\sectionExercises}[1]{\phantomsection\section*{Exercises}\addcontentsline{toc}{section}{Exercises}\markright{\textsc{\@chapapp{} \thechapter{} Exercises}}}
|
||||
\makeatother
|
||||
|
||||
%%% Definitional equality (used infix) %%%
|
||||
\newcommand{\jdeq}{\equiv} % An equality judgment
|
||||
\let\judgeq\jdeq
|
||||
%\newcommand{\defeq}{\coloneqq} % An equality currently being defined
|
||||
\newcommand{\defeq}{\vcentcolon\equiv} % A judgmental equality currently being defined
|
||||
|
||||
%%% Term being defined
|
||||
\newcommand{\define}[1]{\textbf{#1}}
|
||||
|
||||
%%% Vec (for example)
|
||||
|
||||
\newcommand{\Vect}{\ensuremath{\mathsf{Vec}}}
|
||||
\newcommand{\Fin}{\ensuremath{\mathsf{Fin}}}
|
||||
\newcommand{\fmax}{\ensuremath{\mathsf{fmax}}}
|
||||
\newcommand{\seq}[1]{\langle #1\rangle}
|
||||
|
||||
%%% Dependent products %%%
|
||||
\def\prdsym{\textstyle\prod}
|
||||
%% Call the macro like \prd{x,y:A}{p:x=y} with any number of
|
||||
%% arguments. Make sure that whatever comes *after* the call doesn't
|
||||
%% begin with an open-brace, or it will be parsed as another argument.
|
||||
\makeatletter
|
||||
% Currently the macro is configured to produce
|
||||
% {\textstyle\prod}(x:A) \; {\textstyle\prod}(y:B),\
|
||||
% in display-math mode, and
|
||||
% \prod_{(x:A)} \prod_{y:B}
|
||||
% in text-math mode.
|
||||
\def\prd#1{\@ifnextchar\bgroup{\prd@parens{#1}}{\@ifnextchar\sm{\prd@parens{#1}\@eatsm}{\prd@noparens{#1}}}}
|
||||
\def\prd@parens#1{\@ifnextchar\bgroup%
|
||||
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\prd@parens}%
|
||||
{\@ifnextchar\sm%
|
||||
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\@eatsm}%
|
||||
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}}}
|
||||
\def\@eatsm\sm{\sm@parens}
|
||||
\def\prd@noparens#1{\mathchoice{\@dprd@noparens{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}
|
||||
% Helper macros for three styles
|
||||
\def\lprd#1{\@ifnextchar\bgroup{\@lprd{#1}\lprd}{\@@lprd{#1}}}
|
||||
\def\@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1})\;}
|
||||
\def\@@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1}),\ }
|
||||
\def\tprd#1{\@tprd{#1}\@ifnextchar\bgroup{\tprd}{}}
|
||||
\def\@tprd#1{\mathchoice{{\textstyle\prod_{(#1)}}}{\prod_{(#1)}}{\prod_{(#1)}}{\prod_{(#1)}}}
|
||||
\def\dprd#1{\@dprd{#1}\@ifnextchar\bgroup{\dprd}{}}
|
||||
\def\@dprd#1{\prod_{(#1)}\,}
|
||||
\def\@dprd@noparens#1{\prod_{#1}\,}
|
||||
|
||||
%%% Lambda abstractions.
|
||||
% Each variable being abstracted over is a separate argument. If
|
||||
% there is more than one such argument, they *must* be enclosed in
|
||||
% braces. Arguments can be untyped, as in \lam{x}{y}, or typed with a
|
||||
% colon, as in \lam{x:A}{y:B}. In the latter case, the colons are
|
||||
% automatically noticed and (with current implementation) the space
|
||||
% around the colon is reduced. You can even give more than one variable
|
||||
% the same type, as in \lam{x,y:A}.
|
||||
\def\lam#1{{\lambda}\@lamarg#1:\@endlamarg\@ifnextchar\bgroup{.\,\lam}{.\,}}
|
||||
\def\@lamarg#1:#2\@endlamarg{\if\relax\detokenize{#2}\relax #1\else\@lamvar{\@lameatcolon#2},#1\@endlamvar\fi}
|
||||
\def\@lamvar#1,#2\@endlamvar{(#2\,{:}\,#1)}
|
||||
% \def\@lamvar#1,#2{{#2}^{#1}\@ifnextchar,{.\,{\lambda}\@lamvar{#1}}{\let\@endlamvar\relax}}
|
||||
\def\@lameatcolon#1:{#1}
|
||||
\let\lamt\lam
|
||||
% This version silently eats any typing annotation.
|
||||
\def\lamu#1{{\lambda}\@lamuarg#1:\@endlamuarg\@ifnextchar\bgroup{.\,\lamu}{.\,}}
|
||||
\def\@lamuarg#1:#2\@endlamuarg{#1}
|
||||
|
||||
%%% Dependent products written with \forall, in the same style
|
||||
\def\fall#1{\forall (#1)\@ifnextchar\bgroup{.\,\fall}{.\,}}
|
||||
|
||||
%%% Existential quantifier %%%
|
||||
\def\exis#1{\exists (#1)\@ifnextchar\bgroup{.\,\exis}{.\,}}
|
||||
|
||||
%%% Dependent sums %%%
|
||||
\def\smsym{\textstyle\sum}
|
||||
% Use in the same way as \prd
|
||||
\def\sm#1{\@ifnextchar\bgroup{\sm@parens{#1}}{\@ifnextchar\prd{\sm@parens{#1}\@eatprd}{\sm@noparens{#1}}}}
|
||||
\def\sm@parens#1{\@ifnextchar\bgroup%
|
||||
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\sm@parens}%
|
||||
{\@ifnextchar\prd%
|
||||
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\@eatprd}%
|
||||
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}}}}
|
||||
\def\@eatprd\prd{\prd@parens}
|
||||
\def\sm@noparens#1{\mathchoice{\@dsm@noparens{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}}
|
||||
\def\lsm#1{\@ifnextchar\bgroup{\@lsm{#1}\lsm}{\@@lsm{#1}}}
|
||||
\def\@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1})\;}
|
||||
\def\@@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1}),\ }
|
||||
\def\tsm#1{\@tsm{#1}\@ifnextchar\bgroup{\tsm}{}}
|
||||
\def\@tsm#1{\mathchoice{{\textstyle\sum_{(#1)}}}{\sum_{(#1)}}{\sum_{(#1)}}{\sum_{(#1)}}}
|
||||
\def\dsm#1{\@dsm{#1}\@ifnextchar\bgroup{\dsm}{}}
|
||||
\def\@dsm#1{\sum_{(#1)}\,}
|
||||
\def\@dsm@noparens#1{\sum_{#1}\,}
|
||||
|
||||
%%% W-types
|
||||
\def\wtypesym{{\mathsf{W}}}
|
||||
\def\wtype#1{\@ifnextchar\bgroup%
|
||||
{\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}\wtype}%
|
||||
{\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}}}
|
||||
\def\lwtype#1{\@ifnextchar\bgroup{\@lwtype{#1}\lwtype}{\@@lwtype{#1}}}
|
||||
\def\@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1})\;}
|
||||
\def\@@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1}),\ }
|
||||
\def\twtype#1{\@twtype{#1}\@ifnextchar\bgroup{\twtype}{}}
|
||||
\def\@twtype#1{\mathchoice{{\textstyle\mathsf{W}_{(#1)}}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}}
|
||||
\def\dwtype#1{\@dwtype{#1}\@ifnextchar\bgroup{\dwtype}{}}
|
||||
\def\@dwtype#1{\mathsf{W}_{(#1)}\,}
|
||||
|
||||
\newcommand{\suppsym}{{\mathsf{sup}}}
|
||||
\newcommand{\supp}{\ensuremath\suppsym\xspace}
|
||||
|
||||
\def\wtypeh#1{\@ifnextchar\bgroup%
|
||||
{\mathchoice{\@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}\wtypeh}%
|
||||
{\mathchoice{\@@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}}}
|
||||
\def\lwtypeh#1{\@ifnextchar\bgroup{\@lwtypeh{#1}\lwtypeh}{\@@lwtypeh{#1}}}
|
||||
\def\@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1})\;}
|
||||
\def\@@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1}),\ }
|
||||
\def\twtypeh#1{\@twtypeh{#1}\@ifnextchar\bgroup{\twtypeh}{}}
|
||||
\def\@twtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h_{(#1)}}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}}
|
||||
\def\dwtypeh#1{\@dwtypeh{#1}\@ifnextchar\bgroup{\dwtypeh}{}}
|
||||
\def\@dwtypeh#1{\mathsf{W}^h_{(#1)}\,}
|
||||
|
||||
|
||||
\makeatother
|
||||
|
||||
% Other notations related to dependent sums
|
||||
\let\setof\Set % from package 'braket', write \setof{ x:A | P(x) }.
|
||||
% \newcommand{\pair}{\ensuremath{\mathsf{pair}}\xspace}
|
||||
\newcommand{\tup}[2]{(#1,#2)}
|
||||
\newcommand{\proj}[1]{\ensuremath{\mathsf{pr}_{#1}}\xspace}
|
||||
\newcommand{\fst}{\ensuremath{\proj1}\xspace}
|
||||
\newcommand{\snd}{\ensuremath{\proj2}\xspace}
|
||||
\newcommand{\ac}{\ensuremath{\mathsf{ac}}\xspace} % not needed in symbol index
|
||||
\newcommand{\un}{\ensuremath{\mathsf{upun}}\xspace} % not needed in symbol index, uniqueness principle for unit type
|
||||
|
||||
%%% recursor and induction
|
||||
\newcommand{\rec}[1]{\mathsf{rec}_{#1}}
|
||||
\newcommand{\ind}[1]{\mathsf{ind}_{#1}}
|
||||
\newcommand{\indid}[1]{\ind{=_{#1}}} % (Martin-Lof) path induction principle for identity types
|
||||
\newcommand{\indidb}[1]{\ind{=_{#1}}'} % (Paulin-Mohring) based path induction principle for identity types
|
||||
|
||||
%%% the uniqueness principle for product types, formerly called surjective pairing and named \spr:
|
||||
\newcommand{\uppt}{\ensuremath{\mathsf{uppt}}\xspace}
|
||||
|
||||
% Paths in pairs
|
||||
\newcommand{\pairpath}{\ensuremath{\mathsf{pair}^{\mathord{=}}}\xspace}
|
||||
% \newcommand{\projpath}[1]{\proj{#1}^{\mathord{=}}}
|
||||
\newcommand{\projpath}[1]{\ensuremath{\apfunc{\proj{#1}}}\xspace}
|
||||
|
||||
%%% For quotients %%%
|
||||
%\newcommand{\pairr}[1]{{\langle #1\rangle}}
|
||||
\newcommand{\pairr}[1]{{\mathopen{}(#1)\mathclose{}}}
|
||||
\newcommand{\Pairr}[1]{{\mathopen{}\left(#1\right)\mathclose{}}}
|
||||
|
||||
% \newcommand{\type}{\ensuremath{\mathsf{Type}}} % this command is overridden below, so it's commented out
|
||||
\newcommand{\im}{\ensuremath{\mathsf{im}}} % the image
|
||||
|
||||
%%% 2D path operations
|
||||
\newcommand{\leftwhisker}{\mathbin{{\ct}_{\ell}}}
|
||||
\newcommand{\rightwhisker}{\mathbin{{\ct}_{r}}}
|
||||
\newcommand{\hct}{\star}
|
||||
|
||||
%%% modalities %%%
|
||||
\newcommand{\modal}{\ensuremath{\ocircle}}
|
||||
\let\reflect\modal
|
||||
\newcommand{\modaltype}{\ensuremath{\type_\modal}}
|
||||
% \newcommand{\ism}[1]{\ensuremath{\mathsf{is}_{#1}}}
|
||||
% \newcommand{\ismodal}{\ism{\modal}}
|
||||
% \newcommand{\existsmodal}{\ensuremath{{\exists}_{\modal}}}
|
||||
% \newcommand{\existsmodalunique}{\ensuremath{{\exists!}_{\modal}}}
|
||||
% \newcommand{\modalfunc}{\textsf{\modal-fun}}
|
||||
% \newcommand{\Ecirc}{\ensuremath{\mathsf{E}_\modal}}
|
||||
% \newcommand{\Mcirc}{\ensuremath{\mathsf{M}_\modal}}
|
||||
\newcommand{\mreturn}{\ensuremath{\eta}}
|
||||
\let\project\mreturn
|
||||
%\newcommand{\mbind}[1]{\ensuremath{\hat{#1}}}
|
||||
\newcommand{\ext}{\mathsf{ext}}
|
||||
%\newcommand{\mmap}[1]{\ensuremath{\bar{#1}}}
|
||||
%\newcommand{\mjoin}{\ensuremath{\mreturn^{-1}}}
|
||||
% Subuniverse
|
||||
\renewcommand{\P}{\ensuremath{\type_{P}}\xspace}
|
||||
|
||||
%%% Localizations
|
||||
% \newcommand{\islocal}[1]{\ensuremath{\mathsf{islocal}_{#1}}\xspace}
|
||||
% \newcommand{\loc}[1]{\ensuremath{\mathcal{L}_{#1}}\xspace}
|
||||
|
||||
%%% Identity types %%%
|
||||
\newcommand{\idsym}{{=}}
|
||||
% \newcommand{\id}[3][]{\ensuremath{#2 =_{#1} #3}\xspace}
|
||||
\newcommand{\idtype}[3][]{\ensuremath{\mathsf{Id}_{#1}(#2,#3)}\xspace}
|
||||
\newcommand{\idtypevar}[1]{\ensuremath{\mathsf{Id}_{#1}}\xspace}
|
||||
% A propositional equality currently being defined
|
||||
\newcommand{\defid}{\coloneqq}
|
||||
|
||||
%%% Dependent paths
|
||||
\newcommand{\dpath}[4]{#3 =^{#1}_{#2} #4}
|
||||
|
||||
%%% singleton
|
||||
% \newcommand{\sgl}{\ensuremath{\mathsf{sgl}}\xspace}
|
||||
% \newcommand{\sctr}{\ensuremath{\mathsf{sctr}}\xspace}
|
||||
|
||||
%%% Reflexivity terms %%%
|
||||
% \newcommand{\reflsym}{{\mathsf{refl}}}
|
||||
% \newcommand{\refl}[1]{\ensuremath{\mathsf{refl}_{#1}}\xspace}
|
||||
|
||||
%%% Path concatenation (used infix, in diagrammatic order) %%%
|
||||
\newcommand{\ct}{%
|
||||
\mathchoice{\mathbin{\raisebox{0.5ex}{$\displaystyle\centerdot$}}}%
|
||||
{\mathbin{\raisebox{0.5ex}{$\centerdot$}}}%
|
||||
{\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}%
|
||||
{\mathbin{\raisebox{0.1ex}{$\scriptscriptstyle\,\centerdot\,$}}}
|
||||
}
|
||||
|
||||
%%% Path reversal %%%
|
||||
\newcommand{\opp}[1]{\mathord{{#1}^{-1}}}
|
||||
\let\rev\opp
|
||||
|
||||
%%% Transport (covariant) %%%
|
||||
\newcommand{\trans}[2]{\ensuremath{{#1}_{*}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||
\let\Trans\trans
|
||||
%\newcommand{\Trans}[2]{\ensuremath{{#1}_{*}\left({#2}\right)}\xspace}
|
||||
\newcommand{\transf}[1]{\ensuremath{{#1}_{*}}\xspace} % Without argument
|
||||
%\newcommand{\transport}[2]{\ensuremath{\mathsf{transport}_{*} \: {#2}\xspace}}
|
||||
\newcommand{\transfib}[3]{\ensuremath{\mathsf{transport}^{#1}(#2,#3)\xspace}}
|
||||
\newcommand{\Transfib}[3]{\ensuremath{\mathsf{transport}^{#1}\Big(#2,\, #3\Big)\xspace}}
|
||||
\newcommand{\transfibf}[1]{\ensuremath{\mathsf{transport}^{#1}\xspace}}
|
||||
|
||||
%%% 2D transport
|
||||
\newcommand{\transtwo}[2]{\ensuremath{\mathsf{transport}^2\mathopen{}\left({#1},{#2}\right)\mathclose{}}\xspace}
|
||||
|
||||
%%% Constant transport
|
||||
\newcommand{\transconst}[3]{\ensuremath{\mathsf{transportconst}}^{#1}_{#2}(#3)\xspace}
|
||||
\newcommand{\transconstf}{\ensuremath{\mathsf{transportconst}}\xspace}
|
||||
|
||||
%%% Map on paths %%%
|
||||
\newcommand{\mapfunc}[1]{\ensuremath{\mathsf{ap}_{#1}}\xspace} % Without argument
|
||||
\newcommand{\map}[2]{\ensuremath{{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||
\let\Ap\map
|
||||
%\newcommand{\Ap}[2]{\ensuremath{{#1}\left({#2}\right)}\xspace}
|
||||
\newcommand{\mapdepfunc}[1]{\ensuremath{\mathsf{apd}_{#1}}\xspace} % Without argument
|
||||
% \newcommand{\mapdep}[2]{\ensuremath{{#1}\llparenthesis{#2}\rrparenthesis}\xspace}
|
||||
\newcommand{\mapdep}[2]{\ensuremath{\mapdepfunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace}
|
||||
\let\apfunc\mapfunc
|
||||
\let\ap\map
|
||||
\let\apdfunc\mapdepfunc
|
||||
\let\apd\mapdep
|
||||
|
||||
%%% 2D map on paths
|
||||
\newcommand{\aptwofunc}[1]{\ensuremath{\mathsf{ap}^2_{#1}}\xspace}
|
||||
\newcommand{\aptwo}[2]{\ensuremath{\aptwofunc{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||
\newcommand{\apdtwofunc}[1]{\ensuremath{\mathsf{apd}^2_{#1}}\xspace}
|
||||
\newcommand{\apdtwo}[2]{\ensuremath{\apdtwofunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace}
|
||||
|
||||
%%% Identity functions %%%
|
||||
\newcommand{\idfunc}[1][]{\ensuremath{\mathsf{id}_{#1}}\xspace}
|
||||
|
||||
%%% Homotopies (written infix) %%%
|
||||
\newcommand{\htpy}{\sim}
|
||||
|
||||
%%% Other meanings of \sim
|
||||
\newcommand{\bisim}{\sim} % bisimulation
|
||||
\newcommand{\eqr}{\sim} % an equivalence relation
|
||||
|
||||
%%% Equivalence types %%%
|
||||
\newcommand{\eqv}[2]{\ensuremath{#1 \simeq #2}\xspace}
|
||||
\newcommand{\eqvspaced}[2]{\ensuremath{#1 \;\simeq\; #2}\xspace}
|
||||
\newcommand{\eqvsym}{\simeq} % infix symbol
|
||||
\newcommand{\texteqv}[2]{\ensuremath{\mathsf{Equiv}(#1,#2)}\xspace}
|
||||
\newcommand{\isequiv}{\ensuremath{\mathsf{isequiv}}}
|
||||
\newcommand{\qinv}{\ensuremath{\mathsf{qinv}}}
|
||||
\newcommand{\ishae}{\ensuremath{\mathsf{ishae}}}
|
||||
\newcommand{\linv}{\ensuremath{\mathsf{linv}}}
|
||||
\newcommand{\rinv}{\ensuremath{\mathsf{rinv}}}
|
||||
\newcommand{\biinv}{\ensuremath{\mathsf{biinv}}}
|
||||
\newcommand{\lcoh}[3]{\mathsf{lcoh}_{#1}(#2,#3)}
|
||||
\newcommand{\rcoh}[3]{\mathsf{rcoh}_{#1}(#2,#3)}
|
||||
\newcommand{\hfib}[2]{{\mathsf{fib}}_{#1}(#2)}
|
||||
|
||||
%%% Map on total spaces %%%
|
||||
\newcommand{\total}[1]{\ensuremath{\mathsf{total}(#1)}}
|
||||
|
||||
%%% Universe types %%%
|
||||
%\newcommand{\type}{\ensuremath{\mathsf{Type}}\xspace}
|
||||
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
|
||||
\let\bbU\UU
|
||||
\let\type\UU
|
||||
% Universes of truncated types
|
||||
\newcommand{\typele}[1]{\ensuremath{{#1}\text-\mathsf{Type}}\xspace}
|
||||
\newcommand{\typeleU}[1]{\ensuremath{{#1}\text-\mathsf{Type}_\UU}\xspace}
|
||||
\newcommand{\typelep}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}}\xspace}
|
||||
\newcommand{\typelepU}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}_\UU}\xspace}
|
||||
\let\ntype\typele
|
||||
\let\ntypeU\typeleU
|
||||
\let\ntypep\typelep
|
||||
\let\ntypepU\typelepU
|
||||
\newcommand{\set}{\ensuremath{\mathsf{Set}}\xspace}
|
||||
\newcommand{\setU}{\ensuremath{\mathsf{Set}_\UU}\xspace}
|
||||
\newcommand{\prop}{\ensuremath{\mathsf{Prop}}\xspace}
|
||||
\newcommand{\propU}{\ensuremath{\mathsf{Prop}_\UU}\xspace}
|
||||
%Pointed types
|
||||
\newcommand{\pointed}[1]{\ensuremath{#1_\bullet}}
|
||||
|
||||
%%% Ordinals and cardinals
|
||||
\newcommand{\card}{\ensuremath{\mathsf{Card}}\xspace}
|
||||
\newcommand{\ord}{\ensuremath{\mathsf{Ord}}\xspace}
|
||||
\newcommand{\ordsl}[2]{{#1}_{/#2}}
|
||||
|
||||
%%% Univalence
|
||||
\newcommand{\ua}{\ensuremath{\mathsf{ua}}\xspace} % the inverse of idtoeqv
|
||||
\newcommand{\idtoeqv}{\ensuremath{\mathsf{idtoeqv}}\xspace}
|
||||
\newcommand{\univalence}{\ensuremath{\mathsf{univalence}}\xspace} % the full axiom
|
||||
|
||||
%%% Truncation levels
|
||||
\newcommand{\iscontr}{\ensuremath{\mathsf{isContr}}}
|
||||
\newcommand{\contr}{\ensuremath{\mathsf{contr}}} % The path to the center of contraction
|
||||
\newcommand{\isset}{\ensuremath{\mathsf{isSet}}}
|
||||
\newcommand{\isprop}{\ensuremath{\mathsf{isProp}}}
|
||||
% h-propositions
|
||||
% \newcommand{\anhprop}{a mere proposition\xspace}
|
||||
% \newcommand{\hprops}{mere propositions\xspace}
|
||||
|
||||
%%% Homotopy fibers %%%
|
||||
%\newcommand{\hfiber}[2]{\ensuremath{\mathsf{hFiber}(#1,#2)}\xspace}
|
||||
\let\hfiber\hfib
|
||||
|
||||
%%% Bracket/squash/truncation types %%%
|
||||
% \newcommand{\brck}[1]{\textsf{mere}(#1)}
|
||||
% \newcommand{\Brck}[1]{\textsf{mere}\Big(#1\Big)}
|
||||
% \newcommand{\trunc}[2]{\tau_{#1}(#2)}
|
||||
% \newcommand{\Trunc}[2]{\tau_{#1}\Big(#2\Big)}
|
||||
% \newcommand{\truncf}[1]{\tau_{#1}}
|
||||
%\newcommand{\trunc}[2]{\Vert #2\Vert_{#1}}
|
||||
\newcommand{\trunc}[2]{\mathopen{}\left\Vert #2\right\Vert_{#1}\mathclose{}}
|
||||
\newcommand{\ttrunc}[2]{\bigl\Vert #2\bigr\Vert_{#1}}
|
||||
\newcommand{\Trunc}[2]{\Bigl\Vert #2\Bigr\Vert_{#1}}
|
||||
\newcommand{\truncf}[1]{\Vert \blank \Vert_{#1}}
|
||||
\newcommand{\tproj}[3][]{\mathopen{}\left|#3\right|_{#2}^{#1}\mathclose{}}
|
||||
\newcommand{\tprojf}[2][]{|\blank|_{#2}^{#1}}
|
||||
\def\pizero{\trunc0}
|
||||
%\newcommand{\brck}[1]{\trunc{-1}{#1}}
|
||||
%\newcommand{\Brck}[1]{\Trunc{-1}{#1}}
|
||||
%\newcommand{\bproj}[1]{\tproj{-1}{#1}}
|
||||
%\newcommand{\bprojf}{\tprojf{-1}}
|
||||
|
||||
\newcommand{\brck}[1]{\trunc{}{#1}}
|
||||
\newcommand{\bbrck}[1]{\ttrunc{}{#1}}
|
||||
\newcommand{\Brck}[1]{\Trunc{}{#1}}
|
||||
\newcommand{\bproj}[1]{\tproj{}{#1}}
|
||||
\newcommand{\bprojf}{\tprojf{}}
|
||||
|
||||
% Big parentheses
|
||||
\newcommand{\Parens}[1]{\Bigl(#1\Bigr)}
|
||||
|
||||
% Projection and extension for truncations
|
||||
\let\extendsmb\ext
|
||||
\newcommand{\extend}[1]{\extendsmb(#1)}
|
||||
|
||||
%
|
||||
%%% The empty type
|
||||
\newcommand{\emptyt}{\ensuremath{\mathbf{0}}\xspace}
|
||||
|
||||
%%% The unit type
|
||||
\newcommand{\unit}{\ensuremath{\mathbf{1}}\xspace}
|
||||
\newcommand{\ttt}{\ensuremath{\star}\xspace}
|
||||
|
||||
%%% The two-element type
|
||||
\newcommand{\bool}{\ensuremath{\mathbf{2}}\xspace}
|
||||
\newcommand{\btrue}{{1_{\bool}}}
|
||||
\newcommand{\bfalse}{{0_{\bool}}}
|
||||
|
||||
%%% Injections into binary sums and pushouts
|
||||
\newcommand{\inlsym}{{\mathsf{inl}}}
|
||||
\newcommand{\inrsym}{{\mathsf{inr}}}
|
||||
\newcommand{\inl}{\ensuremath\inlsym\xspace}
|
||||
\newcommand{\inr}{\ensuremath\inrsym\xspace}
|
||||
|
||||
%%% The segment of the interval
|
||||
\newcommand{\seg}{\ensuremath{\mathsf{seg}}\xspace}
|
||||
|
||||
%%% Free groups
|
||||
\newcommand{\freegroup}[1]{F(#1)}
|
||||
\newcommand{\freegroupx}[1]{F'(#1)} % the "other" free group
|
||||
|
||||
%%% Glue of a pushout
|
||||
\newcommand{\glue}{\mathsf{glue}}
|
||||
|
||||
%%% Circles and spheres
|
||||
\newcommand{\Sn}{\mathbb{S}}
|
||||
\newcommand{\base}{\ensuremath{\mathsf{base}}\xspace}
|
||||
\newcommand{\lloop}{\ensuremath{\mathsf{loop}}\xspace}
|
||||
\newcommand{\surf}{\ensuremath{\mathsf{surf}}\xspace}
|
||||
|
||||
%%% Suspension
|
||||
\newcommand{\susp}{\Sigma}
|
||||
\newcommand{\north}{\mathsf{N}}
|
||||
\newcommand{\south}{\mathsf{S}}
|
||||
\newcommand{\merid}{\mathsf{merid}}
|
||||
|
||||
%%% Blanks (shorthand for lambda abstractions)
|
||||
\newcommand{\blank}{\mathord{\hspace{1pt}\text{--}\hspace{1pt}}}
|
||||
|
||||
%%% Nameless objects
|
||||
\newcommand{\nameless}{\mathord{\hspace{1pt}\underline{\hspace{1ex}}\hspace{1pt}}}
|
||||
|
||||
%%% Some decorations
|
||||
%\newcommand{\bbU}{\ensuremath{\mathbb{U}}\xspace}
|
||||
% \newcommand{\bbB}{\ensuremath{\mathbb{B}}\xspace}
|
||||
\newcommand{\bbP}{\ensuremath{\mathbb{P}}\xspace}
|
||||
|
||||
%%% Some categories
|
||||
\newcommand{\uset}{\ensuremath{\mathcal{S}et}\xspace}
|
||||
\newcommand{\ucat}{\ensuremath{{\mathcal{C}at}}\xspace}
|
||||
\newcommand{\urel}{\ensuremath{\mathcal{R}el}\xspace}
|
||||
\newcommand{\uhilb}{\ensuremath{\mathcal{H}ilb}\xspace}
|
||||
\newcommand{\utype}{\ensuremath{\mathcal{T}\!ype}\xspace}
|
||||
|
||||
% Pullback corner
|
||||
%\newbox\pbbox
|
||||
%\setbox\pbbox=\hbox{\xy \POS(65,0)\ar@{-} (0,0) \ar@{-} (65,65)\endxy}
|
||||
%\def\pb{\save[]+<3.5mm,-3.5mm>*{\copy\pbbox} \restore}
|
||||
|
||||
% Macros for the categories chapter
|
||||
% \newcommand{\inv}[1]{{#1}^{-1}}
|
||||
\newcommand{\idtoiso}{\ensuremath{\mathsf{idtoiso}}\xspace}
|
||||
\newcommand{\isotoid}{\ensuremath{\mathsf{isotoid}}\xspace}
|
||||
\newcommand{\op}{^{\mathrm{op}}}
|
||||
\newcommand{\y}{\ensuremath{\mathbf{y}}\xspace}
|
||||
\newcommand{\dgr}[1]{{#1}^{\dagger}}
|
||||
\newcommand{\unitaryiso}{\mathrel{\cong^\dagger}}
|
||||
\newcommand{\cteqv}[2]{\ensuremath{#1 \simeq #2}\xspace}
|
||||
\newcommand{\cteqvsym}{\simeq} % Symbol for equivalence of categories
|
||||
|
||||
%%% Natural numbers
|
||||
\newcommand{\N}{\ensuremath{\mathbb{N}}\xspace}
|
||||
%\newcommand{\N}{\textbf{N}}
|
||||
\let\nat\N
|
||||
\newcommand{\natp}{\ensuremath{\nat'}\xspace} % alternative nat in induction chapter
|
||||
|
||||
\newcommand{\zerop}{\ensuremath{0'}\xspace} % alternative zero in induction chapter
|
||||
\newcommand{\suc}{\mathsf{succ}}
|
||||
\newcommand{\sucp}{\ensuremath{\suc'}\xspace} % alternative suc in induction chapter
|
||||
\newcommand{\add}{\mathsf{add}}
|
||||
\newcommand{\ack}{\mathsf{ack}}
|
||||
\newcommand{\ite}{\mathsf{iter}}
|
||||
\newcommand{\assoc}{\mathsf{assoc}}
|
||||
\newcommand{\dbl}{\ensuremath{\mathsf{double}}}
|
||||
\newcommand{\dblp}{\ensuremath{\dbl'}\xspace} % alternative double in induction chapter
|
||||
|
||||
|
||||
%%% Lists
|
||||
\newcommand{\lst}[1]{\mathsf{List}(#1)}
|
||||
\newcommand{\nil}{\mathsf{nil}}
|
||||
\newcommand{\cons}{\mathsf{cons}}
|
||||
|
||||
%%% Vectors of given length, used in induction chapter
|
||||
\newcommand{\vect}[2]{\ensuremath{\mathsf{Vec}_{#1}(#2)}\xspace}
|
||||
|
||||
%%% Integers
|
||||
\newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace}
|
||||
\newcommand{\Zsuc}{\mathsf{succ}}
|
||||
\newcommand{\Zpred}{\mathsf{pred}}
|
||||
|
||||
%%% Rationals
|
||||
\newcommand{\Q}{\ensuremath{\mathbb{Q}}\xspace}
|
||||
|
||||
%%% Function extensionality
|
||||
\newcommand{\funext}{\mathsf{funext}}
|
||||
\newcommand{\happly}{\mathsf{happly}}
|
||||
|
||||
%%% A naturality lemma
|
||||
\newcommand{\com}[3]{\mathsf{swap}_{#1,#2}(#3)}
|
||||
|
||||
%%% Code/encode/decode
|
||||
\newcommand{\code}{\ensuremath{\mathsf{code}}\xspace}
|
||||
\newcommand{\encode}{\ensuremath{\mathsf{encode}}\xspace}
|
||||
\newcommand{\decode}{\ensuremath{\mathsf{decode}}\xspace}
|
||||
|
||||
% Function definition with domain and codomain
|
||||
\newcommand{\function}[4]{\left\{\begin{array}{rcl}#1 &
|
||||
\longrightarrow & #2 \\ #3 & \longmapsto & #4 \end{array}\right.}
|
||||
|
||||
%%% Cones and cocones
|
||||
\newcommand{\cone}[2]{\mathsf{cone}_{#1}(#2)}
|
||||
\newcommand{\cocone}[2]{\mathsf{cocone}_{#1}(#2)}
|
||||
% Apply a function to a cocone
|
||||
\newcommand{\composecocone}[2]{#1\circ#2}
|
||||
\newcommand{\composecone}[2]{#2\circ#1}
|
||||
%%% Diagrams
|
||||
\newcommand{\Ddiag}{\mathscr{D}}
|
||||
|
||||
%%% (pointed) mapping spaces
|
||||
\newcommand{\Map}{\mathsf{Map}}
|
||||
|
||||
%%% The interval
|
||||
\newcommand{\interval}{\ensuremath{I}\xspace}
|
||||
\newcommand{\izero}{\ensuremath{0_{\interval}}\xspace}
|
||||
\newcommand{\ione}{\ensuremath{1_{\interval}}\xspace}
|
||||
|
||||
%%% Arrows
|
||||
\newcommand{\epi}{\ensuremath{\twoheadrightarrow}}
|
||||
\newcommand{\mono}{\ensuremath{\rightarrowtail}}
|
||||
|
||||
%%% Sets
|
||||
\newcommand{\bin}{\ensuremath{\mathrel{\widetilde{\in}}}}
|
||||
|
||||
%%% Semigroup structure
|
||||
\newcommand{\semigroupstrsym}{\ensuremath{\mathsf{SemigroupStr}}}
|
||||
\newcommand{\semigroupstr}[1]{\ensuremath{\mathsf{SemigroupStr}}(#1)}
|
||||
\newcommand{\semigroup}[0]{\ensuremath{\mathsf{Semigroup}}}
|
||||
|
||||
%%% Macros for the formal type theory
|
||||
\newcommand{\emptyctx}{\ensuremath{\cdot}}
|
||||
\newcommand{\production}{\vcentcolon\vcentcolon=}
|
||||
\newcommand{\conv}{\downarrow}
|
||||
\newcommand{\ctx}{\ensuremath{\mathsf{ctx}}}
|
||||
\newcommand{\wfctx}[1]{#1\ \ctx}
|
||||
\newcommand{\oftp}[3]{#1 \vdash #2 : #3}
|
||||
\newcommand{\jdeqtp}[4]{#1 \vdash #2 \jdeq #3 : #4}
|
||||
\newcommand{\judg}[2]{#1 \vdash #2}
|
||||
\newcommand{\tmtp}[2]{#1 \mathord{:} #2}
|
||||
|
||||
% rule names
|
||||
\newcommand{\form}{\textsc{form}}
|
||||
\newcommand{\intro}{\textsc{intro}}
|
||||
\newcommand{\elim}{\textsc{elim}}
|
||||
\newcommand{\comp}{\textsc{comp}}
|
||||
\newcommand{\uniq}{\textsc{uniq}}
|
||||
\newcommand{\Weak}{\mathsf{Wkg}}
|
||||
\newcommand{\Vble}{\mathsf{Vble}}
|
||||
\newcommand{\Exch}{\mathsf{Exch}}
|
||||
\newcommand{\Subst}{\mathsf{Subst}}
|
||||
|
||||
%%% Macros for HITs
|
||||
\newcommand{\cc}{\mathsf{c}}
|
||||
\newcommand{\pp}{\mathsf{p}}
|
||||
\newcommand{\cct}{\widetilde{\mathsf{c}}}
|
||||
\newcommand{\ppt}{\widetilde{\mathsf{p}}}
|
||||
\newcommand{\Wtil}{\ensuremath{\widetilde{W}}\xspace}
|
||||
|
||||
%%% Macros for n-types
|
||||
\newcommand{\istype}[1]{\mathsf{is}\mbox{-}{#1}\mbox{-}\mathsf{type}}
|
||||
\newcommand{\nplusone}{\ensuremath{(n+1)}}
|
||||
\newcommand{\nminusone}{\ensuremath{(n-1)}}
|
||||
% \newcommand{\fact}{\mathsf{fact}}
|
||||
|
||||
%%% Macros for homotopy
|
||||
\newcommand{\kbar}{\overline{k}} % Used in van Kampen's theorem
|
||||
|
||||
%%% Macros for induction
|
||||
\newcommand{\natw}{\ensuremath{\mathbf{N^w}}\xspace}
|
||||
\newcommand{\zerow}{\ensuremath{0^\mathbf{w}}\xspace}
|
||||
\newcommand{\sucw}{\ensuremath{\mathbf{s^w}}\xspace}
|
||||
\newcommand{\nalg}{\nat\mathsf{Alg}}
|
||||
\newcommand{\nhom}{\nat\mathsf{Hom}}
|
||||
\newcommand{\ishinitw}{\mathsf{isHinit}_{\mathsf{W}}}
|
||||
\newcommand{\ishinitn}{\mathsf{isHinit}_\nat}
|
||||
\newcommand{\w}{\mathsf{W}}
|
||||
\newcommand{\walg}{\w\mathsf{Alg}}
|
||||
\newcommand{\whom}{\w\mathsf{Hom}}
|
||||
|
||||
%%% Macros for real numbers
|
||||
\newcommand{\RC}{\ensuremath{\mathbb{R}_\mathsf{c}}\xspace} % Cauchy
|
||||
\newcommand{\RD}{\ensuremath{\mathbb{R}_\mathsf{d}}\xspace} % Dedekind
|
||||
\newcommand{\R}{\ensuremath{\mathbb{R}}\xspace} % Either
|
||||
\newcommand{\barRD}{\ensuremath{\bar{\mathbb{R}}_\mathsf{d}}\xspace} % Dedekind completion of Dedekind
|
||||
|
||||
\newcommand{\close}[1]{\sim_{#1}} % Relation of closeness
|
||||
\newcommand{\closesym}{\mathord\sim}
|
||||
\newcommand{\rclim}{\mathsf{lim}} % HIT constructor for Cauchy reals
|
||||
\newcommand{\rcrat}{\mathsf{rat}} % Embedding of rationals into Cauchy reals
|
||||
\newcommand{\rceq}{\mathsf{eq}_{\RC}} % HIT path constructor
|
||||
\newcommand{\CAP}{\mathcal{C}} % The type of Cauchy approximations
|
||||
\newcommand{\Qp}{\Q_{+}}
|
||||
\newcommand{\apart}{\mathrel{\#}} % apartness
|
||||
\newcommand{\dcut}{\mathsf{isCut}} % Dedekind cut
|
||||
\newcommand{\cover}{\triangleleft} % inductive cover
|
||||
\newcommand{\intfam}[3]{(#2, \lam{#1} #3)} % family of rational intervals
|
||||
|
||||
% Macros for the Cauchy reals construction
|
||||
\newcommand{\bsim}{\frown}
|
||||
\newcommand{\bbsim}{\smile}
|
||||
|
||||
\newcommand{\hapx}{\diamondsuit\approx}
|
||||
\newcommand{\hapname}{\diamondsuit}
|
||||
\newcommand{\hapxb}{\heartsuit\approx}
|
||||
\newcommand{\hapbname}{\heartsuit}
|
||||
\newcommand{\tap}[1]{\bullet\approx_{#1}\triangle}
|
||||
\newcommand{\tapname}{\triangle}
|
||||
\newcommand{\tapb}[1]{\bullet\approx_{#1}\square}
|
||||
\newcommand{\tapbname}{\square}
|
||||
|
||||
%%% Macros for surreals
|
||||
\newcommand{\NO}{\ensuremath{\mathsf{No}}\xspace}
|
||||
\newcommand{\surr}[2]{\{\,#1\,\big|\,#2\,\}}
|
||||
\newcommand{\LL}{\mathcal{L}}
|
||||
\newcommand{\RR}{\mathcal{R}}
|
||||
\newcommand{\noeq}{\mathsf{eq}_{\NO}} % HIT path constructor
|
||||
|
||||
\newcommand{\ble}{\trianglelefteqslant}
|
||||
\newcommand{\blt}{\vartriangleleft}
|
||||
\newcommand{\bble}{\sqsubseteq}
|
||||
\newcommand{\bblt}{\sqsubset}
|
||||
|
||||
\newcommand{\hle}{\diamondsuit\preceq}
|
||||
\newcommand{\hlt}{\diamondsuit\prec}
|
||||
\newcommand{\hlname}{\diamondsuit}
|
||||
\newcommand{\hleb}{\heartsuit\preceq}
|
||||
\newcommand{\hltb}{\heartsuit\prec}
|
||||
\newcommand{\hlbname}{\heartsuit}
|
||||
% \newcommand{\tle}{(\bullet\preceq\triangle)}
|
||||
% \newcommand{\tlt}{(\bullet\prec\triangle)}
|
||||
\newcommand{\tle}{\triangle\preceq}
|
||||
\newcommand{\tlt}{\triangle\prec}
|
||||
\newcommand{\tlname}{\triangle}
|
||||
% \newcommand{\tleb}{(\bullet\preceq\square)}
|
||||
% \newcommand{\tltb}{(\bullet\prec\square)}
|
||||
\newcommand{\tleb}{\square\preceq}
|
||||
\newcommand{\tltb}{\square\prec}
|
||||
\newcommand{\tlbname}{\square}
|
||||
|
||||
%%% Macros for set theory
|
||||
\newcommand{\vset}{\mathsf{set}} % point constructor for cummulative hierarchy V
|
||||
\def\cd{\tproj0}
|
||||
\newcommand{\inj}{\ensuremath{\mathsf{inj}}} % type of injections
|
||||
\newcommand{\acc}{\ensuremath{\mathsf{acc}}} % accessibility
|
||||
|
||||
\newcommand{\atMostOne}{\mathsf{atMostOne}}
|
||||
|
||||
\newcommand{\power}[1]{\mathcal{P}(#1)} % power set
|
||||
\newcommand{\powerp}[1]{\mathcal{P}_+(#1)} % inhabited power set
|
||||
|
||||
%%%% THEOREM ENVIRONMENTS %%%%
|
||||
|
||||
% Hyperref includes the command \autoref{...} which is like \ref{...}
|
||||
% except that it automatically inserts the type of the thing you're
|
||||
% referring to, e.g. it produces "Theorem 3.8" instead of just "3.8"
|
||||
% (and makes the whole thing a hyperlink). This saves a slight amount
|
||||
% of typing, but more importantly it means that if you decide later on
|
||||
% that 3.8 should be a Lemma or a Definition instead of a Theorem, you
|
||||
% don't have to change the name in all the places you referred to it.
|
||||
|
||||
% The following hack improves on this by using the same counter for
|
||||
% all theorem-type environments, so that after Theorem 1.1 comes
|
||||
% Corollary 1.2 rather than Corollary 1.1. This makes it much easier
|
||||
% for the reader to find a particular theorem when flipping through
|
||||
% the document.
|
||||
\makeatletter
|
||||
\def\defthm#1#2#3{%
|
||||
%% Ensure all theorem types are numbered with the same counter
|
||||
\newaliascnt{#1}{thm}
|
||||
\newtheorem{#1}[#1]{#2}
|
||||
\aliascntresetthe{#1}
|
||||
%% This command tells cleveref's \cref what to call things
|
||||
\crefname{#1}{#2}{#3}}
|
||||
|
||||
% Now define a bunch of theorem-type environments.
|
||||
\newtheorem{thm}{Theorem}[section]
|
||||
\crefname{thm}{Theorem}{Theorems}
|
||||
\defthm{propn}{Proposition}{Propositions} % Probably we shouldn't use "Proposition" in this way
|
||||
\defthm{cor}{Corollary}{Corollaries}
|
||||
\defthm{lem}{Lemma}{Lemmas}
|
||||
\defthm{ax}{Axiom}{Axioms}
|
||||
\defthm{conj}{Conjecture}{Conjectures}
|
||||
% Since definitions and theorems in type theory are synonymous, should
|
||||
% we actually use the same theoremstyle for them?
|
||||
\theoremstyle{definition}
|
||||
\defthm{defn}{Definition}{Definitions}
|
||||
\theoremstyle{remark}
|
||||
\defthm{rmk}{Remark}{Remarks}
|
||||
\defthm{ex}{Example}{Examples}
|
||||
\defthm{exs}{Examples}{Examples}
|
||||
\defthm{notes}{Notes}{Notes}
|
||||
% Number exercises within chapters, with their own counter.
|
||||
%\newtheorem{ex}{Exercise}[chapter]
|
||||
%\crefname{ex}{Exercise}{Exercises}
|
||||
|
||||
% Display format for sections
|
||||
\crefformat{section}{\S#2#1#3}
|
||||
\Crefformat{section}{Section~#2#1#3}
|
||||
\crefrangeformat{section}{\S\S#3#1#4--#5#2#6}
|
||||
\Crefrangeformat{section}{Sections~#3#1#4--#5#2#6}
|
||||
\crefmultiformat{section}{\S\S#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||
\Crefmultiformat{section}{Sections~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||
\crefrangemultiformat{section}{\S\S#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||
\Crefrangemultiformat{section}{Sections~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||
|
||||
% Display format for appendices
|
||||
\crefformat{appendix}{Appendix~#2#1#3}
|
||||
\Crefformat{appendix}{Appendix~#2#1#3}
|
||||
\crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6}
|
||||
\Crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6}
|
||||
\crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||
\Crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||
\crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||
\Crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||
|
||||
\crefname{part}{Part}{Parts}
|
||||
|
||||
% Number subsubsections
|
||||
\setcounter{secnumdepth}{5}
|
||||
|
||||
% Display format for figures
|
||||
\crefname{figure}{Figure}{Figures}
|
||||
|
||||
% Use cleveref instead of hyperref's \autoref
|
||||
\let\autoref\cref
|
||||
|
||||
|
||||
%%%% EQUATION NUMBERING %%%%
|
||||
|
||||
% The following hack uses the single theorem counter to number
|
||||
% equations as well, so that we don't have both Theorem 1.1 and
|
||||
% equation (1.1).
|
||||
\let\c@equation\c@thm
|
||||
\numberwithin{equation}{section}
|
||||
|
||||
|
||||
%%%% ENUMERATE NUMBERING %%%%
|
||||
|
||||
% Number the first level of enumerates as (i), (ii), ...
|
||||
\renewcommand{\theenumi}{(\roman{enumi})}
|
||||
\renewcommand{\labelenumi}{\theenumi}
|
||||
|
||||
|
||||
%%%% MARGINS %%%%
|
||||
|
||||
% This is a matter of personal preference, but I think the left
|
||||
% margins on enumerates and itemizes are too wide.
|
||||
% \setitemize[1]{leftmargin=2em}
|
||||
% \setenumerate[1]{leftmargin=*}
|
||||
|
||||
% Likewise that they are too spaced out.
|
||||
% \setitemize[1]{itemsep=-0.2em}
|
||||
% \setenumerate[1]{itemsep=-0.2em}
|
||||
|
||||
%%% Notes %%%
|
||||
\def\noteson{%
|
||||
\gdef\note##1{\mbox{}\marginpar{\color{blue}\textasteriskcentered\ ##1}}}
|
||||
\gdef\notesoff{\gdef\note##1{\null}}
|
||||
\noteson
|
||||
|
||||
\newcommand{\Coq}{\textsc{Coq}\xspace}
|
||||
\newcommand{\Agda}{\textsc{Agda}\xspace}
|
||||
\newcommand{\NuPRL}{\textsc{NuPRL}\xspace}
|
||||
|
||||
%%%% CITATIONS %%%%
|
||||
|
||||
% \let \cite \citep
|
||||
|
||||
%%%% INDEX %%%%
|
||||
|
||||
\newcommand{\footstyle}[1]{{\hyperpage{#1}}n} % If you index something that is in a footnote
|
||||
\newcommand{\defstyle}[1]{\textbf{\hyperpage{#1}}} % Style for pageref to a definition
|
||||
|
||||
\newcommand{\indexdef}[1]{\index{#1|defstyle}} % Index a definition
|
||||
\newcommand{\indexfoot}[1]{\index{#1|footstyle}} % Index a term in a footnote
|
||||
\newcommand{\indexsee}[2]{\index{#1|see{#2}}} % Index "see also"
|
||||
|
||||
|
||||
%%%% Standard phrasing or spelling of common phrases %%%%
|
||||
|
||||
\newcommand{\ZF}{Zermelo--Fraenkel}
|
||||
\newcommand{\CZF}{Constructive \ZF{} Set Theory}
|
||||
|
||||
\newcommand{\LEM}[1]{\ensuremath{\mathsf{LEM}_{#1}}\xspace}
|
||||
\newcommand{\choice}[1]{\ensuremath{\mathsf{AC}_{#1}}\xspace}
|
||||
|
||||
%%%% MISC %%%%
|
||||
|
||||
\newcommand{\mentalpause}{\medskip} % Use for "mental" pause, instead of \smallskip or \medskip
|
||||
|
||||
%% Use \symlabel instead of \label to mark a pageref that you need in the index of symbols
|
||||
\newcounter{symindex}
|
||||
\newcommand{\symlabel}[1]{\refstepcounter{symindex}\label{#1}}
|
||||
|
||||
% Local Variables:
|
||||
% mode: latex
|
||||
% TeX-master: "hott-online"
|
||||
% End:
|
||||
20
src/MayConcise/Chapter1.lagda.md
Normal file
20
src/MayConcise/Chapter1.lagda.md
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
module MayConcise.Chapter1 where
|
||||
```
|
||||
|
||||
## 1 What is algebraic topology?
|
||||
|
||||
https://en.wikipedia.org/wiki/Homomorphism
|
||||
|
||||
> A homomorphism is a map between two algebraic structures of the same type (that is of the same name), that preserves the operations of the structures. This means a map f : A → B {\displaystyle f:A\to B} between two sets A {\displaystyle A}, B {\displaystyle B} equipped with the same structure such that, if ⋅ {\displaystyle \cdot } is an operation of the structure (supposed here, for simplification, to be a binary operation), then
|
||||
>
|
||||
> ```
|
||||
> f ( x ⋅ y ) = f ( x ) ⋅ f ( y ) {\displaystyle f(x\cdot y)=f(x)\cdot f(y)}
|
||||
> ```
|
||||
>
|
||||
> for every pair x {\displaystyle x}, y {\displaystyle y} of elements of A {\displaystyle A}.
|
||||
|
||||
```
|
||||
homotopy : {X Y : Set} {p q : X → Y}
|
||||
```
|
||||
29
src/VanDoornDissertation/HIT.lagda.md
Normal file
29
src/VanDoornDissertation/HIT.lagda.md
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
module VanDoornDissertation.HIT where
|
||||
|
||||
open import Data.Nat
|
||||
open import VanDoornDissertation.Preliminaries
|
||||
```
|
||||
|
||||
# 3 Higher Inductive Types
|
||||
|
||||
## 3.1 Propositional Truncation
|
||||
|
||||
```
|
||||
data one-step-truncation (A : Set) : Set where
|
||||
f : A → one-step-truncation A
|
||||
e : (x y : A) → f x ≡ f y
|
||||
|
||||
weakly-constant : {A B : Set} → (g : A → B) → Set
|
||||
weakly-constant {A} g = {x y : A} → g x ≡ g y
|
||||
|
||||
definition3∙1∙1 : {A : Set} → one-step-truncation A → ℕ → Set
|
||||
definition3∙1∙1 {A} trunc zero = A
|
||||
definition3∙1∙1 {A} trunc (suc n) = one-step-truncation (definition3∙1∙1 trunc n)
|
||||
|
||||
fs : {A : Set} → one-step-truncation A → (n : ℕ) → Set
|
||||
fs trunc n = (definition3∙1∙1 trunc n) → (definition3∙1∙1 trunc (suc n))
|
||||
|
||||
-- lemma3∙1∙3 : {X : Set} → {x : X} → is
|
||||
```
|
||||
89
src/VanDoornDissertation/Preliminaries.lagda.md
Normal file
89
src/VanDoornDissertation/Preliminaries.lagda.md
Normal file
|
|
@ -0,0 +1,89 @@
|
|||
```
|
||||
{-# OPTIONS --cubical #-}
|
||||
module VanDoornDissertation.Preliminaries where
|
||||
|
||||
open import Agda.Primitive
|
||||
open import Agda.Primitive.Cubical
|
||||
```
|
||||
|
||||
### 2.2.1 Paths
|
||||
|
||||
```
|
||||
Path : {ℓ : Level} (A : Set ℓ) → A → A → Set ℓ
|
||||
Path A = PathP (λ i → A)
|
||||
|
||||
infix 4 _≡_
|
||||
_≡_ : {ℓ : Level} {A : Set ℓ} → A → A → Set ℓ
|
||||
_≡_ {A = A} = Path A
|
||||
|
||||
private
|
||||
to-path : {ℓ : Level} {A : Set ℓ} → (f : I → A) → Path A (f i0) (f i1)
|
||||
to-path f i = f i
|
||||
refl : {ℓ : Level} {A : Set ℓ} {x : A} → x ≡ x
|
||||
refl {x = x} = to-path (λ i → x)
|
||||
|
||||
id : {l : Level} {A : Set l} → A → A
|
||||
id x = x
|
||||
|
||||
ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
|
||||
→ (f : A → B)
|
||||
→ (p : x ≡ y)
|
||||
→ f x ≡ f y
|
||||
ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)
|
||||
-- J (λ x y p → f x ≡ f y) (λ x → refl) x y p
|
||||
|
||||
transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
|
||||
→ (P : A → Set l₂)
|
||||
→ (p : x ≡ y)
|
||||
→ P x → P y
|
||||
transport {l₁} {l₂} {A} {x} {y} P p = primTransp (λ i → P (p i)) i0
|
||||
```
|
||||
|
||||
### 2.2.3 More on paths
|
||||
|
||||
#### Pathovers
|
||||
|
||||
```
|
||||
dependent-path : {A : Set}
|
||||
→ (P : A → Set)
|
||||
→ {x y : A}
|
||||
→ (p : x ≡ y)
|
||||
→ (u : P x) → (v : P y) → Set
|
||||
dependent-path P p u v = transport P p u ≡ v
|
||||
|
||||
syntax dependent-path P p u v = u ≡[ P , p ] v
|
||||
|
||||
-- https://git.mzhang.io/school/type-theory/issues/16
|
||||
apd : ∀ {a b} {A : I → Set a} {B : (i : I) → A i → Set b}
|
||||
→ (f : (i : I) → (a : A i) → B i a)
|
||||
→ {x : A i0}
|
||||
→ {y : A i1}
|
||||
→ (p : PathP A x y)
|
||||
→ PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
|
||||
apd f p i = f i (p i)
|
||||
```
|
||||
|
||||
#### Squares
|
||||
|
||||
```
|
||||
data square {A : Set} {a00 : A} : {a20 a02 a22 : A}
|
||||
→ a00 ≡ a20
|
||||
→ a02 ≡ a22
|
||||
→ a00 ≡ a02
|
||||
→ a20 ≡ a22
|
||||
→ Set
|
||||
where
|
||||
reflₛ : square refl refl refl refl
|
||||
```
|
||||
|
||||
#### Squareovers and cubes
|
||||
|
||||
```
|
||||
|
||||
```
|
||||
|
||||
#### Paths in type formers
|
||||
|
||||
```
|
||||
|
||||
```
|
||||
Loading…
Reference in a new issue