{- HIT:
   - 2-Sphere HIT.
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 6.4 Circles and spheres -}

module s2 where
import path
import proto

data S1 = base | loop <i> [ (i=0) -> base, (i=1) -> base ]
data susp (A: U) = north | south | merid (a : A) <i> [ (i=0) -> north, (i=1) -> south ]
data sph = pt | surf <i j> [ (i=0) -> pt, (i=1) -> pt, (j=0) -> pt, (j=1) -> pt ]

LOOP: U = Path S1 base base
loopS1 : LOOP = <i> loop {S1} @ i

S2: U = susp S1

I2 (A: U) (a0 a1 b0 b1: A) (u: Path A a0 a1) (v: Path A b0 b1)
      (r0: Path A a0 b0) (r1: Path A a1 b1) : U
      = PathP (<i> (PathP (<j> A) (u@i) (v@i))) r0 r1

plain (A: U) (x: A): I2 A x x x x (<i> x) (<i> x) (<i> x) (<i> x)
      = <i j> comp (<_>A) x [(i = 0) -> <i> x, (i=1) -> <i> x,
                             (j = 0) -> <i> x, (j=1) -> <i> x ]

loop2   : Path (Path sph pt pt) (<i>pt) (<i>pt) = plain sph pt
loop3   : Path sph pt pt = loop2 @ 0
loopSph : Path (Path sph pt pt) (<i>pt) (<i>pt) = <i j> surf {sph} @ i @ j
loop4   : Path sph pt pt = loopSph @ 1
loopEq  : Path (Path (Path sph pt pt) (<i>pt) (<i>pt)) loop2 loopSph = undefined

data D3 (x: sph) = bo (x: sph)
   | spc <i j k> [ (i=0) -> bo x, (i=1) -> bo x ,
                   (j=0) -> bo x, (j=1) -> bo x ,
                   (k=0) -> bo x, (k=1) -> bo x ]

loopD1  : Path (Path (D3 pt) (bo pt) (bo pt)) (<i>bo pt) (<i>bo pt) = <i>(<j>bo pt)
loopD3  : Path (Path (Path (D3 pt) (bo pt) (bo pt)) (<i>bo pt) (<i>bo pt)) (loopD1) (loopD1)
        = <i j k> spc {D3 pt} @ i @ j @ k