ℤ
Refl ≡ loop
flipPath
doubleCover
true≢false
cong
loopSpace loopSpace
ℕ ⊔ ℕ
Path≡⊔NoConfusion
rewind