typeset huber equations for stt

Author: 5HT

doc/anders.pdf

@@ -51,6 +51,8 @@
 \DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}}
 \DeclareUnicodeCharacter{03C8}{\ensuremath{\psi}}
 \DeclareUnicodeCharacter{2605}{\ensuremath{\star}}
+\DeclareUnicodeCharacter{266F}{\ensuremath{\sharp}}
+\DeclareUnicodeCharacter{03BC}{\ensuremath{\mu}}
 
 \begin{document}
 
@@ -941,6 +943,9 @@ \section{Annex A. Simon Huber Canonical Equations}
 transpⁱ (Disc S A) φ (spoke f y j) = spoke (transpⁱ (S → Disc S A) φ f) (transpⁱ S φ y) j \\
 transpⁱ (ℑ A) φ (ℑ-unit a) = ℑ-unit (transpⁱ A φ a) \\
 transpⁱ (♭ A) φ (♭-unit a) = ♭-unit (transpⁱ A φ a) \\
+transpⁱ (♯ A) φ (♯-unit a) = ♯-unit (transpⁱ A φ a) \\
+transpⁱ (tw A) φ (tw-unit a) = tw-unit (transpⁱ A φ a) \\
+transpⁱ (Π (x :\textsubscript{μ} A), B) φ u₀ v = transpⁱ B[x/w] φ (u₀ w(i/0)) \\
 transp⁻ⁱ A φ u = (transpⁱ A(i/1−i) φ u)(i/1−i) : A(i/0) \\
 tFillⁱ A φ u₀ = transpʲ A(i/i∧j) (φ∨(i=0)) u₀ : A \\
 \\
@@ -953,7 +958,7 @@ \section{Annex A. Simon Huber Canonical Equations}
 hcompⁱ (Pathʲ A v w) [φ ↦ u] u₀ = 〈j〉\\
 \ hcompⁱ A [ φ ↦ u j, (j = 0) ↦ v, (j = 1) ↦ w ] (u₀ j) \\
 hcompⁱ G [ψ ↦ u] u₀ = glue [φ ↦ t₁] a₁ : G, G = Glue [φ ↦ (T,w)] A, \\
-t₁ = u(i/1) : T, a₁ = unglue u(i/1) : A, glue [φ ↦ t₁] a1 = t₁ : T \\
+t₁ = u(i/1) : T, a₁ = unglue u(i/1) : A, glue [φ ↦ t₁] a₁ = t₁ : T \\
 hcompⁱ (W (x : A), B) [φ ↦ sup a f] (sup a₀ f₀) \\
 \ = sup (hcompⁱ A [φ ↦ a] a₀) (hcompⁱ (B(v) → W) [φ ↦ f] f₀), v = hFillⁱ A [φ ↦ a] a₀ \\
 hcompⁱ (Coequ A B f g) [φ ↦ ι₂ u] (ι₂ u₀) = ι₂ (hcompⁱ B [φ ↦ u] u₀) \\
@@ -964,6 +969,9 @@ \section{Annex A. Simon Huber Canonical Equations}
 \ = spoke (hcompⁱ (S → Disc S A) [φ ↦ f] f₀) (hcompⁱ S [φ ↦ y] y₀) j \\
 hcompⁱ (ℑ A) [φ ↦ ℑ-unit u] (ℑ-unit u₀) = ℑ-unit (hcompⁱ A [φ ↦ u] u₀) \\
 hcompⁱ (♭ A) [φ ↦ ♭-unit u] (♭-unit u₀) = ♭-unit (hcompⁱ A [φ ↦ u] u₀) \\
+hcompⁱ (♯ A) [φ ↦ ♯-unit u] (♯-unit u₀) = ♯-unit (hcompⁱ A [φ ↦ u] u₀) \\
+hcompⁱ (tw A) [φ ↦ tw-unit u] (tw-unit u₀) = tw-unit (hcompⁱ A [φ ↦ u] u₀) \\
+hcompⁱ (Π (x :\textsubscript{μ} A), B) [φ ↦ u] u₀ v = hcompⁱ B[x/v] [φ ↦ u v] (u₀ v) \\
 hFillⁱ A [φ ↦ u] u₀ = hcompʲ A [φ ↦ u(i/i∧j), (i=0) ↦ u₀] u₀ : A \\
 \end{tabular}
 \end{table}