{-# 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

{-# REWRITE 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 = 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 = 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))

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 → Σ π

π₁ : ∀ {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)

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-β₂ #-}

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

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

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

uabeta : ∀ {u} {α β : Set u} (e : α ≃ β) (m : α) → trans (ua e) m ⇝ π₁ 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)