```{-

Definition of the circle as a HIT with a proof that Ω(S¹) ≡ ℤ

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.S1.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat
hiding (_+_ ; _*_ ; +-assoc ; +-comm)
open import Cubical.Data.Int

data S¹ : Type₀ where
base : S¹
loop : base ≡ base

-- Check that transp is the identity function for S¹
module _ where
transpS¹ : ∀ (φ : I) (u0 : S¹) → transp (λ _ → S¹) φ u0 ≡ u0
transpS¹ φ u0 = refl

compS1 : ∀ (φ : I) (u : ∀ i → Partial φ S¹) (u0 : S¹ [ φ ↦ u i0 ]) →
comp (λ _ → S¹) u (outS u0) ≡ hcomp u (outS u0)
compS1 φ u u0 = refl

helix : S¹ → Type₀
helix base     = Int
helix (loop i) = sucPathInt i

ΩS¹ : Type₀
ΩS¹ = base ≡ base

encode : ∀ x → base ≡ x → helix x
encode x p = subst helix p (pos zero)

winding : ΩS¹ → Int
winding = encode base

intLoop : Int → ΩS¹
intLoop (pos zero)       = refl
intLoop (pos (suc n))    = intLoop (pos n) ∙ loop
intLoop (negsuc zero)    = sym loop
intLoop (negsuc (suc n)) = intLoop (negsuc n) ∙ sym loop

decodeSquare : (n : Int) → PathP (λ i → base ≡ loop i) (intLoop (predInt n)) (intLoop n)
decodeSquare (pos zero) i j    = loop (i ∨ ~ j)
decodeSquare (pos (suc n)) i j = hfill (λ k → λ { (j = i0) → base
; (j = i1) → loop k } )
(inS (intLoop (pos n) j)) i
decodeSquare (negsuc n) i j = hcomp (λ k → λ { (i = i1) → intLoop (negsuc n) j
; (j = i0) → base
; (j = i1) → loop (i ∨ ~ k) })
(intLoop (negsuc n) j)

decode : (x : S¹) → helix x → base ≡ x
decode base         = intLoop
decode (loop i) y j =
let n : Int
n = unglue (i ∨ ~ i) y
in hcomp (λ k → λ { (i = i0) → intLoop (predSuc y k) j
; (i = i1) → intLoop y j
; (j = i0) → base
; (j = i1) → loop i })
(decodeSquare n i j)

decodeEncode : (x : S¹) (p : base ≡ x) → decode x (encode x p) ≡ p
decodeEncode x p = J (λ y q → decode y (encode y q) ≡ q) (λ _ → refl) p

isSetΩS¹ : isSet ΩS¹
isSetΩS¹ p q r s j i =
hcomp (λ k → λ { (i = i0) → decodeEncode base p k
; (i = i1) → decodeEncode base q k
; (j = i0) → decodeEncode base (r i) k
; (j = i1) → decodeEncode base (s i) k })
(decode base (isSetInt (winding p) (winding q) (cong winding r) (cong winding s) j i))

-- This proof does not rely on rewriting hcomp with empty systems in
-- Int as ghcomp has been implemented!
windingIntLoop : (n : Int) → winding (intLoop n) ≡ n
windingIntLoop (pos zero)       = refl
windingIntLoop (pos (suc n))    = cong sucInt (windingIntLoop (pos n))
windingIntLoop (negsuc zero)    = refl
windingIntLoop (negsuc (suc n)) = cong predInt (windingIntLoop (negsuc n))

ΩS¹≡Int : ΩS¹ ≡ Int
ΩS¹≡Int = isoToPath (iso winding intLoop windingIntLoop (decodeEncode base))

-- intLoop and winding are group homomorphisms
private
intLoop-sucInt : (z : Int) → intLoop (sucInt z) ≡ intLoop z ∙ loop
intLoop-sucInt (pos n)          = refl
intLoop-sucInt (negsuc zero)    = sym (lCancel loop)
intLoop-sucInt (negsuc (suc n)) =
rUnit (intLoop (negsuc n))
∙ (λ i → intLoop (negsuc n) ∙ lCancel loop (~ i))
∙ assoc (intLoop (negsuc n)) (sym loop) loop

intLoop-predInt : (z : Int) → intLoop (predInt z) ≡ intLoop z ∙ sym loop
intLoop-predInt (pos zero)    = lUnit (sym loop)
intLoop-predInt (pos (suc n)) =
rUnit (intLoop (pos n))
∙ (λ i → intLoop (pos n) ∙ (rCancel loop (~ i)))
∙ assoc (intLoop (pos n)) loop (sym loop)
intLoop-predInt (negsuc n)    = refl

intLoop-hom : (a b : Int) → (intLoop a) ∙ (intLoop b) ≡ intLoop (a + b)
intLoop-hom a (pos zero)       = sym (rUnit (intLoop a))
intLoop-hom a (pos (suc n))    =
assoc (intLoop a) (intLoop (pos n)) loop
∙ (λ i → (intLoop-hom a (pos n) i) ∙ loop)
∙ sym (intLoop-sucInt (a + pos n))
intLoop-hom a (negsuc zero)    = sym (intLoop-predInt a)
intLoop-hom a (negsuc (suc n)) =
assoc (intLoop a) (intLoop (negsuc n)) (sym loop)
∙ (λ i → (intLoop-hom a (negsuc n) i) ∙ (sym loop))
∙ sym (intLoop-predInt (a + negsuc n))

winding-hom : (a b : ΩS¹) → winding (a ∙ b) ≡ (winding a) + (winding b)
winding-hom a b i =
hcomp (λ t → λ { (i = i0) → winding (decodeEncode base a t ∙ decodeEncode base b t)
; (i = i1) → windingIntLoop (winding a + winding b) t })
(winding (intLoop-hom (winding a) (winding b) i))

-- Based homotopy group

basedΩS¹ : (x : S¹) → Type₀
basedΩS¹ x = x ≡ x

-- Proof that the homotopy group is actually independent on the basepoint
-- first, give a quasi-inverse to the basechange basedΩS¹→ΩS¹ for any loop i
-- (which does *not* match at endpoints)
private
ΩS¹→basedΩS¹-filler : I → I → ΩS¹ → I → S¹
ΩS¹→basedΩS¹-filler l i x j =
hfill (λ t → λ { (j = i0) → loop (i ∧ t)
; (j = i1) → loop (i ∧ t) })
(inS (x j)) l

basedΩS¹→ΩS¹-filler : (_ i : I) → basedΩS¹ (loop i) → I → S¹
basedΩS¹→ΩS¹-filler l i x j =
hfill (λ t → λ { (j = i0) → loop (i ∧ (~ t))
; (j = i1) → loop (i ∧ (~ t)) })
(inS (x j)) l

ΩS¹→basedΩS¹ : (i : I) → ΩS¹ → basedΩS¹ (loop i)
ΩS¹→basedΩS¹ i x j = ΩS¹→basedΩS¹-filler i1 i x j

basedΩS¹→ΩS¹ : (i : I) → basedΩS¹ (loop i) → ΩS¹
basedΩS¹→ΩS¹ i x j = basedΩS¹→ΩS¹-filler i1 i x j

basedΩS¹→ΩS¹→basedΩS¹ : (i : I) → (x : basedΩS¹ (loop i))
→ ΩS¹→basedΩS¹ i (basedΩS¹→ΩS¹ i x) ≡ x
basedΩS¹→ΩS¹→basedΩS¹ i x j k =
hcomp (λ t → λ { (j = i1) → basedΩS¹→ΩS¹-filler (~ t) i x k
; (j = i0) → ΩS¹→basedΩS¹ i (basedΩS¹→ΩS¹ i x) k
; (k = i0) → loop (i ∧ (t ∨ (~ j)))
; (k = i1) → loop (i ∧ (t ∨ (~ j))) })
(ΩS¹→basedΩS¹-filler (~ j) i (basedΩS¹→ΩS¹ i x) k)

ΩS¹→basedΩS¹→ΩS¹ : (i : I) → (x : ΩS¹)
→ basedΩS¹→ΩS¹ i (ΩS¹→basedΩS¹ i x) ≡ x
ΩS¹→basedΩS¹→ΩS¹ i x j k =
hcomp (λ t → λ { (j = i1) → ΩS¹→basedΩS¹-filler (~ t) i x k
; (j = i0) → basedΩS¹→ΩS¹ i (ΩS¹→basedΩS¹ i x) k
; (k = i0) → loop (i ∧ ((~ t) ∧ j))
; (k = i1) → loop (i ∧ ((~ t) ∧ j)) })
(basedΩS¹→ΩS¹-filler (~ j) i (ΩS¹→basedΩS¹ i x) k)

-- from the existence of our quasi-inverse, we deduce that the basechange is an equivalence
-- for all loop i

basedΩS¹→ΩS¹-isequiv : (i : I) → isEquiv (basedΩS¹→ΩS¹ i)
basedΩS¹→ΩS¹-isequiv i = isoToIsEquiv (iso (basedΩS¹→ΩS¹ i) (ΩS¹→basedΩS¹ i)
(ΩS¹→basedΩS¹→ΩS¹ i) (basedΩS¹→ΩS¹→basedΩS¹ i))

-- now extend the basechange so that both ends match
-- (and therefore we get a basechange for any x : S¹)

private
loop-conjugation : basedΩS¹→ΩS¹ i1 ≡ λ x → x
loop-conjugation i x =
let p = (doubleCompPath-elim loop x (sym loop))
∙ (λ i → (lUnit loop i ∙ x) ∙ sym loop)
in
((sym (decodeEncode base (basedΩS¹→ΩS¹ i1 x)))
∙ (λ t → intLoop (winding (p t)))
∙ (λ t → intLoop (winding-hom (intLoop (pos (suc zero)) ∙ x)
(intLoop (negsuc zero)) t))
∙ (λ t → intLoop ((winding-hom (intLoop (pos (suc zero))) x t)
+ (windingIntLoop (negsuc zero) t)))
∙ (λ t → intLoop (((windingIntLoop (pos (suc zero)) t) + (winding x)) + (negsuc zero)))
∙ (λ t → intLoop ((+-comm (pos (suc zero)) (winding x) t) + (negsuc zero)))
∙ (λ t → intLoop (+-assoc (winding x) (pos (suc zero)) (negsuc zero) (~ t)))
∙ (decodeEncode base x)) i

refl-conjugation : basedΩS¹→ΩS¹ i0 ≡ λ x → x
refl-conjugation i x j =
hfill (λ t → λ { (j = i0) → base
; (j = i1) → base })
(inS (x j)) (~ i)

basechange : (x : S¹) → basedΩS¹ x → ΩS¹
basechange base y = y
basechange (loop i) y =
hcomp (λ t → λ { (i = i0) → refl-conjugation t y
; (i = i1) → loop-conjugation t y })
(basedΩS¹→ΩS¹ i y)

-- for any loop i, the old basechange is equal to the new one
basedΩS¹→ΩS¹≡basechange : (i : I) → basedΩS¹→ΩS¹ i ≡ basechange (loop i)
basedΩS¹→ΩS¹≡basechange i j y =
hfill (λ t → λ { (i = i0) → refl-conjugation t y
; (i = i1) → loop-conjugation t y })
(inS (basedΩS¹→ΩS¹ i y)) j

-- so for any loop i, the extended basechange is an equivalence
basechange-isequiv-aux : (i : I) → isEquiv (basechange (loop i))
basechange-isequiv-aux i =
transport (λ j → isEquiv (basedΩS¹→ΩS¹≡basechange i j)) (basedΩS¹→ΩS¹-isequiv i)

-- as being an equivalence is contractible, basechange is an equivalence for all x : S¹
basechange-isequiv : (x : S¹) → isEquiv (basechange x)
basechange-isequiv base = basechange-isequiv-aux i0
basechange-isequiv (loop i) =
hcomp (λ t → λ { (i = i0) → basechange-isequiv-aux i0
; (i = i1) → isPropIsEquiv (basechange base) (basechange-isequiv-aux i1)
(basechange-isequiv-aux i0) t })
(basechange-isequiv-aux i)

basedΩS¹≡ΩS¹ : (x : S¹) → basedΩS¹ x ≡ ΩS¹
basedΩS¹≡ΩS¹ x = ua (basechange x , basechange-isequiv x)

basedΩS¹≡Int : (x : S¹) → basedΩS¹ x ≡ Int
basedΩS¹≡Int x = (basedΩS¹≡ΩS¹ x) ∙ ΩS¹≡Int

-- Some tests
module _ where
private
test-winding-pos : winding (intLoop (pos 5)) ≡ pos 5
test-winding-pos = refl

test-winding-neg : winding (intLoop (negsuc 5)) ≡ negsuc 5
test-winding-neg = refl

-- the inverse when S¹ is seen as a group

inv : S¹ → S¹
inv base = base
inv (loop i) = loop (~ i)

invInvolutive : section inv inv
invInvolutive base = refl
invInvolutive (loop i) = refl

invS¹Equiv : S¹ ≃ S¹
invS¹Equiv = isoToEquiv (iso inv inv invInvolutive invInvolutive)

invS¹Path : S¹ ≡ S¹
invS¹Path = ua invS¹Equiv

-- rot, used in the Hopf fibration

rotLoop : (a : S¹) → a ≡ a
rotLoop base       = loop
rotLoop (loop i) j =
hcomp (λ k → λ { (i = i0) → loop (j ∨ ~ k)
; (i = i1) → loop (j ∧ k)
; (j = i0) → loop (i ∨ ~ k)
; (j = i1) → loop (i ∧ k)}) base

rot : S¹ → S¹ → S¹
rot base x     = x
rot (loop i) x = rotLoop x i

_*_ : S¹ → S¹ → S¹
a * b = rot a b

infixl 30 _*_

-- rot i j = filler-rot i j i1
filler-rot : I → I → I → S¹
filler-rot i j = hfill (λ k → λ { (i = i0) → loop (j ∨ ~ k)
; (i = i1) → loop (j ∧ k)
; (j = i0) → loop (i ∨ ~ k)
; (j = i1) → loop (i ∧ k) }) (inS base)

isPropFamS¹ : ∀ {ℓ} (P : S¹ → Type ℓ) (pP : (x : S¹) → isProp (P x)) (b0 : P base) →
PathP (λ i → P (loop i)) b0 b0
isPropFamS¹ P pP b0 i = pP (loop i) (transp (λ j → P (loop (i ∧ j))) (~ i) b0)
(transp (λ j → P (loop (i ∨ ~ j))) i b0) i

rotIsEquiv : (a : S¹) → isEquiv (rot a)
rotIsEquiv base = idIsEquiv S¹
rotIsEquiv (loop i) = isPropFamS¹ (λ x → isEquiv (rot x))
(λ x → isPropIsEquiv (rot x))
(idIsEquiv _) i

-- more direct definition of the rot (loop i) equivalence

rotLoopInv : (a : S¹) → PathP (λ i → rotLoop (rotLoop a (~ i)) i ≡ a) refl refl
rotLoopInv a i j =
hcomp
(λ k → λ {
(i = i0) → a;
(i = i1) → rotLoop a (j ∧ ~ k);
(j = i0) → rotLoop (rotLoop a (~ i)) i;
(j = i1) → rotLoop a (i ∧ ~ k)})
(rotLoop (rotLoop a (~ i ∨ j)) i)

rotLoopEquiv : (i : I) → S¹ ≃ S¹
rotLoopEquiv i =
isoToEquiv
(iso (λ a → rotLoop a i)
(λ a → rotLoop a (~ i))
(λ a → rotLoopInv a i)
(λ a → rotLoopInv a (~ i)))

-- some cancellation laws, used in the Hopf fibration
private
rotInv-aux-1 : I → I → I → I → S¹
rotInv-aux-1 j k i =
hfill (λ l → λ { (k = i0) → (loop (i ∧ ~ l)) * loop j
; (k = i1) → loop j
; (i = i0) → (loop k * loop j) * loop (~ k)
; (i = i1) → loop (~ k ∧ ~ l) * loop j })
(inS ((loop (k ∨ i) * loop j) * loop (~ k)))

rotInv-aux-2 : I → I → I → S¹
rotInv-aux-2 i j k =
hcomp (λ l → λ { (k = i0) → inv (filler-rot (~ i) (~ j) l)
; (k = i1) → loop (j ∧ l)
; (i = i0) → filler-rot k j l
; (i = i1) → loop (j ∧ l)
; (j = i0) → loop (i ∨ k ∨ (~ l))
; (j = i1) → loop ((i ∨ k) ∧ l) })
(base)

rotInv-aux-3 : I → I → I → I → S¹
rotInv-aux-3 j k i =
hfill (λ l → λ { (k = i0) → rotInv-aux-2 i j l
; (k = i1) → loop j
; (i = i0) → loop (k ∨ l) * loop j
; (i = i1) → loop k * (inv (loop (~ j) * loop k)) })
(inS (loop k * (inv (loop (~ j) * loop (k ∨ ~ i)))))

rotInv-aux-4 : I → I → I → I → S¹
rotInv-aux-4 j k i =
hfill (λ l → λ { (k = i0) → rotInv-aux-2 i j l
; (k = i1) → loop j
; (i = i0) → loop j * loop (k ∨ l)
; (i = i1) → (inv (loop (~ j) * loop k)) * loop k })
(inS ((inv (loop (~ j) * loop (k ∨ ~ i))) * loop k))

rotInv-1 : (a b : S¹) → b * a * inv b ≡ a
rotInv-1 base base i = base
rotInv-1 base (loop k) i = rotInv-aux-1 i0 k i i1
rotInv-1 (loop j) base i = loop j
rotInv-1 (loop j) (loop k) i = rotInv-aux-1 j k i i1

rotInv-2 : (a b : S¹) → inv b * a * b ≡ a
rotInv-2 base base i = base
rotInv-2 base (loop k) i = rotInv-aux-1 i0 (~ k) i i1
rotInv-2 (loop j) base i = loop j
rotInv-2 (loop j) (loop k) i = rotInv-aux-1 j (~ k) i i1

rotInv-3 : (a b : S¹) → b * (inv (inv a * b)) ≡ a
rotInv-3 base base i = base
rotInv-3 base (loop k) i = rotInv-aux-3 i0 k (~ i) i1
rotInv-3 (loop j) base i = loop j
rotInv-3 (loop j) (loop k) i = rotInv-aux-3 j k (~ i) i1

rotInv-4 : (a b : S¹) → inv (b * inv a) * b ≡ a
rotInv-4 base base i = base
rotInv-4 base (loop k) i = rotInv-aux-4 i0 k (~ i) i1
rotInv-4 (loop j) base i = loop j
rotInv-4 (loop j) (loop k) i = rotInv-aux-4 j k (~ i) i1
```