{-# OPTIONS --rewriting #-}

module Path where

open import Equality
open import EquationalReasoning
open import Function
open import FunctionExtensionality
open import Interval
open import Level
open import Product
open import Proposition
open import Sum
open import UIP

----------------------------------------------------------------------
-- Path types
----------------------------------------------------------------------
infix  _~_
data _~_ {ℓ : Level}{Γ : Set ℓ}: (x y : Γ) → Set ℓ where
  path : (f : 𝕀 → Γ) → f O ~ f I

infixl  _at_
_at_ : {ℓ : Level}{Γ : Set ℓ}{x y : Γ} → x ~ y → 𝕀 → Γ
path f at i = f i

atO :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ---------
  p at O ≡ x
atO (path _) = refl

atI :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ------------
  p at I ≡ y
atI (path _) = refl

{-# REWRITE atO atI #-}

----------------------------------------------------------------------
-- Bounded abstraction
----------------------------------------------------------------------
syntax path (λ i → x) = ⟨ i ⟩ x

~eta :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ----------------
  p ≡ ⟨ i ⟩ (p at i)
~eta (path _) = refl

-----------------------------------------------------------------------
-- Degenerate paths
----------------------------------------------------------------------
~refl : {ℓ : Level}{Γ : Set ℓ}(x : Γ) → x ~ x
~refl x = ⟨ _ ⟩ x

----------------------------------------------------------------------
-- Path congruence
----------------------------------------------------------------------
~cong :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  (γ : Γ → Δ)
  {x y : Γ}
  → ---------------
  x ~ y → γ x ~ γ y
~cong γ (path f) = path (γ ∘ f)

~congat :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  (γ : Γ → Δ)
  {x y : Γ}
  (p : x ~ y)
  → ---------------------------
  (~cong γ p) at_ ≡ γ ∘ (p at_)
~congat γ (path _) = refl

~congrefl :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  (γ : Γ → Δ)
  {x : Γ}
  → -----------------------------
  ~cong γ (~refl x) ≡ ~refl (γ x)
~congrefl _ = refl

~congid :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ------------
  ~cong id p ≡ p
~congid (path _) = refl

{-# REWRITE ~congid #-}

~cong∘ :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ}
  {Γ' : Set ℓ'}
  {Γ'' : Set ℓ''}
  (γ : Γ → Γ')
  (γ' : Γ' → Γ'')
  {x y : Γ}
  (p : x ~ y)
  → -------------------------------------
  ~cong γ' (~cong γ p) ≡ ~cong (γ' ∘ γ) p 
~cong∘ γ γ' (path _) = refl

{-# REWRITE ~cong∘ #-}
 
----------------------------------------------------------------------
-- Paths modulo ≡
----------------------------------------------------------------------
infix  _≡~≡_
_≡~≡_ : {ℓ : Level}{Γ : Set ℓ}(x y : Γ) → Set ℓ
_≡~≡_ {Γ = Γ} x y = Σ f ∈ (𝕀 → Γ), (f O ≡ x) × (f I ≡ y)

unpack : {ℓ : Level}{Γ : Set ℓ}{x y : Γ} → (x ~ y) → (x ≡~≡ y)
unpack (path f) = (f , refl , refl)

pack : {ℓ : Level}{Γ : Set ℓ}{x y : Γ} → (x ≡~≡ y) → (x ~ y)
pack (f , refl , refl) = path f

pack∘unpack :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → -----------------
  pack (unpack p) ≡ p
pack∘unpack (path _) = refl

packat :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ≡~≡ y)
  → -----------------
 (pack p) at_ ≡ fst p
packat (_ , refl , refl) = refl

fst∘unpack :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → --------------------
  fst (unpack p) ≡ p at_
fst∘unpack (path _) = refl

----------------------------------------------------------------------
-- Path extensionality
----------------------------------------------------------------------
atInj :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  {p q : x ~ y}
  → --------------------
  p at_ ≡ q at_ → p ≡ q
atInj {ℓ} {p = p} {q} u = 
  proof:
    p
  ≡[ symm (pack∘unpack p) ]
    pack (unpack p)
  ≡[ cong pack (Σext a (×ext {ℓ} {ℓ} uip uip)) ]
    pack (unpack q)
  ≡[ pack∘unpack q ]
    q
  qed
  where 
  a : fst (unpack p) ≡ fst (unpack q)
  a =
    proof:
      fst (unpack p)
    ≡[ fst∘unpack p ]
      p at_
    ≡[ u ]
      q at_
    ≡[ symm (fst∘unpack q) ]
      fst (unpack q)
    qed

~ext :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p q : x ~ y)
  (e : (i : 𝕀) → p at i ~ q at i)
  (e₀ : (i : 𝕀) → e O at i ≡ x)
  (e₁ : (i : 𝕀) → e I at i ≡ y)
  → -----------------------------
  p ~ q
~ext p q e e₀ e₁ =
  pack(
    (λ i → pack ((λ j → e j at i) , e₀ i , e₁ i)) ,
    (proof:
       pack ((λ j → p at j) , e₀ O , e₁ O)
     ≡[ cong₂ (λ u v → pack ((λ j → p at j) , u , v)) uip  uip ]
       pack ((λ j → p at j) , refl , refl)
     ≡[ symm (~eta p) ]
       p
     qed) ,
    ((proof:
       pack ((λ j → q at j) , e₀ I , e₁ I)
     ≡[ cong₂ (λ u v → pack ((λ j → q at j) , u , v)) uip  uip ]
       pack ((λ j → q at j) , refl , refl)
     ≡[ symm (~eta q) ]
       q
     qed)))

----------------------------------------------------------------------
-- Path composition
----------------------------------------------------------------------
{- abstract block used to speed up type-checking uses of path
composition -}
abstract 
  ~comp :
    {ℓ : Level}
    {Γ : Set ℓ}
    (f g : 𝕀 → Γ)
    (u : f I ≡ g O) 
    → -------------
    𝕀 → Γ
  ~comp f g u =
    𝕀ind
      (λ _ → _)
      (λ i _ → f (↑ i))
      (λ i _ → g (↓ i))
      (λ i v w →
        proof:
          f (↑ i)
        ≡[ cong f w ]
          f I
        ≡[ u ]
          g O
        ≡[ cong g (symm v) ]
          g (↓ i)
        qed)
    
  ~comp-l :
    {ℓ : Level}
    {Γ : Set ℓ}
    (f g : 𝕀 → Γ)
    (u : f I ≡ g O)
    (i : 𝕀)
    → -------------------------------
    ↓ i ≡ O → ~comp f g u i ≡ f (↑ i)
  ~comp-l f g u =
    𝕀ind↓
      (λ _ → _)
      (λ i _ → f (↑ i))
      (λ i _ → g (↓ i))
      (λ i v w →
        proof:
          f (↑ i)
        ≡[ cong f w ]
          f I
        ≡[ u ]
          g O
        ≡[ cong g (symm v) ]
          g (↓ i)
        qed)
  
  ~comp-r :
    {ℓ : Level}
    {Γ : Set ℓ}
    (f g : 𝕀 → Γ)
    (u : f I ≡ g O)
    (i : 𝕀)
    → -------------------------------
    ↑ i ≡ I → ~comp f g u i ≡ g (↓ i)
  ~comp-r f g u = 
    𝕀ind↑
      (λ _ → _)
      (λ i _ → f (↑ i))
      (λ i _ → g (↓ i))
      (λ i v w →
        proof:
          f (↑ i)
        ≡[ cong f w ]
          f I
        ≡[ u ]
          g O
        ≡[ cong g (symm v) ]
          g (↓ i)
        qed)  
  
  ~compO :
    {ℓ : Level}
    {Γ : Set ℓ}
    (f g : 𝕀 → Γ)
    (u : f I ≡ g O)
    → -----------------
    ~comp f g u O ≡ f O
  ~compO f g u = ~comp-l f g u O refl
  
  ~compI :
    {ℓ : Level}
    {Γ : Set ℓ}
    (f g : 𝕀 → Γ)
    (u : f I ≡ g O)
    → -----------------
    ~comp f g u I ≡ g I
  ~compI f g u = ~comp-r f g u I refl
-- end of abstract block

infixr  _∙_
_∙_ : {ℓ : Level}{Γ : Set ℓ}{x y z : Γ} → (y ~ z) → (x ~ y) → (x ~ z)
_∙_ q p =
  let
    f = p at_
    g = q at_
  in pack (~comp f g refl , ~compO f g refl , ~compI f g refl)

∙at :
 {ℓ : Level}
 {Γ : Set ℓ}
 {x y z : Γ}
 (q : y ~ z)
 (p : x ~ y)
 → --------------------------------------
 (q ∙ p) at_ ≡ ~comp (p at_) (q at_) refl
∙at q p =
  let
    f = p at_
    g = q at_
  in packat (~comp f g refl , ~compO f g refl , ~compI f g refl)

----------------------------------------------------------------------
-- Equational reasoning infrastructure for ~
----------------------------------------------------------------------
infix   path:_ 
path:_ :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  → -----------
  x ~ y → x ~ y
path: p = p

infixr  step~
step~ :
  {ℓ : Level}
  {Γ : Set ℓ}
  (x : Γ)
  {y z : Γ}
  → -------------------
  y ~ z → x ~ y → x ~ z
step~ _ = _∙_

syntax step~ x q p = x ~[ p ] q

infix   _endp 
_endp :
  {ℓ : Level}
  {Γ : Set ℓ}
  (x : Γ)
  → -------
  x ~ x
x endp = ~refl x

≡to~ :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  → -----------
  x ≡ y → x ~ y
≡to~ refl = ~refl _

----------------------------------------------------------------------
-- Paths in 𝕀
----------------------------------------------------------------------
infix  _to_
_to_ : (i j : 𝕀) → i ~ j
i to j = ⟨ k ⟩ cvx i k j

~𝕀uniq :
  {i j  : 𝕀}
  (p q : i ~ j)
  → -----------
  p ~ q
~𝕀uniq p q =
  ~ext
    p
    q
    (λ i → ⟨ j ⟩(cvx (p at i) j (q at i)))
    (λ _ → refl)
    (λ _ → refl)

----------------------------------------------------------------------
-- Path reversal
----------------------------------------------------------------------
~symm :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → --------
  y ~ x
~symm (path f) = ⟨ i ⟩ (f (rev i))

~symmrefl :
  {ℓ : Level}
  {A : Set ℓ}
  {x : A}
  → -----------------------
  ~symm (~refl x) ≡ ~refl x 
~symmrefl = refl 

~congsymm :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  {γ : Γ → Δ}
  {x y : Γ}
  (p : x ~ y)
  → -----------------------------------
  ~cong γ (~symm p) ≡ ~symm (~cong γ p)
~congsymm (path _) = atInj (funext (λ _ → refl))

~symmsymm :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → -----------------
  ~symm (~symm p) ~ p
~symmsymm (path f) =
  ~ext
    (⟨ i ⟩(f (rev (rev i))))
    (⟨ i ⟩(f i))
    (λ i → ~cong f (rev (rev i) to i))
    (λ _ → refl)
    (λ _ → refl)

----------------------------------------------------------------------
-- Path contraction
----------------------------------------------------------------------
infix  _upto_
_upto_ :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  (i : 𝕀)
  → ----------
  x ~ p at i
(path f) upto i = ~cong f (O to i)

uptoO :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ------------------
  (p upto O) ≡ ~refl x
uptoO (path f) = refl

uptoI :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ------------
  (p upto I) ≡ p
uptoI (path f) = refl

{-# REWRITE uptoO uptoI #-}

~reflupto :
 {ℓ : Level}
  {Γ : Set ℓ}
  (x : Γ)
  (i : 𝕀)
  → ----------------------
  ~refl x upto i ≡ ~refl x
~reflupto _ _ = refl

~contr :
  {ℓ : Level}
  {A : Set ℓ}
  {x y : A}
  (p : x ~ y)
  → ---------------------
  (x , ~refl x) ~ (y , p)
~contr p = ⟨ i ⟩(p at i , p upto i)

infix  _from_
_from_ :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  (i : 𝕀)
  → ----------
  p at i ~ y
path f from i = ~cong f (i to I)

fromO :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ----------
  p from O ≡ p
fromO (path f) = refl

fromI :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ----------------
  p from I ≡ ~refl y
fromI (path f) = refl

{-# REWRITE fromO fromI #-}

~reflfrom :
  {ℓ : Level}
  {Γ : Set ℓ}
  (x : Γ)
  (i : 𝕀)
  → ----------------------
  ~refl x from i ≡ ~refl x
~reflfrom _ _ = refl

----------------------------------------------------------------------
-- Properties of path composition
----------------------------------------------------------------------
∘~comp :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  (γ : Γ → Δ)
  (f g : 𝕀 → Γ)
  (u : f I ≡ g O)
  → --------------------------------------------------
  γ ∘ (~comp f g u) ≡ ~comp (γ ∘ f) (γ ∘ g) (cong γ u)
∘~comp γ f g u = funext (𝕀ind P h k (λ _ _ _ → uip))
  where
  P : 𝕀 → Set _
  P i = γ (~comp f g u i) ≡ ~comp (γ ∘ f) (γ ∘ g) (cong γ u) i

  h : (i : 𝕀) → ↓ i ≡ O → P i
  h i v =
    proof:
      γ (~comp f g u i)
    ≡[ cong γ (~comp-l f g u i v) ]
      γ (f (↑ i))
    ≡[ symm( ~comp-l (γ ∘ f) (γ ∘ g) (cong γ u) i v) ]
      ~comp (γ ∘ f) (γ ∘ g) (cong γ u) i
    qed

  k : (i : 𝕀) → ↑ i ≡ I → P i
  k i w = proof:
      γ (~comp f g u i)
    ≡[ cong γ (~comp-r f g u i w) ]
      γ (g (↓ i))
    ≡[ symm( ~comp-r (γ ∘ f) (γ ∘ g) (cong γ u) i w) ]
      ~comp (γ ∘ f) (γ ∘ g) (cong γ u) i
    qed

~cong∙ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {Δ : Set ℓ'}
  (γ : Γ → Δ)
  {x y z : Γ}
  (q : y ~ z)
  (p : x ~ y)
  → -----------------------------------------
  ~cong γ (q ∙ p) ≡ (~cong γ q) ∙ (~cong γ p)
~cong∙ γ q p = 
  let
    f = p at_
    g = q at_
  in atInj(
    proof:
      _at_ (~cong γ (q ∙ p))
    ≡[ ~congat γ (q ∙ p) ]
       γ ∘ ((q ∙ p) at_)
    ≡[ cong (γ ∘_) (∙at q p) ]
       γ ∘ (~comp f g refl)
    ≡[ ∘~comp γ f g refl ]
      ~comp (γ ∘ f) (γ ∘ g) refl
    ≡[ cong (λ{((f' , g') , u) → ~comp f' g' u})
       (Σext (×ext (symm (~congat γ p)) (symm (~congat γ q))) uip) ]
      ~comp ((~cong γ p) at_) ((~cong γ q) at_) refl
    ≡[ symm (∙at (~cong γ q) (~cong γ p)) ]
      _at_ (~cong γ q ∙ ~cong γ p)  
    qed)

∙refl :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ---------------
  p ~ p ∙ (~refl x)
∙refl (path f) =
  path:
    path f
  ~[ ≡to~ refl ]
    ~cong f (O to I)
  ~[ ~cong (~cong f) (~𝕀uniq (O to I) ((O to I) ∙ ~refl O)) ]
    ~cong f ((O to I) ∙ ~refl O)
  ~[ ≡to~ (~cong∙ f (O to I) (~refl O)) ]
    path f ∙ ~refl (f O)
  endp

refl∙ :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → ---------------
  p ~ (~refl y) ∙ p
refl∙ (path f) =
  path:
    path f
  ~[ ≡to~ refl ]
    ~cong f (O to I)
  ~[ ~cong (~cong f) (~𝕀uniq (O to I) (~refl I ∙ (O to I))) ]
    ~cong f (~refl I ∙ (O to I))
  ~[ ≡to~ (~cong∙ f (~refl I) (O to I)) ]
    ~refl (f I) ∙ path f
  endp

~invl :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → -------------------
  ~symm p ∙ p ~ ~refl x
~invl (path f) =
  path:
    ~symm (path f) ∙ path f
  ~[ ≡to~ (symm (~cong∙ f (⟨ i ⟩(rev i)) (⟨ i ⟩ i))) ]
    ~cong f ((⟨ i ⟩(rev i)) ∙ ⟨ i ⟩ i)
  ~[ ~cong (~cong f) (~𝕀uniq ((⟨ i ⟩(rev i)) ∙ ⟨ i ⟩ i) (~refl O)) ]    
    ~cong f (~refl O)
  ~[ ≡to~ refl ]
    ~refl (f O)
  endp

~invr :
  {ℓ : Level}
  {Γ : Set ℓ}
  {x y : Γ}
  (p : x ~ y)
  → -------------------
  p ∙ ~symm p ~ ~refl y
~invr (path f) =
  path:
    path f ∙ ~symm (path f)
  ~[ ≡to~ (symm (~cong∙ f (⟨ i ⟩ i) (⟨ i ⟩(rev i)))) ]
    ~cong f ((⟨ i ⟩ i) ∙ ⟨ i ⟩(rev i))
  ~[ ~cong (~cong f) (~𝕀uniq ((⟨ i ⟩ i) ∙ ⟨ i ⟩(rev i)) (~refl I)) ]    
    ~cong f (~refl I)
  ~[ ≡to~ refl ]
    ~refl (f I)
  endp

natural :
  {ℓ : Level}
  {Γ : Set ℓ}
  (γ δ : Γ → Γ)
  (φ : (x : Γ) → γ x ~ δ x)
  {x y : Γ}
  (p : x ~ y)
  → -------------------------------
  ~cong δ p ∙ φ x ~ φ y ∙ ~cong γ p
natural γ δ φ (path f) =
  path:
    path (δ ∘ f) ∙ φ (f O)
  ~[ ~cong (path (δ ∘ f) ∙_) (∙refl (φ (f O))) ]
    path (δ ∘ f) ∙ φ (f O) ∙ ~refl (γ (f O)) 
  ~[ ⟨ i ⟩(~cong (δ ∘ f) (i to I) ∙ φ (f i) ∙ ~cong (γ ∘ f) (O to i)) ]
    ~refl (δ (f I)) ∙ φ (f I) ∙ path (γ ∘ f)
  ~[ ~symm (refl∙ (φ (f I) ∙ path (γ ∘ f))) ]
    φ (f I) ∙ path (γ ∘ f)
  endp