From 7679a494f8ea95397970b9212f371a85ebe0e6b5 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Wed, 5 Feb 2025 16:07:04 -0500 Subject: [PATCH] update syntax --- blueprint/src/chapter/syntax.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/blueprint/src/chapter/syntax.tex b/blueprint/src/chapter/syntax.tex index 1558bd7..fc19a0f 100644 --- a/blueprint/src/chapter/syntax.tex +++ b/blueprint/src/chapter/syntax.tex @@ -165,7 +165,7 @@ \end{align*} \textbf{The Set Universe} -$$\text{S} := \sum_{u : \text{U}} \text{isSet}(\text{El}(u))$$ +$$\text{Set} := \sum_{u : \text{U}} \text{isSet}(\text{El}(u))$$ \textbf{Type Equivalence} $$A \simeq B := \sum_{f :A \to B}\sum_{g :B \to A}\sum_{h :B \to A}\Big(\prod_{a : A} \text{id}_{A}(g(f(a)),a) \Big) \times \Big(\prod_{b : B} \text{id}_{B}(f(h(b)),b) \Big)$$ @@ -177,7 +177,7 @@ $$\text{UA}: \prod_{x : \text{U}} \prod_{y : \text{U}} \text{Id}_{\text{U}}(x,y) \simeq \Big(\text{El}(x) \simeq \text{El}(y)\Big)$$ \textbf{The Univalence Axiom for Sets} -$$\text{UAset}: \prod_{x : \text{S}} \prod_{y : \text{S}} \text{Id}_{\text{S}}(x,y) \simeq \Big(\text{El}(x) \cong \text{El}(y)\Big)$$ +$$\text{UASet}: \prod_{x : \text{Set}} \prod_{y : \text{S}} \text{Id}_{\text{Set}}(x,y) \simeq \Big(\text{El}(x) \cong \text{El}(y)\Big)$$ \textbf{Function Extensionality} $$\text{FunExt}: \prod_{a : \text{U}} \prod_{b : \text{U}} \prod_{f : \text{El}(a) \to \text{El}(b)} \prod_{g : \text{El}(a) \to \text{El}(b)}\Big( \prod_{\alpha : \text{El}(a)}\text{id}_{\text{El(b)}}(f\alpha,g\alpha)\Big) \simeq \text{id}_{\text{El}(a) \to \text{El}(b)}(f,g)$$