diff options
Diffstat (limited to 'thesis.org')
| -rw-r--r-- | thesis.org | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -35,6 +35,9 @@ #+latex_compiler: pdflatex + +#+latex_header: \newunicodechar{ʳ}{\ensuremath{^\texttt{r}}} +#+latex_header: \newunicodechar{ˡ}{\ensuremath{^\texttt{l}}} #+latex_header: \newunicodechar{Γ}{\ensuremath{\Gamma}} #+latex_header: \newunicodechar{Δ}{\ensuremath{\Delta}} #+latex_header: \newunicodechar{Κ}{\ensuremath{K}} @@ -44,15 +47,12 @@ #+latex_header: \newunicodechar{ε}{\ensuremath{\epsilon}} #+latex_header: \newunicodechar{λ}{\ensuremath{\lambda}} #+latex_header: \newunicodechar{σ}{\ensuremath{\sigma}} -#+latex_header: \newunicodechar{ˡ}{\ensuremath{^\texttt{l}}} -#+latex_header: \newunicodechar{ʳ}{\ensuremath{^\texttt{r}}} #+latex_header: \newunicodechar{ᵗ}{\ensuremath{^\texttt{t}}} #+latex_header: \newunicodechar{′}{\ensuremath{'}} #+latex_header: \newunicodechar{₁}{\ensuremath{_1}} #+latex_header: \newunicodechar{₂}{\ensuremath{_2}} #+latex_header: \newunicodechar{ₛ}{\ensuremath{_\texttt{s}}} #+latex_header: \newunicodechar{ₜ}{\ensuremath{_\texttt{t}}} - #+latex_header: \newunicodechar{ℓ}{l} #+latex_header: \newunicodechar{ℕ}{\ensuremath{\mathbb{N}}} #+latex_header: \newunicodechar{ℚ}{\ensuremath{\mathbb{Q}}} @@ -74,6 +74,7 @@ #+latex_header: \newunicodechar{≢}{\ensuremath{\not\equiv}} #+latex_header: \newunicodechar{⊆}{\ensuremath{\subseteq}} #+latex_header: \newunicodechar{⊎}{\ensuremath{\uplus}} +#+latex_header: \newunicodechar{⊔}{\ensuremath{\sqcup}} #+latex_header: \newunicodechar{⊤}{\ensuremath{\top}} #+latex_header: \newunicodechar{⊥}{\ensuremath{\bot}} #+latex_header: \newunicodechar{⌊}{\ensuremath{\lfloor}} @@ -231,7 +232,7 @@ xyz #+latex: \fi #+latex: \cleardoublepage -#+toc: headlines 4 +#+toc: headlines 2 # #+toc: listings # #+toc: tables @@ -539,7 +540,7 @@ defined using a record [cite:@agda.readthedocs.io p. be used to define a setoid-enriched monoid: #+begin_src agda2 -record Monoid ℓ₁ ℓ₂ : Set (ℓsuc (ℓ₁ \lub ℓ₂)) where +record Monoid ℓ₁ ℓ₂ : Set (ℓsuc (ℓ₁ ⊔ ℓ₂)) where infixl 5 _∙_ infix 4 _≈_ field |