Skip to content

Commit 945b2fa

Browse files
authored
Update TRIPLES.md
1 parent 14f061f commit 945b2fa

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

intro/TRIPLES.md

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,9 @@ provides a logical foundation for interpreting these types in categorical models
4242

4343
<h2>2. Set-Theoretic Perspective: &Sigma; and Constructive Axiom of Choice</h2>
4444

45-
<p>In classical set theory, &Sigma; types naturally model the totality of relations by encoding dependent pairs (x, y) where y depends on x. This is crucial in constructive mathematics, where the axiom of choice does not hold unrestrictedly.</p>
45+
<p>In classical set theory, &Sigma; types naturally model the totality of relations by
46+
encoding dependent pairs (x, y) where y depends on x. This is crucial in constructive
47+
mathematics, where the axiom of choice does not hold unrestrictedly.</p>
4648

4749
<h2>3. Homotopical Perspective: &Pi; Types as Fiber Bundles</h2>
4850

@@ -52,7 +54,7 @@ provides a logical foundation for interpreting these types in categorical models
5254
<li>Given a fibration p: E &rarr; B, the &Sigma; type represents the total space E,
5355
while the &Pi; type represents the space of sections &Pi;<sub>x</sub> P(x),
5456
which generalizes function spaces in homotopy theory.</li>
55-
<li>The key homotopy-theoretic result is the isomorphism:<br> &Pi;<sub>x</sub> P(x) &cong; Hom(B, E)</li>
57+
<li>The key homotopy-theoretic result is the isomorphism: &Pi;<sub>x</sub> P(x) &cong; Hom(B, E)</li>
5658
</ul>
5759

5860
<h1>Identification setting</h1>

0 commit comments

Comments
 (0)