Define T3

src/Homotopy/Torus/T3.ard

@@ -0,0 +1,47 @@
+\import Equiv
+\import Homotopy.Sphere.Circle
+\import Meta
+
+\data T3
+  | base3
+  | line1 : base3 = base3
+  | line2 : base3 = base3
+  | line3 : base3 = base3
+  | face1 I I \with { left, i => line3 i | right, i => line3 i | i, left => line2 i | i, right => line2 i }
+  | face2 I I \with { left, i => line3 i | right, i => line3 i | i, left => line1 i | i, right => line1 i }
+  | face3 I I \with { left, i => line2 i | right, i => line2 i | i, left => line1 i | i, right => line1 i }
+  | fill3 (i j k : I) \with {
+    | left, i, j => face1 i j
+    | right, i, j => face1 i j
+    | i, left, j => face2 i j
+    | i, right, j => face2 i j
+    | i, j, left => face3 i j
+    | i, j, right => face3 i j
+  }
+
+\func T3Sphere-equiv : QEquiv {T3} {\Sigma Sphere1 Sphere1 Sphere1} \cowith
+  | f => T3Sphere
+  | ret => SphereT3
+  | ret_f _ => mcases {T3Sphere} idp
+  | f_sec _ => mcases {SphereT3} idp
+  \where {
+    \func SphereT3 (_ : \Sigma Sphere1 Sphere1 Sphere1) : T3
+      | (base1, base1, base1) => base3
+      | (loop i, base1, base1) => line1 i
+      | (base1, loop i, base1) => line2 i
+      | (base1, base1, loop i) => line3 i
+      | (base1, loop i, loop j) => face1 i j
+      | (loop i, base1, loop j) => face2 i j
+      | (loop i, loop j, base1) => face3 i j
+      | (loop i, loop j, loop k) => fill3 i j k
+
+    \func T3Sphere (p : T3) : \Sigma Sphere1 Sphere1 Sphere1
+      | base3 => (base1, base1, base1)
+      | line1 i => (loop i, base1, base1)
+      | line2 i => (base1, loop i, base1)
+      | line3 i => (base1, base1, loop i)
+      | face1 i j => (base1, loop i, loop j)
+      | face2 i j => (loop i, base1, loop j)
+      | face3 i j => (loop i, loop j, base1)
+      | fill3 i j k => (loop i, loop j, loop k)
+  }