Skip to content

Commit

Permalink
Update syntax.tex
Browse files Browse the repository at this point in the history
  • Loading branch information
awodey committed Feb 5, 2025
1 parent 7679a49 commit 0868fba
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion blueprint/src/chapter/syntax.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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{Set}} \prod_{y : \text{S}} \text{Id}_{\text{Set}}(x,y) \simeq \Big(\text{El}(x) \cong \text{El}(y)\Big)$$
$$\text{UASet}: \prod_{x : \text{Set}} \prod_{y : \text{Set}} \text{Id}_{\text{Set}}(x,y) \cong \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)$$

0 comments on commit 0868fba

Please sign in to comment.