winding

intPosPart

def intPosPart (z : Int) : Nat

The non-negative part of an integer: k for pos k and zero for any negative integer.

intNegPart

def intNegPart (z : Int) : Nat

The negative part of an integer: k for negsucc k and zero for any non-negative integer.

intIsPos

def intIsPos (z : Int) : Type

Type family that is inhabited (Unit) exactly on non-negative integers and empty on negative ones.

posInj

def posInj (m : Nat) (n : Nat) (p : pos m ≡ pos n) : m ≡ n

Injectivity of pos: a path between pos m and pos n gives a path between m and n.

negsuccInj

def negsuccInj (m : Nat) (n : Nat) (p : negsucc m ≡ negsucc n) : m ≡ n

Injectivity of negsucc: a path between negsucc m and negsucc n gives a path between m and n.

posNeqNegsucc

def posNeqNegsucc (m : Nat) (n : Nat) (p : pos m ≡ negsucc n) : Empty

A non-negative integer is never path-equal to a negative one.

negsuccNeqPos

def negsuccNeqPos (m : Nat) (n : Nat) (p : negsucc m ≡ pos n) : Empty

A negative integer is never path-equal to a non-negative one.

isDiscreteInt

def isDiscreteInt (x : Int) (y : Int) : Dec (x ≡ y)

Path equality on Int is decidable.

isSetInt

def isSetInt : isSet Int

Int is a set (all its path types are propositions), by Hedberg’s theorem.

sucFiberPath

def sucFiberPath (b : Int) (fib : fiber Int Int Int.succ b) : Int.pred b ≡ fst fib

In any fiber of Int.succ over b, the point is path-equal to Int.pred b.

sucEquiv

def sucEquiv : Equiv Int Int

The successor on Int as an equivalence, with each fiber contractible around Int.pred b.

Code

def Code (x : S1) : Type

The universal cover (helix) of the circle: Int over base, with loop sent to the univalence path of sucEquiv.

winding

def winding (p : base ≡ base) : Int

Winding number of a loop at base, computed by transporting 0 along the helix.

windingRefl

theorem windingRefl : winding refl ≡ pos zero

The winding number of the constant loop is 0.

windingLoop

theorem windingLoop : winding loop ≡ pos (succ zero)

The winding number of loop is 1.

windingSymLoop

theorem windingSymLoop : winding (sym loop) ≡ negsucc zero

The winding number of the inverse loop is -1.

windingLoopLoop

theorem windingLoopLoop : winding (trans loop loop) ≡ pos (succ (succ zero))

The winding number of loop composed with itself is 2.