{- 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=0) -> base, (i=1) -> base ] data susp (A: U) = north | south | merid (a : A) [ (i=0) -> north, (i=1) -> south ] data sph = pt | surf [ (i=0) -> pt, (i=1) -> pt, (j=0) -> pt, (j=1) -> pt ] LOOP: U = Path S1 base base loopS1 : LOOP = 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 ( (PathP ( A) (u@i) (v@i))) r0 r1 plain (A: U) (x: A): I2 A x x x x ( x) ( x) ( x) ( x) = comp (<_>A) x [(i = 0) -> x, (i=1) -> x, (j = 0) -> x, (j=1) -> x ] loop2 : Path (Path sph pt pt) (pt) (pt) = plain sph pt loop3 : Path sph pt pt = loop2 @ 0 loopSph : Path (Path sph pt pt) (pt) (pt) = surf {sph} @ i @ j loop4 : Path sph pt pt = loopSph @ 1 loopEq : Path (Path (Path sph pt pt) (pt) (pt)) loop2 loopSph = undefined data D3 (x: sph) = bo (x: sph) | spc [ (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)) (bo pt) (bo pt) = (bo pt) loopD3 : Path (Path (Path (D3 pt) (bo pt) (bo pt)) (bo pt) (bo pt)) (loopD1) (loopD1) = spc {D3 pt} @ i @ j @ k