headers for homotopy course

Author: 5HT

library/mathematics/homotopy/KGn.anders

@@ -1,3 +1,9 @@
+{- K(G,n): https://anders.groupoid.space/mathematics/homotopy/KGn/
+
+   - Eilenberg-MacLane spaces K(G,n).
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module KGn where
 import library/foundations/mltt/inductive
 import library/mathematics/algebra/algebra
@@ -44,7 +50,7 @@ def K1-ind (G : group) (P : K1 G → U)
               (2-quot-ind 𝟏 (R-K1 G) (Q-K1 G) (λ (x : 2-quot 𝟏 (R-K1 G) (Q-K1 G)), P (trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two x))
                           (λ (_ : 𝟏), pPoint)
                           (λ (_ _ : 𝟏) (g : G.1.1), pPath g)
-                          (λ (x y : 𝟏) (r1 r2 : R¯ 𝟏 (R-K1 G) x y) (q : Q-K1 G x y r1 r2), 
+                          (λ (x y : 𝟏) (r1 r2 : R¯ 𝟏 (R-K1 G) x y) (q : Q-K1 G x y r1 r2),
                               <i> PathP (<j> P (trunc₁ (2-quot 𝟏 (R-K1 G) (Q-K1 G)) two (2-quot₃ 𝟏 (R-K1 G) (Q-K1 G) x y r1 r2 q @ i @ j)))
                                         (pPath G.2.1.2.2.1 @ i) (pPath G.2.1.2.2.1 @ i)))
               nHub nSpoke z

library/mathematics/homotopy/S1.anders

@@ -1,3 +1,10 @@
+{- S^1: https://anders.groupoid.space/mathematics/homotopy/s1/
+   - S^1 Sphere (Circle).
+
+   HoTT 6.4 Circles and Spheres
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module S1 where
 import library/mathematics/homotopy/coequalizer
 import library/foundations/mltt/bool

library/mathematics/homotopy/Sn.anders

@@ -1,3 +1,9 @@
+{- n-Sphere: https://anders.groupoid.space/mathematics/homotopy/nsphere/
+
+   HoTT 6.4 Circles and Spheres
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module Sn where
 import library/foundations/mltt/nat
 import library/foundations/univalent/extensionality

library/mathematics/homotopy/coequalizer.anders

@@ -1,16 +1,8 @@
-{- Homotopy Type Theory:
-   - Coequalizer and Hubs/Spokes as primitives.
-   - S¹ sphere and 𝑛-sphere.
-   - Pushout.
-   - Suspension.
-   - 𝑛-Truncation.
+{- Coequalizer: https://anders.groupoid.space/mathematics/homotopy/coequalizer/
 
-   HoTT 6.8 Pushouts
-   HoTT 6.10 Quotients
-   HoTT 6.7 Hub and Spoke Disc
-   HoTT 6.9 Truncations
+   HoTT 6.12 The flattening lemma
 
-   Copyright (c) Groupoid Infinity, 2014-2022. -}
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
 
 module coequalizer where
 import library/foundations/univalent/equiv

library/mathematics/homotopy/colim.anders

@@ -1,3 +1,9 @@
+{- Colimit: https://anders.groupoid.space/mathematics/homotopy/colimit/
+
+   HoTT 7.4 Colimits of n-types
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module colimit where
 import library/foundations/mltt/nat
 import library/foundations/mltt/w

library/mathematics/homotopy/hs.anders

@@ -1,3 +1,10 @@
+{- Homotopy Type Theory:
+   - Coequalizer and Hubs/Spokes as primitives.
+
+   HoTT 6.7 Hub and Spoke Disc
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module hs where
 import library/foundations/univalent/path
 import library/foundations/univalent/equiv

library/mathematics/homotopy/loop.anders

@@ -4,7 +4,7 @@
    HoTT 8.1 0-Truncations Loop Space of Circle
    HoTT 8.4 Fiber Sequence and long exact sequence
 
-   Copyright (c) Groupoid Infinity, 2014-2026. -}
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
 
 module loop where
 import library/foundations/univalent/path

library/mathematics/homotopy/pullback.anders

@@ -2,7 +2,7 @@
 
    HoTT 2.15
 
-   Copyright (c) Groupoid Infinity, 2014-2022. -}
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
 
 module pullback where
 import library/foundations/univalent/path

library/mathematics/homotopy/pushout.anders

@@ -2,7 +2,7 @@
 
    HoTT 6.8 Pushouts
 
-   Copyright (c) Groupoid Infinity, 2014-2025. -}
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
 
 module pushout where
 import library/foundations/mltt/either

library/mathematics/homotopy/quotient.anders

@@ -1,3 +1,9 @@
+{- Quotient: https://anders.groupoid.space/mathematics/homotopy/quotient/
+
+   HoTT 6.10
+
+   Copyright (c) Groupoid Infinity, 2016-2026. -}
+
 module quotient where
 import library/foundations/univalent/path
 import library/mathematics/homotopy/coequalizer