Merge branch 'main' of github.com:groupoid/anders

Author: 5HT

intro/TRIPLES.md

@@ -22,12 +22,12 @@ while the Σ type models dependent pairs. Their interpretations extend into vari
 branches of mathematics, each highlighting a distinct perspective on their structural role.
 Below, we explore four such perspectives: categorical, set-theoretic, homotopical, and groupoidal.
 
-## 1. Categorical Perspective: Π and Σ as Adjunctions (Kock-Wright Interpretation)
+## 1. Categorical Perspective: Π and Σ as Adjunctions (Kock-Wraith Interpretation)
 
 From a categorical viewpoint, Π and Σ types arise naturally through adjunctions.
 The key idea is that dependent function types correspond to right adjoints,
 while dependent sum types correspond to left adjoints. This perspective,
-pioneered by Kock-Wright, provides a logical foundation for interpreting
+pioneered by Kock-Wraith , provides a logical foundation for interpreting
 these types in categorical models of type theory.
 
 * The adjunctions can be explicitly formulated as triples (Σf ⊢ f* ⊢ Πf):