by writing the rotate equivalence more directly. The following code now takes 2s on my machine instead of 140s:
def winding2 (s : [i j] s2 [∂[i j] → base]) : int =
winding (λ j → coe 0 1 base in λ i → hopf (s i j))
def test10 : int =
winding2 (λ i j → comp 0 1 (surf i j) [i=0 k → surf j k | i=1 | ∂[j] → refl])
jonsterling
commented
5 years ago
by writing the rotate equivalence more directly. The following code now takes 2s on my machine instead of 140s: