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 ed94085 commit 60cd914
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 @@ -167,7 +167,7 @@
\textbf{The Set Universe}
$$\text{S} := \sum_{u : \text{U}} \text{isSet}(\text{El}(u))$$

\textbf{Type Isomorphism}
\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)$$

\textbf{Set Isomorphism}
Expand Down

0 comments on commit 60cd914

Please sign in to comment.