open import Paths
open import Spaces::Sphere::S1::Core

def S¹-T³ (p : S¹) (q : S¹) (r : S¹) : T³
| base, base, base ⇒ base3
| loop i, base, base ⇒ line1 i
| base, loop i, base ⇒ line2 i
| base, base, loop i ⇒ line3 i
| base, loop i, loop j ⇒ face1 i j
| loop i, base, loop j ⇒ face2 i j
| loop i, loop j, base ⇒ face3 i j
| loop i, loop j, loop k ⇒ fill3 i j k

open data T³
| base3
| line1 : base3 = base3
| line2 : base3 = base3
| line3 : base3 = base3
| face1 (i j : I) { ∂ i := line3 j | ∂ j := line2 i }
| face2 (i j : I) { ∂ i := line3 j | ∂ j := line1 i }
| face3 (i j : I) { ∂ i := line2 j | ∂ j := line1 i }
| fill3 (i j k : I) {
  | ∂ i := face1 j k
  | ∂ j := face2 i k
  | ∂ k := face3 i j
}