{-# 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
infix 4 _~_
data _~_ {ℓ : Level}{Γ : Set ℓ}: (x y : Γ) → Set ℓ where
path : (f : 𝕀 → Γ) → f O ~ f I
infixl 6 _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 #-}
syntax path (λ i → x) = ⟨ i ⟩ x
~eta :
{ℓ : Level}
{Γ : Set ℓ}
{x y : Γ}
(p : x ~ y)
→
p ≡ ⟨ i ⟩ (p at i)
~eta (path _) = refl
~refl : {ℓ : Level}{Γ : Set ℓ}(x : Γ) → x ~ x
~refl x = ⟨ _ ⟩ x
~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∘ #-}
infix 4 _≡~≡_
_≡~≡_ : {ℓ : 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
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)))
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
infixr 5 _∙_
_∙_ : {ℓ : 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)
infix 1 path:_
path:_ :
{ℓ : Level}
{Γ : Set ℓ}
{x y : Γ}
→
x ~ y → x ~ y
path: p = p
infixr 2 step~
step~ :
{ℓ : Level}
{Γ : Set ℓ}
(x : Γ)
{y z : Γ}
→
y ~ z → x ~ y → x ~ z
step~ _ = _∙_
syntax step~ x q p = x ~[ p ] q
infix 3 _endp
_endp :
{ℓ : Level}
{Γ : Set ℓ}
(x : Γ)
→
x ~ x
x endp = ~refl x
≡to~ :
{ℓ : Level}
{Γ : Set ℓ}
{x y : Γ}
→
x ≡ y → x ~ y
≡to~ refl = ~refl _
infix 6 _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)
~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)
infix 6 _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 6 _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
∘~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