{-# OPTIONS --without-K --rewriting #-}

module Cubical where
open import Agda.Primitive

postulate
  _≡_ : ∀ {u} {α β : Set u} → α → β → Set u
{-# BUILTIN REWRITE _≡_ #-}

postulate
  I : Set lzero
  i₀ : I
  i₁ : I
  coe : ∀ {u} (i k : I) (π : I → Set u) → π i → π k
  coe-β₁ : ∀ {u} {π : I → Set u} (i : I) (x : π i) → coe i i π x ≡ x
  coe-β₂ : ∀ {u} {π : I → Set u} (i k : I) (x : π i) →
    coe k i π (coe i k π x) ≡ x
  coe-β₃ : ∀ {u} {β : Set u} (i k : I) (x : β) →
    coe i k (λ _ → β) x ≡ x

{-# REWRITE coe-β₁ coe-β₂ coe-β₃ #-}

data _⇝_ {u} {α : Set u} : α → α → Set u where
  lam : (f : I → α) → f i₀ ⇝ f i₁

_#_ : ∀ {u} {α : Set u} {a b : α} → a ⇝ b → I → α
_#_ (lam f) = f

postulate
  #-β₁ : ∀ {u} {α : Set u} {a b : α} (p : a ⇝ b) → (p # i₀) ≡ a
  #-β₂ : ∀ {u} {α : Set u} {a b : α} (p : a ⇝ b) → (p # i₁) ≡ b
  ⇝-η : ∀ {u} {α : Set u} {a b : α} (p : a ⇝ b) →
    lam (λ i → (p # i)) ≡ p

{-# REWRITE #-β₁ #-β₂ ⇝-η #-}

rfl : ∀ {u} {α : Set u} {a : α} → a ⇝ a
rfl {a = a} = lam (λ _ → a)

sym : ∀ {u} {α : Set u} {a b : α} → a ⇝ b → b ⇝ a
sym {b = b} p = coe i₁ i₀ (λ i → b ⇝ (p # i)) rfl

funext : ∀ {u v} {α : Set u} {β : α → Set v} {f g : (x : α) → β x}
  (p : (x : α) → f x ⇝ g x) → f ⇝ g
funext p = lam (λ i x → (p x # i))

cong : ∀ {u v} {α : Set u} {β : Set v} {a b : α} (f : α → β)
  (p : a ⇝ b) → f a ⇝  f b
cong f p = lam (λ i → f (p # i))

trans : ∀ {u} {α β : Set u} (p : α ⇝ β) → α → β
trans p = coe i₀ i₁ (λ i → p # i)

trans⁻¹ : ∀ {u} {α β : Set u} (p : α ⇝ β) → β → α
trans⁻¹ p = coe i₁ i₀ (λ i → p # i)

transK : ∀ {u} {α β : Set u} (p : α ⇝ β) (x : α) →
  x ⇝ trans⁻¹ p (trans p x)
transK p x = rfl --lam (λ i → coe i i₀ (λ i → p # i) (coe i₀ i (λ i → p # i) x))

trans⁻¹K : ∀ {u} {α β : Set u} (p : α ⇝ β) (x : β) →
  x ⇝ trans p (trans⁻¹ p x)
trans⁻¹K p x = rfl --sym (lam (λ i → coe i i₁ (λ i → p # i) (coe i₁ i (λ i → p # i) x)))

subst : ∀ {u v} {α : Set u} (π : α → Set v) {a b : α} (p : a ⇝ b) → π a → π b
subst π p = coe i₀ i₁ (λ i → π (p # i))

comp : ∀ {u} {α : Set u} {a b c : α} (p : a ⇝ b) (q : b ⇝ c) → a ⇝ c
comp p q = subst _ q p

postulate
  _∧_ : I → I → I
  ∧-β₁ : (i : I) → (i ∧ i₀) ≡ i₀
  ∧-β₂ : (i : I) → (i ∧ i₁) ≡ i
  ∧-β₃ : (i : I) → (i₀ ∧ i) ≡ i₀
  ∧-β₄ : (i : I) → (i₁ ∧ i) ≡ i

{-# REWRITE ∧-β₁ ∧-β₂ ∧-β₃ ∧-β₄ #-}

conn-and : ∀ {u} {α : Set u} {a b : α} (p : a ⇝ b) (i : I) → a ⇝ (p # i)
conn-and p i = lam (λ j → p # (i ∧ j))

J : ∀ {u v} {α : Set u} {a : α} {π : (b : α) → a ⇝ b → Set v}
  (h : π a rfl) (b : α) (p : a ⇝ b) → π b p
J {π = π} h b p = coe i₀ i₁ (λ i → π (p # i) (conn-and p i)) h

data Σ {u v} {α : Set u} (π : α → Set v) : Set (u ⊔ v) where
  _,_ : (x : α) → π x → Σ π

data _+_ {u v} (α : Set u) (β : Set v) : Set (u ⊔ v) where
  inl : α → α + β
  inr : β → α + β

data N : Set lzero where
  zero : N
  succ : N → N

{-# BUILTIN NATURAL N #-}

π₁ : ∀ {u v} {α : Set u} {π : α → Set v} → Σ π → α
π₁ (x , y) = x

_×_ : ∀ {u v} (α : Set u) (β : Set v) → Set (u ⊔ v)
α × β = Σ {α = α} (λ _ → β)

_~_ : ∀ {u v} {α : Set u} {π : α → Set v} (f g : (x : α) → π x) → Set (u ⊔ v)
_~_ {α = α} f g = (x : α) → f x ⇝ g x

id : ∀ {u} {α : Set u} → α → α
id x = x

seg : i₀ ⇝ i₁
seg = lam id

neg : I → I
neg i = sym seg # i

neg-β₁ : neg i₀ ⇝ i₁
neg-β₁ = rfl

neg-β₂ : neg i₁ ⇝ i₀
neg-β₂ = rfl

_∘_ : ∀ {u v} {α : Set u} {β : Set v} {φ : Set u} → (β → φ) → (α → β) → α → φ
(f ∘ g) x = f (g x)

linv : ∀ {u v} {α : Set u} {β : Set v} (f : α → β) → Set (u ⊔ v)
linv f = Σ (λ g → (g ∘ f) ~ id)

rinv : ∀ {u v} {α : Set u} {β : Set v} (f : α → β) → Set (u ⊔ v)
rinv f = Σ (λ g → (f ∘ g) ~ id)

biinv : ∀ {u v} {α : Set u} {β : Set v} (f : α → β) → Set (u ⊔ v)
biinv f = linv f × rinv f

_≃_ : ∀ {u v} (α : Set u) (β : Set v) → Set (u ⊔ v)
α ≃ β = Σ {α = α → β} (λ f → biinv f)

forward : ∀ {u v} {α : Set u} {β : Set v} (e : α ≃ β) → α → β
forward (f , _) = f

backward : ∀ {u v} {α : Set u} {β : Set v} (e : α ≃ β) → β → α
backward (_ , ((g , _) , _)) = g

postulate
  V : ∀ {u} (i : I) {α β : Set u} → α ≃ β → Set u
  V-β₁ : ∀ {u} {α β : Set u} (e : α ≃ β) → V i₀ e ≡ α
  V-β₂ : ∀ {u} {α β : Set u} (e : α ≃ β) → V i₁ e ≡ β

{-# REWRITE V-β₁ V-β₂ #-}

postulate
  V-β₃ : ∀ {u} {α β : Set u} (e : α ≃ β) (x : α) → coe i₀ i₁ (λ i → V i e) x ≡ forward e x
  V-β₄ : ∀ {u} {α β : Set u} (e : α ≃ β) (x : β) → coe i₁ i₀ (λ i → V i e) x ≡ backward e x
{-# REWRITE V-β₃ V-β₄ #-}

ua : ∀ {u} {α β : Set u} (e : α ≃ β) → α ⇝ β
ua e = lam (λ i → V i e)

Vproj : ∀ {u} (i : I) {α β : Set u} (e : α ≃ β) → α → V i e
Vproj i e m = coe i₀ i (λ i → V i e) m

uabeta : ∀ {u} {α β : Set u} (e : α ≃ β) (m : α) → trans (ua e) m ⇝ forward e m
uabeta e m = lam (λ i → coe i i₁ (λ i → ua e # i) (Vproj i e m))

I-ind : ∀ {u} (π : I → Set u) (p₀ : π i₀) (p₁ : π i₁)
  (p : (subst π seg p₀) ⇝ p₁) (i : I) → π i
I-ind π p₀ p₁ p i = coe i₁ i (λ j → π (seg # j)) (p # i)

I-ind-β₀ : ∀ {u} (π : I → Set u) (p₀ : π i₀) (p₁ : π i₁)
  (p : (subst π seg p₀) ⇝ p₁) → I-ind π p₀ p₁ p i₀ ⇝ p₀
I-ind-β₀ π p₀ p₁ p = rfl

I-ind-β₁ : ∀ {u} (π : I → Set u) (p₀ : π i₀) (p₁ : π i₁)
  (p : (subst π seg p₀) ⇝ p₁) → I-ind π p₀ p₁ p i₁ ⇝ p₁
I-ind-β₁ π p₀ p₁ p = rfl

postulate
  S¹ : Set lzero
  base : S¹
  loop : I → S¹

  loop-β₁ : loop i₀ ≡ base
  loop-β₂ : loop i₁ ≡ base

{-# REWRITE loop-β₁ loop-β₂ #-}

loopS¹ : base ⇝ base
loopS¹ = lam loop

postulate
  S¹-elim : ∀ {u} (π : S¹ → Set u) (b : π base) (l : subst π loopS¹ b ⇝ b) (u : S¹) → π u
  S¹-elim-β₁ : ∀ {u} {π : S¹ → Set u} (b : π base) (l : subst π loopS¹ b ⇝ b) → S¹-elim π b l base ≡ b
  S¹-elim-β₂ : ∀ {u} {π : S¹ → Set u} (b : π base) (l : subst π loopS¹ b ⇝ b) (i : I) → S¹-elim π b l (loop i) ≡ (l # i)

{-# REWRITE S¹-elim-β₁ S¹-elim-β₂ #-}

S¹-rec : ∀ {u} {β : Set u} (b : β) (l : b ⇝ b) → S¹ → β
S¹-rec {β = β} b l = S¹-elim (λ _ → β) b l

triv : base ⇝ base
triv = rfl

one-turn : (x : base ⇝ base) → base ⇝ base
one-turn x = comp x loopS¹

back-turn : (x : base ⇝ base) → base ⇝ base
back-turn x = comp x (sym loopS¹)

Z : Set lzero
Z = N + N

{- +2 = inr (succ (succ zero))
   +1 = inr (succ zero)
    0 = inr zero
   -1 = inl zero
   -2 = inl (succ zero) -}

succ-Z-aux : N → Z
succ-Z-aux zero = inr zero
succ-Z-aux (succ n) = inl n

succ-Z : Z → Z
succ-Z (inl u) = succ-Z-aux u
succ-Z (inr v) = inr (succ v)

pred-Z-aux : N → Z
pred-Z-aux zero = inl zero
pred-Z-aux (succ n) = inr n

pred-Z : Z → Z
pred-Z (inl u) = inl (succ u)
pred-Z (inr v) = pred-Z-aux v

succ-pred-inr-Z : (u : N) → succ-Z (pred-Z (inr u)) ⇝ inr u
succ-pred-inr-Z zero = rfl
succ-pred-inr-Z (succ u) = rfl

pred-succ-inl-Z : (u : N) → pred-Z (succ-Z (inl u)) ⇝ inl u
pred-succ-inl-Z zero = rfl
pred-succ-inl-Z (succ u) = rfl

succ-pred-Z : (u : Z) → succ-Z (pred-Z u) ⇝ u
succ-pred-Z (inl u) = rfl
succ-pred-Z (inr v) = succ-pred-inr-Z v

pred-succ-Z : (u : Z) → pred-Z (succ-Z u) ⇝ u
pred-succ-Z (inl u) = pred-succ-inl-Z u
pred-succ-Z (inr v) = rfl

succ-path-Z : Z ⇝ Z
succ-path-Z = ua (succ-Z , ((pred-Z , pred-succ-Z) , (pred-Z , succ-pred-Z)))

helix : S¹ → Set lzero
helix = S¹-rec Z succ-path-Z

minus-one-Z : Z
minus-one-Z = inl zero

zero-Z : Z
zero-Z = inr zero

winding : base ⇝ base → Z
winding x = trans (lam (λ i → helix (x # i))) zero-Z

one-Z : Z
one-Z = inr (succ zero)

test-one-Z : trans succ-path-Z zero-Z ⇝ one-Z
test-one-Z = rfl

test-minus-one-Z : trans⁻¹ succ-path-Z zero-Z ⇝ minus-one-Z
test-minus-one-Z = rfl