We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 94e4c08 commit d8bc0a9Copy full SHA for d8bc0a9
intro/TRIPLES.md
@@ -22,7 +22,7 @@ while the Σ type models dependent pairs. Their interpretations extend into vari
22
branches of mathematics, each highlighting a distinct perspective on their structural role.
23
Below, we explore four such perspectives: categorical, set-theoretic, homotopical, and groupoidal.
24
25
-## 1. Categorical Perspective: Π and Σ as Adjunctions (Kock-Wright Interpretation)
+## 1. Categorical Perspective: Π and Σ as Adjunctions (Kock-Wraith Interpretation)
26
27
From a categorical viewpoint, Π and Σ types arise naturally through adjunctions.
28
The key idea is that dependent function types correspond to right adjoints,
0 commit comments