-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmain.toc
More file actions
62 lines (62 loc) · 5.01 KB
/
Copy pathmain.toc
File metadata and controls
62 lines (62 loc) · 5.01 KB
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
\contentsline {section}{\numberline {1}Introduction}{2}{section.1}%
\contentsline {section}{\numberline {2}Background}{4}{section.2}%
\contentsline {subsection}{\numberline {2.1}Motivation}{4}{subsection.2.1}%
\contentsline {subsubsection}{\numberline {2.1.1}Set Theory and Classical Foundations}{4}{subsubsection.2.1.1}%
\contentsline {subsubsection}{\numberline {2.1.2}Contrast between Type Theory and Set Theory}{4}{subsubsection.2.1.2}%
\contentsline {section}{\numberline {3}Type Theory}{6}{section.3}%
\contentsline {subsection}{\numberline {3.1}Dependent Types}{7}{subsection.3.1}%
\contentsline {subsection}{\numberline {3.2}Inference Rules}{7}{subsection.3.2}%
\contentsline {subsection}{\numberline {3.3}$\Pi $-types}{8}{subsection.3.3}%
\contentsline {subsubsection}{\numberline {3.3.1}Inference Rules for $\Pi $-types}{8}{subsubsection.3.3.1}%
\contentsline {subsection}{\numberline {3.4}$\Sigma $-types}{9}{subsection.3.4}%
\contentsline {subsubsection}{\numberline {3.4.1}Inference Rules for $\Sigma $-type}{9}{subsubsection.3.4.1}%
\contentsline {subsection}{\numberline {3.5}Inductive Types}{11}{subsection.3.5}%
\contentsline {subsection}{\numberline {3.6}Identity Types}{11}{subsection.3.6}%
\contentsline {subsubsection}{\numberline {3.6.1}Operations on Paths}{12}{subsubsection.3.6.1}%
\contentsline {subsection}{\numberline {3.7}Propositions as Types}{13}{subsection.3.7}%
\contentsline {section}{\numberline {4}Basic Category Theory and Homotopy Theory}{14}{section.4}%
\contentsline {subsection}{\numberline {4.1}Category Theory: Basics}{14}{subsection.4.1}%
\contentsline {subsection}{\numberline {4.2}Homotopies}{15}{subsection.4.2}%
\contentsline {section}{\numberline {5}The Homotopy Interpretation}{18}{section.5}%
\contentsline {paragraph}{Identity types as path spaces}{18}{section*.3}%
\contentsline {paragraph}{Type families as fibrations}{18}{section*.4}%
\contentsline {paragraph}{Transport as path lifting}{19}{section*.5}%
\contentsline {paragraph}{Contractible types}{19}{section*.6}%
\contentsline {paragraph}{Analytic vs.\ synthetic}{20}{section*.7}%
\contentsline {section}{\numberline {6}Univalent Foundations}{21}{section.6}%
\contentsline {subsection}{\numberline {6.1}Univalence}{21}{subsection.6.1}%
\contentsline {subsection}{\numberline {6.2}Higher Inductive Types (HITs)}{22}{subsection.6.2}%
\contentsline {subsection}{\numberline {6.3}Truncation Levels}{23}{subsection.6.3}%
\contentsline {subsection}{\numberline {6.4}Formalization}{24}{subsection.6.4}%
\contentsline {subsection}{\numberline {6.5}Proof Assistants}{25}{subsection.6.5}%
\contentsline {subsubsection}{\numberline {6.5.1}Lean}{25}{subsubsection.6.5.1}%
\contentsline {subsubsection}{\numberline {6.5.2}A Note on Lean 4 Syntax}{26}{subsubsection.6.5.2}%
\contentsline {paragraph}{Type signatures}{26}{section*.8}%
\contentsline {paragraph}{Inductive types}{26}{section*.9}%
\contentsline {paragraph}{Function definitions, \texttt {def} and \texttt {axiom}}{26}{section*.10}%
\contentsline {paragraph}{Dependent function types ($\Pi $-types)}{26}{section*.11}%
\contentsline {paragraph}{Dependent pair types ($\Sigma $-types)}{27}{section*.12}%
\contentsline {paragraph}{Universe levels}{27}{section*.13}%
\contentsline {paragraph}{Path induction: \texttt {p.rec} and \texttt {@Identity.rec}}{27}{section*.14}%
\contentsline {paragraph}{Nested $\Sigma $-type projections}{27}{section*.15}%
\contentsline {paragraph}{Elaboration heartbeats}{27}{section*.16}%
\contentsline {paragraph}{Tactics}{27}{section*.17}%
\contentsline {section}{\numberline {7}Formalization in HoTTLean}{28}{section.7}%
\contentsline {subsection}{\numberline {7.1}The HoTTLean Library}{28}{subsection.7.1}%
\contentsline {subsubsection}{\numberline {7.1.1}SynthLean}{28}{subsubsection.7.1.1}%
\contentsline {subsubsection}{\numberline {7.1.2}Summary of Contributions}{29}{subsubsection.7.1.2}%
\contentsline {subsection}{\numberline {7.2}Magma Type}{29}{subsection.7.2}%
\contentsline {subsubsection}{\numberline {7.2.1}Motivating Magmas}{29}{subsubsection.7.2.1}%
\contentsline {subsubsection}{\numberline {7.2.2}Paths in $\Sigma $-Types}{30}{subsubsection.7.2.2}%
\contentsline {subsubsection}{\numberline {7.2.3}The Structure Identity Principle}{31}{subsubsection.7.2.3}%
\contentsline {subsubsection}{\numberline {7.2.4}Proof for Formalization}{32}{subsubsection.7.2.4}%
\contentsline {subsubsection}{\numberline {7.2.5}Lean Formalization}{33}{subsubsection.7.2.5}%
\contentsline {paragraph}{Auxiliaries}{34}{section*.18}%
\contentsline {paragraph}{Formalization}{36}{section*.19}%
\contentsline {subsection}{\numberline {7.3}Hedberg's Theorem}{40}{subsection.7.3}%
\contentsline {subsubsection}{\numberline {7.3.1}Identity Systems}{40}{subsubsection.7.3.1}%
\contentsline {subsubsection}{\numberline {7.3.2}Proof}{41}{subsubsection.7.3.2}%
\contentsline {subsubsection}{\numberline {7.3.3}Lean Formalization}{43}{subsubsection.7.3.3}%
\contentsline {section}{\numberline {8}Conclusion}{46}{section.8}%
\contentsline {section}{\numberline {9}Future Work}{47}{section.9}%
\contentsline {section}{\numberline {10}Appendix Code}{48}{section.10}%