circlelib/circle.ktt

The circle, its universal cover, and winding numbers.

6 declarations, all certified by the kernel · source

1import int
2 
3✓data S1 : U := base | loop (i : I) [i = 0 -> base, i = 1 -> base]
4 
5✓def loopP : Path S1 base base := \i -> loop i
6 
7✓def helix : S1 -> U
8  | base => Int
9  | loop i => sucPathInt i
10 
11✓def winding (p : Path S1 base base) : Int := transport (\i -> helix (p i)) (pos zero)
12 
13✓def compS1 (p q : Path S1 base base) : Path S1 base base := trans p q
14 
15✓def invLoop : Path S1 base base := sym loopP