{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Agda.Builtin.Nat
open import Agda.Builtin.Int

refl : ∀ {ℓ : Level} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x

_∙_ : ∀ {ℓ : Level} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {A = A} {x = x} p q i = hcomp (λ j → λ { (i = i0) → x ; (i = i1) → q j }) (p i)
infixr 80 _∙_

!_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
!_ p i = p (~ i)
infixr 100 !_

is-equiv = isEquiv

is-eq : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂}
  → (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x)
  → is-equiv f
is-eq {A = A} {B = B} f g f-g g-f = record {equiv-proof = λ b → (g b , f-g b) , lemma b} where
  postulate -- to keep this file small
    lemma : ∀ (b : B) (y : Σ A (λ a → f a ≡ b)) → (g b , f-g b) ≡ y

equiv : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂}
  → (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x)
  → A ≃ B
equiv {A = A} {B = B} f g f-g g-f = f , is-eq f g f-g g-f

-- J

J : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A} (B : (x' : A) → x ≡ x' → Type ℓ₂) (refl* : B x refl)
  {x' : A} (p : x ≡ x') → B x' p
J B refl* p = transp (λ i → B (p i) (λ j → p (i ∧ j))) i0 refl*

{- argument "x" was made explicit to make your life easier. -}
J-refl : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} (x : A) (B : (x' : A) → x ≡ x' → Type ℓ₂) (refl* : B x refl)
  → J B refl* refl ≡ refl*
J-refl x B refl* i = transp (λ _ → B _ refl) i refl*

-- univalence

id : ∀ {ℓ : Level} (A : Type ℓ) → A → A
id A x = x

id-is-equiv : ∀ {ℓ : Level} (A : Type ℓ) → is-equiv (id A)
equiv-proof (id-is-equiv A) x = ((x , refl) , λ z i → snd z (~ i) , λ j → snd z (~ i ∨ j))

id-equiv : ∀ {ℓ : Level} (A : Type ℓ) → A ≃ A
id-equiv A = id A , id-is-equiv A

ua : ∀ {ℓ : Level} {A B : Type ℓ} → A ≃ B → A ≡ B
ua {_} {A} {B} e i = Glue B (λ { (i = i0) → (A , e) ; (i = i1) → (B , id-equiv B) })

{- Part 1: the circle -}

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

-- This function maps integers to loops. The theorem is that it is an equivalence,
-- which means loops at base are equivalent to integers.
--
-- "loop^ 2" should be the concatenation of two copies of the constructor "loop".
--
-- There are many choices for the inductive cases, and you should pick the ones
-- that make the "loop^-pred" lemma easy to prove.
loop^ : Int → base ≡ base
loop^ (pos 0) = refl
loop^ (pos (suc n)) = loop^ (pos n) ∙ loop
loop^ (negsuc 0) = ! loop
loop^ (negsuc (suc n)) = loop^ (negsuc n) ∙ ! loop

{- Part 2: encoding the loop -}

-- We will first construct its inverse function, "winding", which maps loops back to
-- integers by counting their "winding numbers". The core trick is to generalize
-- the function to take paths from the base point, not just the loops at the base.
-- The generalization enables us to use the magical J to consider only the reflexivity case.

-- To do so, let's create a cloud over the circle for us to count the numbers.
-- The idea is to create a family of types, "Code", such that the number will bump up
-- when we go around the circle. (It is basically a helix.)

succ : Int → Int
succ (pos n) = pos (suc n)
succ (negsuc 0) = pos 0
succ (negsuc (suc n)) = negsuc n

pred : Int → Int
pred (pos (suc n)) = pos n
pred (pos 0) = negsuc 0
pred (negsuc n) = negsuc (suc n)

succ-pred : ∀ x → succ (pred x) ≡ x
succ-pred (pos (suc n)) = refl
succ-pred (pos 0) = refl
succ-pred (negsuc n) = refl

pred-succ : ∀ x → pred (succ x) ≡ x
pred-succ (pos n) = refl
pred-succ (negsuc 0) = refl
pred-succ (negsuc (suc n)) = refl

succ-equiv : Int ≃ Int
succ-equiv = equiv succ pred succ-pred pred-succ

-- "Code" is the helix, the universal covering of the circle.
Code : S¹ → Type₀
Code base = Int
Code (loop i) = ua succ-equiv i

-- This is the generalized function which takes paths from the base point.
encode : ∀ (x : S¹) → base ≡ x → Code x
encode _ = J (λ x _ → Code x) (pos 0)
        -- transp (λ i → Code (p i)) i0 (pos 0) also works

encode-refl : encode base refl ≡ pos 0
encode-refl = J-refl base (λ x _ → Code x) (pos 0)
           -- refl also works

-- This is the function we cares about.
winding : base ≡ base → Int
winding = encode base

{- Part 3: generalization of loop^ -}

-- We want to generalize loop^ to match the generalization of winding.

-- This is the most difficult task!
-- Hints: the intended solution uses "hfill" in more challenging branches.
loop^-pred : ∀ (n : Int) → (λ i → base ≡ loop i) [ loop^ (pred n) ≡ loop^ n ]
loop^-pred (pos zero) i j = loop (i ∨ ~ j)
loop^-pred (pos (suc n)) i j = hfill (λ k → λ { (j = i0) → base ; (j = i1) → loop k } ) (inS (loop^ (pos n) j)) i
loop^-pred (negsuc n) i j = hfill (λ k → λ { (j = i0) → base ; (j = i1) → loop (~ k) }) (inS (loop^ (negsuc n) j)) (~ i)

decode : ∀ (x : S¹) → Code x → base ≡ x
decode base n = loop^ n
decode (loop i) y j =
  -- studying the code could improve your understanding
  let succ-n = unglue (i ∨ ~ i) y in
  hcomp
    (λ k → λ { (i = i0) → loop^ (pred-succ y k) j -- we want to fix the zero side.
             ; (i = i1) → loop^ y j
             ; (j = i0) → base
             ; (j = i1) → loop i })
    (loop^-pred succ-n i j)

{- Part 5: loop^-winding -}

-- Now, you can use J to prove this after all the hard work.
decode-encode : ∀ (x : S¹) (p : base ≡ x) → decode x (encode x p) ≡ p
decode-encode x p = J (λ x p → decode x (encode x p) ≡ p) (λ i → decode base (encode-refl i)) p
                 -- J (λ x p → decode x (encode x p) ≡ p) (λ i → refl) p -- this also works

-- This is what we want.
loop^-winding : ∀ (l : base ≡ base) → loop^ (winding l) ≡ l
loop^-winding = decode-encode base

{- Part 5: winding-loop^ -}

-- We don't need to generalize the functions for the other direction.
winding-loop^ : ∀ (n : Int) → winding (loop^ n) ≡ n
winding-loop^ (pos 0) = refl
winding-loop^ (pos (suc n)) i = succ (winding-loop^ (pos n) i)
winding-loop^ (negsuc 0) = refl
winding-loop^ (negsuc (suc n)) i = pred (winding-loop^ (negsuc n) i)

-- ** Remember to remove all magic. **

{- Part 6: DONE! -}

theorem : (base ≡ base) ≃ Int
theorem = equiv winding loop^ winding-loop^ loop^-winding