Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/RenSubFirstDraft.agda

Created September 24, 2017 23:05
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/6c5cfadba4d58670c905a0f5fdbadffe to your computer and use it in GitHub Desktop.
Save mietek/6c5cfadba4d58670c905a0f5fdbadffe to your computer and use it in GitHub Desktop.
Download ZIP
Raw
RenSubFirstDraft.agda
-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand
{-# OPTIONS --no-positivity-check #-}
module RenSubFirstDraft where
--------------------------------------------------------------------------------
--
-- 0. Prelude
-- open import Function public
-- using (_∘_ ; case_of_ ; flip)
-- open import Relation.Binary.PropositionalEquality public
-- using (_≡_ ; refl ; cong ; subst ; sym ; trans ; module ≡-Reasoning)
-- renaming (cong₂ to cong²)
_∘_ : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {P : X → Set ℓ′} {Q : ∀ {x} → P x → Set ℓ″}
→ (∀ {x} → (y : P x) → Q y) → (f : ∀ x → P x)
→ (∀ x → Q (f x))
(g ∘ f) x = g (f x)
case_of_ : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′}
→ X → (X → Y)
→ Y
case x of f = f x
flip : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : X → Y → Set ℓ″}
→ (∀ x y → Z x y)
→ (∀ y x → Z x y)
flip f y x = f x y
open import Agda.Builtin.Equality public
using (_≡_ ; refl)
-- {-# BUILTIN REWRITE _≡_ #-}
sym : ∀ {ℓ} → {X : Set ℓ} {x x′ : X}
→ x ≡ x′
→ x′ ≡ x
sym refl = refl
trans : ∀ {ℓ} → {X : Set ℓ} {x x′ x″ : X}
→ x ≡ x′ → x′ ≡ x″
→ x ≡ x″
trans refl refl = refl
subst : ∀ {ℓ ℓ′} → {X : Set ℓ}
→ (P : X → Set ℓ′) → ∀ {x x′} → x ≡ x′ → P x
→ P x′
subst P refl p = p
cong : ∀ {ℓ ℓ′} → {X : Set ℓ} {Y : Set ℓ′} {x x′ : X}
→ (f : X → Y) → x ≡ x′
→ f x ≡ f x′
cong f refl = refl
cong² : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {x x′ : X} {y y′ : Y}
→ (f : X → Y → Z) → x ≡ x′ → y ≡ y′
→ f x y ≡ f x′ y′
cong² f refl refl = refl
cong³ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {A : Set ℓ‴} {x x′ : X} {y y′ : Y} {z z′ : Z}
→ (f : X → Y → Z → A) → x ≡ x′ → y ≡ y′ → z ≡ z′
→ f x y z ≡ f x′ y′ z′
cong³ f refl refl refl = refl
module ≡-Reasoning {ℓ} {X : Set ℓ} where
infix 1 begin_
begin_ : ∀ {x x′ : X} → x ≡ x′ → x ≡ x′
begin p = p
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ (x {x′} : X) → x ≡ x′ → x ≡ x′
x ≡⟨⟩ p = p
infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ (x {x′ x″} : X) → x ≡ x′ → x′ ≡ x″ → x ≡ x″
x ≡⟨ p ⟩ q = trans p q
infix 3 _∎
_∎ : ∀ (x : X) → x ≡ x
x ∎ = refl
--------------------------------------------------------------------------------
--
-- 1. Syntax of the simply typed λ-calculus
-- Types
infixr 7 _⊃_
data 𝒯 : Set where
• : 𝒯
_⊃_ : (A B : 𝒯) → 𝒯
-- Contexts
data 𝒞 : Set where
[] : 𝒞
[_,_] : (Γ : 𝒞) (A : 𝒯) → 𝒞
-- Variables
infix 4 _∋_
data _∋_ : 𝒞 → 𝒯 → Set where
zero : ∀ {Γ A} → [ Γ , A ] ∋ A
suc : ∀ {Γ A B} → (i : Γ ∋ A)
→ [ Γ , B ] ∋ A
-- Terms
infix 3 _⊢_
data _⊢_ : 𝒞 → 𝒯 → Set where
` : ∀ {Γ A} → (i : Γ ∋ A)
→ Γ ⊢ A
ƛ : ∀ {Γ A B} → (M : [ Γ , A ] ⊢ B)
→ Γ ⊢ A ⊃ B
_∙_ : ∀ {Γ A B} → (M : Γ ⊢ A ⊃ B) (N : Γ ⊢ A)
→ Γ ⊢ B
--------------------------------------------------------------------------------
--
-- 2. Renamings
infix 4 _∋⋆_
data _∋⋆_ : 𝒞 → 𝒞 → Set where
[] : ∀ {Γ} → Γ ∋⋆ []
[_,_] : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ) (i : Δ ∋ A)
→ Δ ∋⋆ [ Γ , A ]
putᵣ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
→ Δ ∋⋆ Γ
putᵣ {[]} f = []
putᵣ {[ Γ , A ]} f = [ putᵣ (λ i → f (suc i)) , f zero ]
getᵣ : ∀ {Γ Δ A} → Δ ∋⋆ Γ → Γ ∋ A
→ Δ ∋ A
getᵣ [ η , i ] zero = i
getᵣ [ η , i ] (suc j) = getᵣ η j
unwkᵣ : ∀ {Γ Δ A} → Δ ∋⋆ [ Γ , A ]
→ Δ ∋⋆ Γ
unwkᵣ [ η , i ] = η
wkᵣ : ∀ {A Γ Δ} → Δ ∋⋆ Γ
→ [ Δ , A ] ∋⋆ Γ
wkᵣ [] = []
wkᵣ [ η , i ] = [ wkᵣ η , suc i ]
liftᵣ : ∀ {A Γ Δ} → Δ ∋⋆ Γ
→ [ Δ , A ] ∋⋆ [ Γ , A ]
liftᵣ η = [ wkᵣ η , zero ]
idᵣ : ∀ {Γ} → Γ ∋⋆ Γ
idᵣ {[]} = []
idᵣ {[ Γ , A ]} = liftᵣ idᵣ
ren : ∀ {Γ Δ A} → Δ ∋⋆ Γ → Γ ⊢ A
→ Δ ⊢ A
ren η (` i) = ` (getᵣ η i)
ren η (ƛ M) = ƛ (ren (liftᵣ η) M)
ren η (M ∙ N) = ren η M ∙ ren η N
wk : ∀ {C Γ A} → Γ ⊢ A
→ [ Γ , C ] ⊢ A
wk M = ren (wkᵣ idᵣ) M
-- Composition of renamings
-- NOTE: _○_ = getᵣ⋆
_○_ : ∀ {Γ Δ Ξ} → Δ ∋⋆ Γ → Γ ∋⋆ Ξ
→ Δ ∋⋆ Ξ
η₁ ○ [] = []
η₁ ○ [ η₂ , i ] = [ η₁ ○ η₂ , getᵣ η₁ i ]
--------------------------------------------------------------------------------
--
-- 2.1. Properties of renamings
module _ where
open ≡-Reasoning
wkgetᵣ : ∀ {C Γ Δ A} → (η : Δ ∋⋆ Γ) (i : Γ ∋ A)
→ getᵣ (wkᵣ {C} η) i ≡ suc (getᵣ η i)
wkgetᵣ [ η , j ] zero = refl
wkgetᵣ [ η , j ] (suc i) = wkgetᵣ η i
liftgetᵣ : ∀ {C Γ Δ A} → (η : Δ ∋⋆ Γ) (i : Γ ∋ A)
→ getᵣ (liftᵣ {C} η) (suc i) ≡ suc (getᵣ η i)
liftgetᵣ η i = wkgetᵣ η i
idgetᵣ : ∀ {Γ A} → (i : Γ ∋ A)
→ getᵣ idᵣ i ≡ i
idgetᵣ zero = refl
idgetᵣ (suc i) = begin
getᵣ (wkᵣ idᵣ) i ≡⟨ wkgetᵣ idᵣ i ⟩
suc (getᵣ idᵣ i) ≡⟨ cong suc (idgetᵣ i) ⟩
suc i ∎
idren : ∀ {Γ A} → (M : Γ ⊢ A)
→ ren idᵣ M ≡ M
idren (` i) = cong ` (idgetᵣ i)
idren (ƛ M) = cong ƛ (idren M)
idren (M ∙ N) = cong² _∙_ (idren M) (idren N)
--------------------------------------------------------------------------------
--
-- 3. Substitutions
data _⊢⋆_ : 𝒞 → 𝒞 → Set where
[] : ∀ {Γ} → Γ ⊢⋆ []
[_,_] : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ) (M : Δ ⊢ A)
→ Δ ⊢⋆ [ Γ , A ]
putₛ : ∀ {Γ Δ} → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
→ Δ ⊢⋆ Γ
putₛ {[]} f = []
putₛ {[ Γ , A ]} f = [ putₛ (λ M → f (wk M)) , f (` zero) ]
getₛ : ∀ {Γ Δ A} → Δ ⊢⋆ Γ → Γ ∋ A
→ Δ ⊢ A
getₛ [ σ , M ] zero = M
getₛ [ σ , M ] (suc i) = getₛ σ i
unwkₛ : ∀ {Γ Δ A} → Δ ⊢⋆ [ Γ , A ]
→ Δ ⊢⋆ Γ
unwkₛ [ σ , M ] = σ
wkₛ : ∀ {A Γ Δ} → Δ ⊢⋆ Γ
→ [ Δ , A ] ⊢⋆ Γ
wkₛ [] = []
wkₛ [ σ , M ] = [ wkₛ σ , wk M ]
liftₛ : ∀ {A Γ Δ} → Δ ⊢⋆ Γ
→ [ Δ , A ] ⊢⋆ [ Γ , A ]
liftₛ σ = [ wkₛ σ , ` zero ]
idₛ : ∀ {Γ} → Γ ⊢⋆ Γ
idₛ {[]} = []
idₛ {[ Γ , A ]} = liftₛ idₛ
sub : ∀ {Γ Δ A} → Δ ⊢⋆ Γ → Γ ⊢ A
→ Δ ⊢ A
sub σ (` i) = getₛ σ i
sub σ (ƛ M) = ƛ (sub (liftₛ σ) M)
sub σ (M ∙ N) = sub σ M ∙ sub σ N
cut : ∀ {Γ A B} → [ Γ , A ] ⊢ B → Γ ⊢ A
→ Γ ⊢ B
cut M N = sub [ idₛ , N ] M
-- Composition of substitutions
-- NOTE: _●_ = sub⋆
_●_ : ∀ {Γ Δ Ξ} → Δ ⊢⋆ Γ → Γ ⊢⋆ Ξ
→ Δ ⊢⋆ Ξ
σ₁ ● [] = []
σ₁ ● [ σ₂ , M ] = [ σ₁ ● σ₂ , sub σ₁ M ]
--------------------------------------------------------------------------------
--
-- 3.1. Properties of substitutions
module _ where
open ≡-Reasoning
wkgetₛ : ∀ {C Γ Δ A} → (σ : Δ ⊢⋆ Γ) (i : Γ ∋ A)
→ getₛ (wkₛ {C} σ) i ≡ wk (getₛ σ i)
wkgetₛ [ σ , M ] zero = refl
wkgetₛ [ σ , M ] (suc i) = wkgetₛ σ i
liftgetₛ : ∀ {C Γ Δ A} → (σ : Δ ⊢⋆ Γ) (i : Γ ∋ A)
→ getₛ (liftₛ {C} σ) (suc i) ≡ wk (getₛ σ i)
liftgetₛ σ i = wkgetₛ σ i
idgetₛ : ∀ {Γ A} → (i : Γ ∋ A)
→ getₛ idₛ i ≡ ` i
idgetₛ zero = refl
idgetₛ (suc i) = begin
getₛ (wkₛ idₛ) i ≡⟨ wkgetₛ idₛ i ⟩
wk (getₛ idₛ i) ≡⟨ cong wk (idgetₛ i) ⟩
wk (` i) ≡⟨⟩
` (getᵣ (wkᵣ idᵣ) i) ≡⟨ cong ` (wkgetᵣ idᵣ i) ⟩
` (suc (getᵣ idᵣ i)) ≡⟨ cong ` (cong suc (idgetᵣ i)) ⟩
` (suc i) ∎
idsub : ∀ {Γ A} → (M : Γ ⊢ A)
→ sub idₛ M ≡ M
idsub (` i) = idgetₛ i
idsub (ƛ M) = cong ƛ (idsub M)
idsub (M ∙ N) = cong² _∙_ (idsub M) (idsub N)
--------------------------------------------------------------------------------
--
-- 4. Compositions of renaming and substitution
⌊_⌋ : ∀ {Γ Δ} → Δ ∋⋆ Γ → Δ ⊢⋆ Γ
⌊ [] ⌋ = []
⌊ [ η , i ] ⌋ = [ ⌊ η ⌋ , ` i ]
module _ where
open ≡-Reasoning
⌊get⌋ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ) (i : Γ ∋ A)
→ getₛ ⌊ η ⌋ i ≡ ` (getᵣ η i)
⌊get⌋ [ η , j ] zero = refl
⌊get⌋ [ η , j ] (suc i) = ⌊get⌋ η i
⌊wk⌋ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ)
→ wkₛ {A} ⌊ η ⌋ ≡ ⌊ wkᵣ η ⌋
⌊wk⌋ [] = refl
⌊wk⌋ [ η , i ] = begin
[ wkₛ ⌊ η ⌋ , ` (getᵣ (wkᵣ idᵣ) i) ] ≡⟨ cong² [_,_] refl (cong ` (wkgetᵣ idᵣ i)) ⟩
[ wkₛ ⌊ η ⌋ , ` (suc (getᵣ idᵣ i)) ] ≡⟨ cong² [_,_] (⌊wk⌋ η) (cong ` (cong suc (idgetᵣ i))) ⟩
[ ⌊ wkᵣ η ⌋ , ` (suc i) ] ∎
⌊lift⌋ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ)
→ liftₛ {A} ⌊ η ⌋ ≡ ⌊ liftᵣ η ⌋
⌊lift⌋ η = cong² [_,_] (⌊wk⌋ η) refl
⌊id⌋ : ∀ {Γ} → idₛ {Γ} ≡ ⌊ idᵣ ⌋
⌊id⌋ {[]} = refl
⌊id⌋ {[ Γ , A ]} = begin
[ wkₛ idₛ , ` zero ] ≡⟨ cong² [_,_] (cong wkₛ ⌊id⌋) refl ⟩
[ wkₛ ⌊ idᵣ ⌋ , ` zero ] ≡⟨ cong² [_,_] (⌊wk⌋ idᵣ) refl ⟩
[ ⌊ wkᵣ idᵣ ⌋ , ` zero ] ∎
⌊sub⌋ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ) (M : Γ ⊢ A)
→ sub ⌊ η ⌋ M ≡ ren η M
⌊sub⌋ η (` i) = ⌊get⌋ η i
⌊sub⌋ η (ƛ M) = begin
ƛ (sub (liftₛ ⌊ η ⌋) M) ≡⟨ cong ƛ (cong² sub (⌊lift⌋ η) (refl {x = M})) ⟩
ƛ (sub ⌊ liftᵣ η ⌋ M) ≡⟨ cong ƛ (⌊sub⌋ (liftᵣ η) M) ⟩
ƛ (ren (liftᵣ η) M) ∎
⌊sub⌋ η (M ∙ N) = cong² _∙_ (⌊sub⌋ η M) (⌊sub⌋ η N)
⌊○⌋ : ∀ {Γ Δ Ξ} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ)
→ ⌊ η₁ ○ η₂ ⌋ ≡ ⌊ η₁ ⌋ ● ⌊ η₂ ⌋
⌊○⌋ η₁ [] = refl
⌊○⌋ η₁ [ η₂ , i ] = cong² [_,_] (⌊○⌋ η₁ η₂) (sym (⌊get⌋ η₁ i))
-- Composition of substitution and renaming
-- NOTE: _◐_ = getₛ⋆
_◐_ : ∀ {Γ Δ Ξ} → Δ ⊢⋆ Γ → Γ ∋⋆ Ξ
→ Δ ⊢⋆ Ξ
σ ◐ η = σ ● ⌊ η ⌋
-- Composition of renaming and substitution
-- NOTE: _◑_ = ren⋆
_◑_ : ∀ {Γ Δ Ξ} → Δ ∋⋆ Γ → Γ ⊢⋆ Ξ
→ Δ ⊢⋆ Ξ
η ◑ σ = ⌊ η ⌋ ● σ
--------------------------------------------------------------------------------
--
-- 4.1. Basic properties of _◌_
module _ where
open ≡-Reasoning
zap○ : ∀ {Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (i : Δ ∋ A)
→ [ η₁ , i ] ○ wkᵣ η₂ ≡ η₁ ○ η₂
zap○ η₁ [] i = refl
zap○ η₁ [ η₂ , j ] i = cong² [_,_] (zap○ η₁ η₂ i) refl
id₁○ : ∀ {Γ Δ} → (η : Δ ∋⋆ Γ)
→ idᵣ ○ η ≡ η
id₁○ [] = refl
id₁○ [ η , i ] = cong² [_,_] (id₁○ η) (idgetᵣ i)
id₂○ : ∀ {Γ Δ} → (η : Δ ∋⋆ Γ)
→ η ○ idᵣ ≡ η
id₂○ {[]} [] = refl
id₂○ {[ Δ , A ]} [ η , i ] = begin
[ [ η , i ] ○ wkᵣ idᵣ , i ] ≡⟨ cong² [_,_] (zap○ η idᵣ i) refl ⟩
[ η ○ idᵣ , i ] ≡⟨ cong² [_,_] (id₂○ η) refl ⟩
[ η , i ] ∎
--------------------------------------------------------------------------------
--
-- 4.2. Basic properties of _◐_
module _ where
open ≡-Reasoning
zap◐ : ∀ {Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (M : Δ ⊢ A)
→ [ σ , M ] ◐ wkᵣ η ≡ σ ◐ η
zap◐ σ [] M = refl
zap◐ σ [ η , i ] M = cong² [_,_] (zap◐ σ η M) refl
id₂◐ : ∀ {Γ Δ} → (σ : Δ ⊢⋆ Γ)
→ σ ◐ idᵣ ≡ σ
id₂◐ [] = refl
id₂◐ [ σ , M ] = begin
[ [ σ , M ] ◐ wkᵣ idᵣ , M ] ≡⟨ cong² [_,_] (zap◐ σ idᵣ M) refl ⟩
[ σ ◐ idᵣ , M ] ≡⟨ cong² [_,_] (id₂◐ σ) refl ⟩
[ σ , M ] ∎
--------------------------------------------------------------------------------
--
-- 4.3. Advanced properties of _○_
module _ where
open ≡-Reasoning
get○ : ∀ {Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (i : Ξ ∋ A)
→ getᵣ (η₁ ○ η₂) i ≡ (getᵣ η₁ ∘ getᵣ η₂) i
get○ η₁ [ η₂ , j ] zero = refl
get○ η₁ [ η₂ , j ] (suc i) = get○ η₁ η₂ i
wk○ : ∀ {Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ)
→ wkᵣ {A} (η₁ ○ η₂) ≡ wkᵣ η₁ ○ η₂
wk○ η₁ [] = refl
wk○ η₁ [ η₂ , i ] = cong² [_,_] (wk○ η₁ η₂) (sym (wkgetᵣ η₁ i))
lift○ : ∀ {Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ)
→ liftᵣ {A} (η₁ ○ η₂) ≡ liftᵣ η₁ ○ liftᵣ η₂
lift○ η₁ η₂ = begin
liftᵣ (η₁ ○ η₂) ≡⟨ cong² [_,_] (wk○ η₁ η₂) refl ⟩
[ wkᵣ η₁ ○ η₂ , zero ] ≡⟨ cong² [_,_] (sym (zap○ (wkᵣ η₁) η₂ zero)) refl ⟩
[ [ wkᵣ η₁ , zero ] ○ wkᵣ η₂ , zero ] ∎
wkid₁○ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ)
→ wkᵣ {A} idᵣ ○ η ≡ wkᵣ η
wkid₁○ η = begin
wkᵣ idᵣ ○ η ≡⟨ sym (wk○ idᵣ η) ⟩
wkᵣ (idᵣ ○ η) ≡⟨ cong wkᵣ (id₁○ η) ⟩
wkᵣ η ∎
wkid₂○ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ)
→ wkᵣ {A} η ○ idᵣ ≡ wkᵣ η
wkid₂○ η = begin
wkᵣ η ○ idᵣ ≡⟨ sym (wk○ η idᵣ) ⟩
wkᵣ (η ○ idᵣ) ≡⟨ cong wkᵣ (id₂○ η) ⟩
wkᵣ η ∎
liftwkid₂○ : ∀ {Γ Δ A} → (η : Δ ∋⋆ Γ)
→ liftᵣ {A} η ○ wkᵣ idᵣ ≡ wkᵣ η
liftwkid₂○ η = begin
[ wkᵣ η , zero ] ○ wkᵣ idᵣ ≡⟨ zap○ (wkᵣ η) idᵣ zero ⟩
wkᵣ η ○ idᵣ ≡⟨ wkid₂○ η ⟩
wkᵣ η ∎
ren○ : ∀ {Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ ren (η₁ ○ η₂) M ≡ (ren η₁ ∘ ren η₂) M
ren○ η₁ η₂ (` i) = cong ` (get○ η₁ η₂ i)
ren○ η₁ η₂ (ƛ M) = begin
ƛ (ren (liftᵣ (η₁ ○ η₂)) M) ≡⟨ cong ƛ (cong² ren (lift○ η₁ η₂) refl) ⟩
ƛ (ren (liftᵣ η₁ ○ liftᵣ η₂) M) ≡⟨ cong ƛ (ren○ (liftᵣ η₁) (liftᵣ η₂) M) ⟩
ƛ (ren (liftᵣ η₁) (ren (liftᵣ η₂) M)) ∎
ren○ η₁ η₂ (M ∙ N) = cong² _∙_ (ren○ η₁ η₂ M) (ren○ η₁ η₂ N)
renwk○ : ∀ {C Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ ren (wkᵣ {C} (η₁ ○ η₂)) M ≡ (ren (wkᵣ η₁) ∘ ren η₂) M
renwk○ η₁ η₂ M = begin
ren (wkᵣ (η₁ ○ η₂)) M ≡⟨ cong² ren (wk○ η₁ η₂) (refl {x = M}) ⟩
ren (wkᵣ η₁ ○ η₂) M ≡⟨ ren○ (wkᵣ η₁) η₂ M ⟩
ren (wkᵣ η₁) (ren η₂ M) ∎
renlift○ : ∀ {C Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (M : [ Ξ , C ] ⊢ A)
→ ren (liftᵣ {C} (η₁ ○ η₂)) M ≡ (ren (liftᵣ η₁) ∘ ren (liftᵣ η₂)) M
renlift○ η₁ η₂ M = begin
ren (liftᵣ (η₁ ○ η₂)) M ≡⟨ cong² ren (lift○ η₁ η₂) (refl {x = M}) ⟩
ren (liftᵣ η₁ ○ liftᵣ η₂) M ≡⟨ ren○ (liftᵣ η₁) (liftᵣ η₂) M ⟩
ren (liftᵣ η₁) (ren (liftᵣ η₂) M) ∎
renliftwk○ : ∀ {C Γ Δ Ξ A} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ ren (wkᵣ {C} (η₁ ○ η₂)) M ≡ (ren (liftᵣ η₁) ∘ ren (wkᵣ η₂)) M
renliftwk○ η₁ η₂ M = begin
ren (wkᵣ (η₁ ○ η₂)) M ≡⟨ cong² ren (wk○ η₁ η₂) (refl {x = M}) ⟩
ren (wkᵣ η₁ ○ η₂) M ≡⟨ cong² ren (sym (zap○ (wkᵣ η₁) η₂ zero)) (refl {x = M}) ⟩
ren (liftᵣ η₁ ○ wkᵣ η₂) M ≡⟨ ren○ (liftᵣ η₁) (wkᵣ η₂) M ⟩
ren (liftᵣ η₁) (ren (wkᵣ η₂) M) ∎
--------------------------------------------------------------------------------
--
-- 4.4. Advanced properties of _◐_
module _ where
open ≡-Reasoning
get◐ : ∀ {Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (i : Ξ ∋ A)
→ getₛ (σ ◐ η) i ≡ (getₛ σ ∘ getᵣ η) i
get◐ σ [ η , j ] zero = refl
get◐ σ [ η , j ] (suc i) = get◐ σ η i
wk◐ : ∀ {Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ)
→ wkₛ {A} (σ ◐ η) ≡ wkₛ σ ◐ η
wk◐ σ [] = refl
wk◐ σ [ η , i ] = cong² [_,_] (wk◐ σ η) (sym (wkgetₛ σ i))
lift◐ : ∀ {Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ)
→ liftₛ {A} (σ ◐ η) ≡ liftₛ σ ◐ liftᵣ η
lift◐ σ η = begin
[ wkₛ (σ ◐ η) , ` zero ] ≡⟨ cong² [_,_] (wk◐ σ η) refl ⟩
[ wkₛ σ ◐ η , ` zero ] ≡⟨ cong² [_,_] (sym (zap◐ (wkₛ σ) η (` zero))) refl ⟩
[ [ wkₛ σ , ` zero ] ◐ wkᵣ η , ` zero ] ∎
wkid₂◐ : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ wkₛ {A} σ ◐ idᵣ ≡ wkₛ σ
wkid₂◐ σ = begin
wkₛ σ ◐ idᵣ ≡⟨ sym (wk◐ σ idᵣ) ⟩
wkₛ (σ ◐ idᵣ) ≡⟨ cong wkₛ (id₂◐ σ) ⟩
wkₛ σ ∎
liftwkid₂◐ : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ liftₛ {A} σ ◐ wkᵣ idᵣ ≡ wkₛ σ
liftwkid₂◐ σ = begin
[ wkₛ σ , ` zero ] ◐ wkᵣ idᵣ ≡⟨ zap◐ (wkₛ σ) idᵣ (` zero) ⟩
wkₛ σ ◐ idᵣ ≡⟨ wkid₂◐ σ ⟩
wkₛ σ ∎
sub◐ : ∀ {Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ sub (σ ◐ η) M ≡ (sub σ ∘ ren η) M
sub◐ σ η (` i) = get◐ σ η i
sub◐ σ η (ƛ M) = begin
ƛ (sub (liftₛ (σ ◐ η)) M) ≡⟨ cong ƛ (cong² sub (lift◐ σ η) (refl {x = M})) ⟩
ƛ (sub (liftₛ σ ◐ liftᵣ η) M) ≡⟨ cong ƛ (sub◐ (liftₛ σ) (liftᵣ η) M) ⟩
ƛ (sub (liftₛ σ) (ren (liftᵣ η) M)) ∎
sub◐ σ η (M ∙ N) = cong² _∙_ (sub◐ σ η M) (sub◐ σ η N)
subwk◐ : ∀ {C Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (σ ◐ η)) M ≡ (sub (wkₛ σ) ∘ ren η) M
subwk◐ σ η M = begin
sub (wkₛ (σ ◐ η)) M ≡⟨ cong² sub (wk◐ σ η) (refl {x = M}) ⟩
sub (wkₛ σ ◐ η) M ≡⟨ sub◐ (wkₛ σ) η M ⟩
sub (wkₛ σ) (ren η M) ∎
sublift◐ : ∀ {C Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (M : [ Ξ , C ] ⊢ A)
→ sub (liftₛ {C} (σ ◐ η)) M ≡ (sub (liftₛ σ) ∘ ren (liftᵣ η)) M
sublift◐ σ η M = begin
sub (liftₛ (σ ◐ η)) M ≡⟨ cong² sub (lift◐ σ η) (refl {x = M}) ⟩
sub (liftₛ σ ◐ liftᵣ η) M ≡⟨ sub◐ (liftₛ σ) (liftᵣ η) M ⟩
sub (liftₛ σ) (ren (liftᵣ η) M) ∎
subliftwk◐ : ∀ {C Γ Δ Ξ A} → (σ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (σ ◐ η)) M ≡ (sub (liftₛ σ) ∘ ren (wkᵣ η)) M
subliftwk◐ σ η M = begin
sub (wkₛ (σ ◐ η)) M ≡⟨ cong² sub (wk◐ σ η) (refl {x = M}) ⟩
sub (wkₛ σ ◐ η) M ≡⟨ cong² sub (sym (zap◐ (wkₛ σ) η (` zero))) (refl {x = M}) ⟩
sub (liftₛ σ ◐ wkᵣ η) M ≡⟨ sub◐ (liftₛ σ) (wkᵣ η) M ⟩
sub (liftₛ σ) (ren (wkᵣ η) M) ∎
--------------------------------------------------------------------------------
--
-- 4.5. Basic properties of _◑_
module _ where
open ≡-Reasoning
zap◑ : ∀ {Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (i : Δ ∋ A)
→ [ η , i ] ◑ wkₛ σ ≡ η ◑ σ
zap◑ η [] i = refl
zap◑ η [ σ , j ] i = begin
[ [ η , i ] ◑ wkₛ σ , sub [ ⌊ η ⌋ , ` i ] (wk j) ] ≡⟨ cong² [_,_] (zap◑ η σ i) (sym (sub◐ [ ⌊ η ⌋ , ` i ] (wkᵣ idᵣ) j)) ⟩
[ η ◑ σ , sub ([ ⌊ η ⌋ , ` i ] ◐ wkᵣ idᵣ) j ] ≡⟨ cong² [_,_] refl (cong² sub (zap◐ ⌊ η ⌋ idᵣ (` i)) (refl {x = j})) ⟩
[ η ◑ σ , sub (⌊ η ⌋ ◐ idᵣ) j ] ≡⟨ cong² [_,_] refl (cong² sub (id₂◐ ⌊ η ⌋) (refl {x = j})) ⟩
[ η ◑ σ , sub ⌊ η ⌋ j ] ∎
id₁◑ : ∀ {Γ Δ} → (σ : Δ ⊢⋆ Γ)
→ idᵣ ◑ σ ≡ σ
id₁◑ [] = refl
id₁◑ [ σ , M ] = begin
[ idᵣ ◑ σ , sub ⌊ idᵣ ⌋ M ] ≡⟨ cong² [_,_] (id₁◑ σ) (cong² sub (sym ⌊id⌋) (refl {x = M})) ⟩
[ σ , sub idₛ M ] ≡⟨ cong² [_,_] refl (idsub M) ⟩
[ σ , M ] ∎
--------------------------------------------------------------------------------
--
-- 4.6. Basic properties of _●_
module _ where
open ≡-Reasoning
zap● : ∀ {Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (M : Δ ⊢ A)
→ [ σ₁ , M ] ● wkₛ σ₂ ≡ σ₁ ● σ₂
zap● σ₁ [] M = refl
zap● σ₁ [ σ₂ , N ] M = begin
[ [ σ₁ , M ] ● wkₛ σ₂ , sub [ σ₁ , M ] (wk N) ] ≡⟨ cong² [_,_] (zap● σ₁ σ₂ M) (sym (sub◐ [ σ₁ , M ] (wkᵣ idᵣ) N)) ⟩
[ σ₁ ● σ₂ , sub ([ σ₁ , M ] ◐ wkᵣ idᵣ) N ] ≡⟨ cong² [_,_] refl (cong² sub (zap◐ σ₁ idᵣ M) (refl {x = N})) ⟩
[ σ₁ ● σ₂ , sub (σ₁ ◐ idᵣ) N ] ≡⟨ cong² [_,_] refl (cong² sub (id₂◐ σ₁) (refl {x = N})) ⟩
[ σ₁ ● σ₂ , sub σ₁ N ] ∎
id₁● : ∀ {Γ Δ} → (σ : Δ ⊢⋆ Γ)
→ idₛ ● σ ≡ σ
id₁● [] = refl
id₁● [ σ , M ] = cong² [_,_] (id₁● σ) (idsub M)
id₂● : ∀ {Γ Δ} → (σ : Δ ⊢⋆ Γ)
→ σ ● idₛ ≡ σ
id₂● σ = begin
σ ● idₛ ≡⟨ cong² _●_ refl ⌊id⌋ ⟩
σ ◐ idᵣ ≡⟨ id₂◐ σ ⟩
σ ∎
--------------------------------------------------------------------------------
--
-- 4.7. Advanced properties of _◑_
module _ where
open ≡-Reasoning
get◑ : ∀ {Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A)
→ getₛ (η ◑ σ) i ≡ (ren η ∘ getₛ σ) i
get◑ η [ σ , M ] zero = ⌊sub⌋ η M
get◑ η [ σ , M ] (suc i) = get◑ η σ i
wk◑ : ∀ {Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ)
→ wkₛ {A} (η ◑ σ) ≡ wkᵣ η ◑ σ
wk◑ η [] = refl
wk◑ η [ σ , M ] = begin
[ wkₛ (η ◑ σ) , wk (sub ⌊ η ⌋ M) ] ≡⟨ cong² [_,_] refl (cong² ren refl (⌊sub⌋ η M)) ⟩
[ wkₛ (η ◑ σ) , wk (ren η M) ] ≡⟨ cong² [_,_] refl (sym (ren○ (wkᵣ idᵣ) η M)) ⟩
[ wkₛ (η ◑ σ) , ren (wkᵣ idᵣ ○ η) M ] ≡⟨ cong² [_,_] refl (cong² ren (sym (wk○ idᵣ η)) refl) ⟩
[ wkₛ (η ◑ σ) , ren (wkᵣ (idᵣ ○ η)) M ] ≡⟨ cong² [_,_] refl (cong² ren (cong wkᵣ (id₁○ η)) refl) ⟩
[ wkₛ (η ◑ σ) , ren (wkᵣ η) M ] ≡⟨ cong² [_,_] (wk◑ η σ) (sym (⌊sub⌋ (wkᵣ η) M)) ⟩
[ wkᵣ η ◑ σ , sub ⌊ wkᵣ η ⌋ M ] ∎
lift◑ : ∀ {Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ)
→ liftₛ {A} (η ◑ σ) ≡ liftᵣ η ◑ liftₛ σ
lift◑ η σ = begin
[ wkₛ (η ◑ σ) , ` zero ] ≡⟨ cong² [_,_] (wk◑ η σ) refl ⟩
[ wkᵣ η ◑ σ , ` zero ] ≡⟨ cong² [_,_] (sym (zap● ⌊ wkᵣ η ⌋ σ (` zero))) refl ⟩
[ [ ⌊ wkᵣ η ⌋ , ` zero ] ● wkₛ σ , ` zero ] ∎
wkid₁◑ : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ wkᵣ {A} idᵣ ◑ σ ≡ wkₛ σ
wkid₁◑ σ = begin
wkᵣ idᵣ ◑ σ ≡⟨ sym (wk◑ idᵣ σ) ⟩
wkₛ (idᵣ ◑ σ) ≡⟨ cong wkₛ (id₁◑ σ) ⟩
wkₛ σ ∎
liftwkid₁◑ : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ (liftᵣ {A} idᵣ ◑ wkₛ σ) ≡ wkₛ σ
liftwkid₁◑ σ = begin
([ wkᵣ idᵣ , zero ] ◑ wkₛ σ) ≡⟨ zap◑ (wkᵣ idᵣ) σ zero ⟩
wkᵣ idᵣ ◑ σ ≡⟨ wkid₁◑ σ ⟩
wkₛ σ ∎
sub◑ : ∀ {Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (η ◑ σ) M ≡ (ren η ∘ sub σ) M
sub◑ η σ (` i) = get◑ η σ i
sub◑ η σ (ƛ M) = begin
ƛ (sub (liftₛ (η ◑ σ)) M) ≡⟨ cong ƛ (cong² sub (lift◑ η σ) (refl {x = M})) ⟩
ƛ (sub (liftᵣ η ◑ liftₛ σ) M) ≡⟨ cong ƛ (sub◑ (liftᵣ η) (liftₛ σ) M) ⟩
ƛ (ren (liftᵣ η) (sub (liftₛ σ) M)) ∎
sub◑ η σ (M ∙ N) = cong² _∙_ (sub◑ η σ M) (sub◑ η σ N)
subwk◑ : ∀ {C Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (η ◑ σ)) M ≡ (ren (wkᵣ η) ∘ sub σ) M
subwk◑ η σ M = begin
sub (wkₛ (η ◑ σ)) M ≡⟨ cong² sub (wk◑ η σ) (refl {x = M}) ⟩
sub (wkᵣ η ◑ σ) M ≡⟨ sub◑ (wkᵣ η) σ M ⟩
ren (wkᵣ η) (sub σ M) ∎
sublift◑ : ∀ {C Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : [ Ξ , C ] ⊢ A)
→ sub (liftₛ {C} (η ◑ σ)) M ≡ (ren (liftᵣ η) ∘ sub (liftₛ σ)) M
sublift◑ η σ M = begin
sub (liftₛ (η ◑ σ)) M ≡⟨ cong² sub (lift◑ η σ) (refl {x = M}) ⟩
sub (liftᵣ η ◑ liftₛ σ) M ≡⟨ sub◑ (liftᵣ η) (liftₛ σ) M ⟩
ren (liftᵣ η) (sub (liftₛ σ) M) ∎
subliftwk◑ : ∀ {C Γ Δ Ξ A} → (η : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (η ◑ σ)) M ≡ (ren (liftᵣ η) ∘ sub (wkₛ σ)) M
subliftwk◑ η σ M = begin
sub (wkₛ (η ◑ σ)) M ≡⟨ cong² sub (wk◑ η σ) (refl {x = M}) ⟩
sub (wkᵣ η ◑ σ) M ≡⟨ cong² sub (sym (zap◑ (wkᵣ η) σ zero)) (refl {x = M}) ⟩
sub (liftᵣ η ◑ wkₛ σ) M ≡⟨ sub◑ (liftᵣ η) (wkₛ σ) M ⟩
ren (liftᵣ η) (sub (wkₛ σ) M) ∎
--------------------------------------------------------------------------------
--
-- 4.8. Advanced properties of _●_
module _ where
open ≡-Reasoning
get● : ∀ {Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A)
→ getₛ (σ₁ ● σ₂) i ≡ (sub σ₁ ∘ getₛ σ₂) i
get● σ₁ [ σ₂ , M ] zero = refl
get● σ₁ [ σ₂ , M ] (suc i) = get● σ₁ σ₂ i
wk● : ∀ {Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ)
→ wkₛ {A} (σ₁ ● σ₂) ≡ wkₛ σ₁ ● σ₂
wk● σ₁ [] = refl
wk● σ₁ [ σ₂ , M ] = begin
[ wkₛ (σ₁ ● σ₂) , wk (sub σ₁ M) ] ≡⟨ cong² [_,_] (wk● σ₁ σ₂) (sym (sub◑ (wkᵣ idᵣ) σ₁ M)) ⟩
[ wkₛ σ₁ ● σ₂ , sub (wkᵣ idᵣ ◑ σ₁) M ] ≡⟨ cong² [_,_] refl (cong² sub (wkid₁◑ σ₁) (refl {x = M})) ⟩
[ wkₛ σ₁ ● σ₂ , sub (wkₛ σ₁) M ] ∎
lift● : ∀ {Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ)
→ liftₛ {A} (σ₁ ● σ₂) ≡ liftₛ σ₁ ● liftₛ σ₂
lift● σ₁ σ₂ = begin
[ wkₛ (σ₁ ● σ₂) , ` zero ] ≡⟨ cong² [_,_] (wk● σ₁ σ₂) refl ⟩
[ wkₛ σ₁ ● σ₂ , ` zero ] ≡⟨ cong² [_,_] (sym (zap● (wkₛ σ₁) σ₂ (` zero))) refl ⟩
[ [ wkₛ σ₁ , ` zero ] ● wkₛ σ₂ , ` zero ] ∎
wkid₁● : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ wkₛ {A} idₛ ● σ ≡ wkₛ σ
wkid₁● σ = begin
wkₛ idₛ ● σ ≡⟨ sym (wk● idₛ σ) ⟩
wkₛ (idₛ ● σ) ≡⟨ cong wkₛ (id₁● σ) ⟩
wkₛ σ ∎
wkid₂● : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ wkₛ {A} σ ● idₛ ≡ wkₛ σ
wkid₂● σ = begin
wkₛ σ ● idₛ ≡⟨ sym (wk● σ idₛ) ⟩
wkₛ (σ ● idₛ) ≡⟨ cong wkₛ (id₂● σ) ⟩
wkₛ σ ∎
liftwkid₂● : ∀ {Γ Δ A} → (σ : Δ ⊢⋆ Γ)
→ liftₛ {A} σ ● wkₛ idₛ ≡ wkₛ σ
liftwkid₂● σ = begin
[ wkₛ σ , ` zero ] ● wkₛ idₛ ≡⟨ zap● (wkₛ σ) idₛ (` zero) ⟩
wkₛ σ ● idₛ ≡⟨ wkid₂● σ ⟩
wkₛ σ ∎
sub● : ∀ {Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (σ₁ ● σ₂) M ≡ (sub σ₁ ∘ sub σ₂) M
sub● σ₁ σ₂ (` i) = get● σ₁ σ₂ i
sub● σ₁ σ₂ (ƛ M) = begin
ƛ (sub (liftₛ (σ₁ ● σ₂)) M) ≡⟨ cong ƛ (cong² sub (lift● σ₁ σ₂) (refl {x = M})) ⟩
ƛ (sub (liftₛ σ₁ ● liftₛ σ₂) M) ≡⟨ cong ƛ (sub● (liftₛ σ₁) (liftₛ σ₂) M) ⟩
ƛ (sub (liftₛ σ₁) (sub (liftₛ σ₂) M)) ∎
sub● σ₁ σ₂ (M ∙ N) = cong² _∙_ (sub● σ₁ σ₂ M) (sub● σ₁ σ₂ N)
subwk● : ∀ {C Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (σ₁ ● σ₂)) M ≡ (sub (wkₛ σ₁) ∘ sub σ₂) M
subwk● σ₁ σ₂ M = begin
sub (wkₛ (σ₁ ● σ₂)) M ≡⟨ cong² sub (wk● σ₁ σ₂) (refl {x = M}) ⟩
sub (wkₛ σ₁ ● σ₂) M ≡⟨ sub● (wkₛ σ₁) σ₂ M ⟩
sub (wkₛ σ₁) (sub σ₂ M) ∎
sublift● : ∀ {C Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (M : [ Ξ , C ] ⊢ A)
→ sub (liftₛ {C} (σ₁ ● σ₂)) M ≡ (sub (liftₛ σ₁) ∘ sub (liftₛ σ₂)) M
sublift● σ₁ σ₂ M = begin
sub (liftₛ (σ₁ ● σ₂)) M ≡⟨ cong² sub (lift● σ₁ σ₂) (refl {x = M}) ⟩
sub (liftₛ σ₁ ● liftₛ σ₂) M ≡⟨ sub● (liftₛ σ₁) (liftₛ σ₂) M ⟩
sub (liftₛ σ₁) (sub (liftₛ σ₂) M) ∎
subliftwk● : ∀ {C Γ Δ Ξ A} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
→ sub (wkₛ {C} (σ₁ ● σ₂)) M ≡ (sub (liftₛ σ₁) ∘ sub (wkₛ σ₂)) M
subliftwk● σ₁ σ₂ M = begin
sub (wkₛ (σ₁ ● σ₂)) M ≡⟨ cong² sub (wk● σ₁ σ₂) (refl {x = M}) ⟩
sub (wkₛ σ₁ ● σ₂) M ≡⟨ cong² sub (sym (zap● (wkₛ σ₁) σ₂ (` zero))) (refl {x = M}) ⟩
sub (liftₛ σ₁ ● wkₛ σ₂) M ≡⟨ sub● (liftₛ σ₁) (wkₛ σ₂) M ⟩
sub (liftₛ σ₁) (sub (wkₛ σ₂) M) ∎
--------------------------------------------------------------------------------
--
-- 4.9. Compositions of compositions
module _ where
open ≡-Reasoning
-- Compositions with _○_
assoc○ : ∀ {Γ Δ Ξ Ω} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (η₃ : Ξ ∋⋆ Ω)
→ η₁ ○ (η₂ ○ η₃) ≡ (η₁ ○ η₂) ○ η₃
assoc○ η₁ η₂ [] = refl
assoc○ η₁ η₂ [ η₃ , i ] = cong² [_,_] (assoc○ η₁ η₂ η₃) (sym (get○ η₁ η₂ i))
-- Compositions with _◐_
comp◐○ : ∀ {Γ Δ Ξ Ω} → (σ : Δ ⊢⋆ Γ) (η₁ : Γ ∋⋆ Ξ) (η₂ : Ξ ∋⋆ Ω)
→ σ ◐ (η₁ ○ η₂) ≡ (σ ◐ η₁) ◐ η₂
comp◐○ σ η₁ [] = refl
comp◐○ σ η₁ [ η₂ , i ] = cong² [_,_] (comp◐○ σ η₁ η₂) (sym (get◐ σ η₁ i))
-- Compositions with _◑_
comp◑○ : ∀ {Γ Δ Ξ Ω} → (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) (σ : Ξ ⊢⋆ Ω)
→ η₁ ◑ (η₂ ◑ σ) ≡ (η₁ ○ η₂) ◑ σ
comp◑○ η₁ η₂ [] = refl
comp◑○ η₁ η₂ [ σ , M ] = cong² [_,_] (comp◑○ η₁ η₂ σ) (trans (sym (sub● ⌊ η₁ ⌋ ⌊ η₂ ⌋ M))
(sym (cong² sub (⌊○⌋ η₁ η₂) (refl {x = M}))))
comp◑◐ : ∀ {Γ Δ Ξ Ω} → (η₁ : Δ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (η₂ : Ξ ∋⋆ Ω)
→ η₁ ◑ (σ ◐ η₂) ≡ (η₁ ◑ σ) ◐ η₂
comp◑◐ η₁ σ [] = refl
comp◑◐ η₁ σ [ η₂ , i ] = begin
[ η₁ ◑ (σ ◐ η₂) , sub ⌊ η₁ ⌋ (sub σ (` i)) ] ≡⟨ cong² [_,_] (comp◑◐ η₁ σ η₂) (⌊sub⌋ η₁ (getₛ σ i)) ⟩
[ (η₁ ◑ σ) ◐ η₂ , ren η₁ (getₛ σ i) ] ≡⟨ cong² [_,_] refl (sym (get◑ η₁ σ i)) ⟩
[ (η₁ ◑ σ) ◐ η₂ , getₛ (η₁ ◑ σ) i ] ∎
comp◑● : ∀ {Γ Δ Ξ Ω} → (η : Δ ∋⋆ Γ) (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Ω)
→ η ◑ (σ₁ ● σ₂) ≡ (η ◑ σ₁) ● σ₂
comp◑● η σ₁ [] = refl
comp◑● η σ₁ [ σ₂ , M ] = cong² [_,_] (comp◑● η σ₁ σ₂) (sym (sub● ⌊ η ⌋ σ₁ M))
-- Compositions with _●_
comp●◐ : ∀ {Γ Δ Ξ Ω} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (η : Ξ ∋⋆ Ω)
→ σ₁ ● (σ₂ ◐ η) ≡ (σ₁ ● σ₂) ◐ η
comp●◐ σ₁ σ₂ [] = refl
comp●◐ σ₁ σ₂ [ η , i ] = cong² [_,_] (comp●◐ σ₁ σ₂ η) (sym (get● σ₁ σ₂ i))
comp●◑ : ∀ {Γ Δ Ξ Ω} → (σ₁ : Δ ⊢⋆ Γ) (η : Γ ∋⋆ Ξ) (σ₂ : Ξ ⊢⋆ Ω)
→ σ₁ ● (η ◑ σ₂) ≡ (σ₁ ◐ η) ● σ₂
comp●◑ σ₁ η [] = refl
comp●◑ σ₁ η [ σ₂ , M ] = cong² [_,_] (comp●◑ σ₁ η σ₂) (sym (sub● σ₁ ⌊ η ⌋ M))
assoc● : ∀ {Γ Δ Ξ Ω} → (σ₁ : Δ ⊢⋆ Γ) (σ₂ : Γ ⊢⋆ Ξ) (σ₃ : Ξ ⊢⋆ Ω)
→ σ₁ ● (σ₂ ● σ₃) ≡ (σ₁ ● σ₂) ● σ₃
assoc● σ₁ σ₂ [] = refl
assoc● σ₁ σ₂ [ σ₃ , M ] = cong² [_,_] (assoc● σ₁ σ₂ σ₃) (sym (sub● σ₁ σ₂ M))
--------------------------------------------------------------------------------
--
-- 5. Convertibility
infix 3 _≅_
data _≅_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
refl≅ : ∀ {Γ A} → {M : Γ ⊢ A}
→ M ≅ M
sym≅ : ∀ {Γ A} → {M M′ : Γ ⊢ A}
→ M ≅ M′
→ M′ ≅ M
trans≅ : ∀ {Γ A} → {M M′ M″ : Γ ⊢ A}
→ M ≅ M′ → M′ ≅ M″
→ M ≅ M″
congƛ≅ : ∀ {Γ A B} → {M M′ : [ Γ , A ] ⊢ B}
→ M ≅ M′
→ ƛ M ≅ ƛ M′
cong∙≅ : ∀ {Γ A B} → {M M′ : Γ ⊢ A ⊃ B} {N N′ : Γ ⊢ A}
→ M ≅ M′ → N ≅ N′
→ M ∙ N ≅ M′ ∙ N′
redβ≅ : ∀ {Γ Δ A B} → (σ : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A)
→ sub σ (ƛ M) ∙ N ≅ sub [ σ , N ] M
expη≅ : ∀ {Γ A B} → (M : Γ ⊢ A ⊃ B)
→ M ≅ ƛ (wk M ∙ ` zero)
≡→≅ : ∀ {Γ A} → {M M′ : Γ ⊢ A} → M ≡ M′ → M ≅ M′
≡→≅ refl = refl≅
module ≅-Reasoning where
infix 1 begin_
begin_ : ∀ {Γ A} → {M M′ : Γ ⊢ A} → M ≅ M′ → M ≅ M′
begin p = p
infixr 2 _≅⟨⟩_
_≅⟨⟩_ : ∀ {Γ A} → (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
M ≅⟨⟩ p = p
infixr 2 _≅⟨_⟩_
_≅⟨_⟩_ : ∀ {Γ A} → (M {M′ M″} : Γ ⊢ A) → M ≅ M′ → M′ ≅ M″ → M ≅ M″
M ≅⟨ p ⟩ q = trans≅ p q
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ {Γ A} → (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
M ≡⟨⟩ p = p
infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ {Γ A} → (M {M′ M″} : Γ ⊢ A) → M ≡ M′ → M′ ≅ M″ → M ≅ M″
M ≡⟨ p ⟩ q = trans≅ (≡→≅ p) q
infix 3 _∎
_∎ : ∀ {Γ A} → (M : Γ ⊢ A) → M ≅ M
M ∎ = refl≅
--------------------------------------------------------------------------------
--
-- 5.1. Convertibility of substitutions
infix 3 _≅⋆_
data _≅⋆_ : ∀ {Γ Δ} → Δ ⊢⋆ Γ → Δ ⊢⋆ Γ → Set where
[] : ∀ {Δ} → ([] {Δ}) ≅⋆ []
[_,_] : ∀ {Γ Δ A} → {σ σ′ : Δ ⊢⋆ Γ} {M M′ : Δ ⊢ A}
→ (ψ : σ ≅⋆ σ′) (p : M ≅ M′)
→ [ σ , M ] ≅⋆ [ σ′ , M′ ]
refl≅⋆ : ∀ {Γ Δ} → {σ : Δ ⊢⋆ Γ}
→ σ ≅⋆ σ
refl≅⋆ {σ = []} = []
refl≅⋆ {σ = [ σ , M ]} = [ refl≅⋆ , refl≅ ]
sym≅⋆ : ∀ {Γ Δ} → {σ σ′ : Δ ⊢⋆ Γ}
→ σ ≅⋆ σ′
→ σ′ ≅⋆ σ
sym≅⋆ [] = []
sym≅⋆ [ ψ , p ] = [ sym≅⋆ ψ , sym≅ p ]
trans≅⋆ : ∀ {Γ Δ} → {σ σ′ σ″ : Δ ⊢⋆ Γ}
→ σ ≅⋆ σ′ → σ′ ≅⋆ σ″
→ σ ≅⋆ σ″
trans≅⋆ [] [] = []
trans≅⋆ [ ψ₁ , p ] [ ψ₂ , q ] = [ trans≅⋆ ψ₁ ψ₂ , trans≅ p q ]
≡→≅⋆ : ∀ {Γ Δ} → {σ σ′ : Δ ⊢⋆ Γ}
→ σ ≡ σ′
→ σ ≅⋆ σ′
≡→≅⋆ refl = refl≅⋆
module ≅⋆-Reasoning where
infix 1 begin_
begin_ : ∀ {Γ Δ} → {σ σ′ : Δ ⊢⋆ Γ} → σ ≅⋆ σ′ → σ ≅⋆ σ′
begin ψ = ψ
infixr 2 _≅⋆⟨⟩_
_≅⋆⟨⟩_ : ∀ {Γ Δ} → (σ {σ′} : Δ ⊢⋆ Γ) → σ ≅⋆ σ′ → σ ≅⋆ σ′
σ ≅⋆⟨⟩ ψ = ψ
infixr 2 _≅⋆⟨_⟩_
_≅⋆⟨_⟩_ : ∀ {Γ Δ} → (σ {σ′ σ″} : Δ ⊢⋆ Γ) → σ ≅⋆ σ′ → σ′ ≅⋆ σ″ → σ ≅⋆ σ″
σ ≅⋆⟨ ψ₁ ⟩ ψ₂ = trans≅⋆ ψ₁ ψ₂
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ {Γ Δ} → (σ {σ′} : Δ ⊢⋆ Γ) → σ ≅⋆ σ′ → σ ≅⋆ σ′
σ ≡⟨⟩ ψ = ψ
infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ {Γ Δ} → (σ {σ′ σ″} : Δ ⊢⋆ Γ) → σ ≡ σ′ → σ′ ≅⋆ σ″ → σ ≅⋆ σ″
σ ≡⟨ ψ₁ ⟩ ψ₂ = trans≅⋆ (≡→≅⋆ ψ₁) ψ₂
infix 3 _∎
_∎ : ∀ {Γ Δ} → (σ : Δ ⊢⋆ Γ) → σ ≅⋆ σ
σ ∎ = refl≅⋆
--------------------------------------------------------------------------------
--
-- 6. Congruence of _≅_ with respect to renaming
module _ where
open ≅-Reasoning
congrenβ≅ : ∀ {Γ Δ Ξ A B} → {η : Δ ∋⋆ Γ}
→ (σ : Γ ⊢⋆ Ξ) (M : [ Ξ , A ] ⊢ B) (N : Γ ⊢ A)
→ ren η (sub σ (ƛ M) ∙ N) ≅ ren η (sub [ σ , N ] M)
congrenβ≅ {η = η} σ M N = begin
ƛ (ren (liftᵣ η) (sub (liftₛ σ) M)) ∙ ren η N ≅⟨ cong∙≅ (congƛ≅ (≡→≅ (sym (sublift◑ η σ M)))) refl≅ ⟩
sub (η ◑ σ) (ƛ M) ∙ ren η N ≅⟨ redβ≅ (η ◑ σ) M (ren η N) ⟩
sub [ η ◑ σ , ren η N ] M ≡⟨ cong² sub (cong² [_,_] refl (sym (⌊sub⌋ η N))) (refl {x = M}) ⟩
sub (η ◑ [ σ , N ]) M ≡⟨ sub◑ η [ σ , N ] M ⟩
ren η (sub [ σ , N ] M) ∎
congrenη`≅ : ∀ {Γ Δ A B} → {η : Δ ∋⋆ Γ}
→ (i : Γ ∋ A ⊃ B)
→ ren η (` i) ≅ ren η (ƛ (wk (` i) ∙ ` zero))
congrenη`≅ {η = η} i = begin
` (getᵣ η i) ≅⟨ expη≅ (` (getᵣ η i)) ⟩
ƛ (wk (` (getᵣ η i)) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ` (sym (get○ (wkᵣ idᵣ) η i)))) refl≅) ⟩
ƛ (` (getᵣ (wkᵣ idᵣ ○ η) i) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ` (cong² getᵣ (wkid₁○ η) (refl {x = i})))) refl≅) ⟩
ƛ (` (getᵣ (wkᵣ η) i) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ` (cong² getᵣ (sym (liftwkid₂○ η)) (refl {x = i})))) refl≅) ⟩
ƛ (` (getᵣ (liftᵣ η ○ wkᵣ idᵣ) i) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ` (get○ (liftᵣ η) (wkᵣ idᵣ) i))) refl≅) ⟩
ƛ (` (getᵣ (liftᵣ η) (getᵣ (wkᵣ idᵣ) i)) ∙ ` zero) ∎
congrenηƛ≅ : ∀ {Γ Δ A B} → {η : Δ ∋⋆ Γ}
→ (M : [ Γ , A ] ⊢ B)
→ ren η (ƛ M) ≅ ren η (ƛ (wk (ƛ M) ∙ ` zero))
congrenηƛ≅ {η = η} M = begin
ƛ (ren (liftᵣ η) M) ≅⟨ expη≅ (ƛ (ren (liftᵣ η) M)) ⟩
ƛ (wk (ƛ (ren (liftᵣ η) M)) ∙ ` zero) ≡⟨⟩
ƛ (ƛ (ren (liftᵣ (wkᵣ idᵣ)) (ren (liftᵣ η) M)) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (sym (renlift○ (wkᵣ idᵣ) η M)))) refl≅) ⟩
ƛ (ƛ (ren (liftᵣ (wkᵣ idᵣ ○ η)) M) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (wkid₁○ η)) (refl {x = M})))) refl≅) ⟩
ƛ (ƛ (ren (liftᵣ (wkᵣ η)) M) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (sym (wkid₂○ η))) (refl {x = M})))) refl≅) ⟩
ƛ (ƛ (ren (liftᵣ (wkᵣ η ○ idᵣ)) M) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (sym (zap○ (wkᵣ η) idᵣ zero))) (refl {x = M})))) refl≅) ⟩
ƛ (ƛ (ren (liftᵣ (liftᵣ η ○ wkᵣ idᵣ)) M) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (renlift○ (liftᵣ η) (wkᵣ idᵣ) M))) refl≅) ⟩
ƛ (ƛ (ren (liftᵣ (liftᵣ η)) (ren (liftᵣ (wkᵣ idᵣ)) M)) ∙ ` zero) ∎
congrenη∙≅ : ∀ {C Γ Δ A B} → {η : Δ ∋⋆ Γ}
→ (M : Γ ⊢ C ⊃ A ⊃ B) (N : Γ ⊢ C)
→ ren η (M ∙ N) ≅ ren η (ƛ (wk (M ∙ N) ∙ ` zero))
congrenη∙≅ {η = η} M N = begin
ren η M ∙ ren η N ≅⟨ expη≅ (ren η M ∙ ren η N) ⟩
ƛ (wk (ren η M ∙ ren η N) ∙ ` zero) ≡⟨⟩
ƛ ((ren (wkᵣ idᵣ) (ren η M) ∙ ren (wkᵣ idᵣ) (ren η N)) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (ren○ (wkᵣ idᵣ) η M))) (≡→≅ (sym (ren○ (wkᵣ idᵣ) η N)))) refl≅) ⟩
ƛ ((ren (wkᵣ idᵣ ○ η) M ∙ ren (wkᵣ idᵣ ○ η) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (wkid₁○ η) (refl {x = M}))) (≡→≅ (cong² ren (wkid₁○ η) (refl {x = N})))) refl≅) ⟩
ƛ ((ren (wkᵣ η) M ∙ ren (wkᵣ η) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (sym (wkid₂○ η)) (refl {x = M}))) (≡→≅ (cong² ren (sym (wkid₂○ η)) (refl {x = N})))) refl≅) ⟩
ƛ ((ren (wkᵣ η ○ idᵣ) M ∙ ren (wkᵣ η ○ idᵣ) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (sym (wk○ η idᵣ)) (refl {x = M}))) (≡→≅ (cong² ren (sym (wk○ η idᵣ)) (refl {x = N})))) refl≅) ⟩
ƛ ((ren (wkᵣ (η ○ idᵣ)) M ∙ ren (wkᵣ (η ○ idᵣ)) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (renliftwk○ η idᵣ M)) (≡→≅ (renliftwk○ η idᵣ N))) refl≅) ⟩
ƛ ((ren (liftᵣ η) (wk M) ∙ ren (liftᵣ η) (wk N)) ∙ ` zero) ∎
congren≅ : ∀ {Γ Δ A} → {η : Δ ∋⋆ Γ} {M M′ : Γ ⊢ A}
→ M ≅ M′
→ ren η M ≅ ren η M′
congren≅ refl≅ = refl≅
congren≅ (sym≅ p) = sym≅ (congren≅ p)
congren≅ (trans≅ p q) = trans≅ (congren≅ p) (congren≅ q)
congren≅ (congƛ≅ p) = congƛ≅ (congren≅ p)
congren≅ (cong∙≅ p q) = cong∙≅ (congren≅ p) (congren≅ q)
congren≅ (redβ≅ σ M N) = congrenβ≅ σ M N
congren≅ (expη≅ (` i)) = congrenη`≅ i
congren≅ (expη≅ (ƛ M)) = congrenηƛ≅ M
congren≅ (expη≅ (M ∙ N)) = congrenη∙≅ M N
--------------------------------------------------------------------------------
--
-- 6.1. Congruence of _≅⋆_
congwk≅⋆ : ∀ {C Γ Δ} → {σ σ′ : Δ ⊢⋆ Γ}
→ σ ≅⋆ σ′
→ wkₛ {C} σ ≅⋆ wkₛ σ′
congwk≅⋆ [] = []
congwk≅⋆ [ ψ , p ] = [ congwk≅⋆ ψ , congren≅ p ]
conglift≅⋆ : ∀ {C Γ Δ} → {σ σ′ : Δ ⊢⋆ Γ}
→ σ ≅⋆ σ′
→ liftₛ {C} σ ≅⋆ liftₛ σ′
conglift≅⋆ [] = [ [] , refl≅ ]
conglift≅⋆ [ ψ , p ] = [ [ congwk≅⋆ ψ , congren≅ p ] , refl≅ ]
--------------------------------------------------------------------------------
--
-- 7. Congruence of _≅_ with respect to substitution
module _ where
open ≅-Reasoning
congsubβ≅ : ∀ {Γ Δ Ξ A B} → {σ₁ : Δ ⊢⋆ Γ}
→ (σ₂ : Γ ⊢⋆ Ξ) (M : [ Ξ , A ] ⊢ B) (N : Γ ⊢ A)
→ sub σ₁ (sub σ₂ (ƛ M) ∙ N) ≅ sub σ₁ (sub [ σ₂ , N ] M)
congsubβ≅ {σ₁ = σ₁} σ₂ M N = begin
ƛ (sub (liftₛ σ₁) (sub (liftₛ σ₂) M)) ∙ sub σ₁ N ≅⟨ cong∙≅ (congƛ≅ (≡→≅ (sym (sublift● σ₁ σ₂ M)))) refl≅ ⟩
sub (σ₁ ● σ₂) (ƛ M) ∙ sub σ₁ N ≅⟨ redβ≅ (σ₁ ● σ₂) M (sub σ₁ N) ⟩
sub [ σ₁ ● σ₂ , sub σ₁ N ] M ≡⟨ sub● σ₁ [ σ₂ , N ] M ⟩
sub σ₁ (sub [ σ₂ , N ] M) ∎
congsubη`≅ : ∀ {Γ Δ A B} → {σ : Δ ⊢⋆ Γ}
→ (i : Γ ∋ A ⊃ B)
→ sub σ (` i) ≅ sub σ (ƛ (wk (` i) ∙ ` zero))
congsubη`≅ {σ = σ} i = begin
getₛ σ i ≅⟨ expη≅ (getₛ σ i) ⟩
ƛ (wk (getₛ σ i) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (sym (wkgetₛ σ i))) refl≅) ⟩
ƛ (getₛ (wkₛ σ) i ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong² getₛ (sym (liftwkid₂◐ σ)) (refl {x = i}))) refl≅) ⟩
ƛ (getₛ (liftₛ σ ◐ wkᵣ idᵣ) i ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (get◐ (liftₛ σ) (wkᵣ idᵣ) i)) refl≅) ⟩
ƛ (getₛ (liftₛ σ) (getᵣ (wkᵣ idᵣ) i) ∙ ` zero) ∎
congsubηƛ≅ : ∀ {Γ Δ A B} → {σ : Δ ⊢⋆ Γ}
→ (M : [ Γ , A ] ⊢ B)
→ sub σ (ƛ M) ≅ sub σ (ƛ (wk (ƛ M) ∙ ` zero))
congsubηƛ≅ {σ = σ} M = begin
ƛ (sub (liftₛ σ) M) ≡⟨⟩
ƛ (sub [ wkₛ σ , ` zero ] M) ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (id₂◐ (wkₛ σ))) refl) (refl {x = M}))) ⟩
ƛ (sub [ wkₛ σ ◐ idᵣ , ` zero ] M) ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (zap◐ (wkₛ σ) idᵣ (` zero))) refl) (refl {x = M}))) ⟩
ƛ (sub [ [ wkₛ σ , ` zero ] ◐ wkᵣ idᵣ , ` zero ] M) ≡⟨⟩
ƛ (sub [ liftₛ σ ◐ wkᵣ idᵣ , ` zero ] M) ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (zap◐ (liftₛ σ) (wkᵣ idᵣ) (` zero))) refl) (refl {x = M}))) ⟩
ƛ (sub [ [ liftₛ σ , ` zero ] ◐ wkᵣ (wkᵣ idᵣ) , ` zero ] M) ≡⟨⟩
ƛ (sub ([ liftₛ σ , ` zero ] ◐ liftᵣ (wkᵣ idᵣ)) M) ≅⟨ congƛ≅ (≡→≅ (sub◐ [ liftₛ σ , ` zero ] (liftᵣ (wkᵣ idᵣ)) M)) ⟩
ƛ (sub [ liftₛ σ , ` zero ] (ren (liftᵣ (wkᵣ idᵣ)) M)) ≅⟨ congƛ≅ (sym≅ (redβ≅ (liftₛ σ) (ren (liftᵣ (wkᵣ idᵣ)) M) (` zero))) ⟩
ƛ (ƛ (sub (liftₛ (liftₛ σ)) (ren (liftᵣ (wkᵣ idᵣ)) M)) ∙ ` zero) ∎
congsubη∙≅ : ∀ {Γ Δ A B C} → {σ : Δ ⊢⋆ Γ}
→ (M : Γ ⊢ C ⊃ A ⊃ B) (N : Γ ⊢ C)
→ sub σ (M ∙ N) ≅ sub σ (ƛ (wk (M ∙ N) ∙ ` zero))
congsubη∙≅ {σ = σ} M N = begin
sub σ M ∙ sub σ N ≅⟨ expη≅ (sub σ M ∙ sub σ N) ⟩
ƛ (wk (sub σ M ∙ sub σ N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (sub◑ (wkᵣ idᵣ) σ M))) (≡→≅ (sym (sub◑ (wkᵣ idᵣ) σ N)))) refl≅) ⟩
ƛ ((sub (wkᵣ idᵣ ◑ σ) M ∙ sub (wkᵣ idᵣ ◑ σ) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² sub (wkid₁◑ σ) (refl {x = M}))) (≡→≅ (cong² sub (wkid₁◑ σ) (refl {x = N})))) refl≅) ⟩
ƛ ((sub (wkₛ σ) M ∙ sub (wkₛ σ) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² sub (sym (wkid₂◐ σ)) (refl {x = M}))) (≡→≅ (cong² sub (sym (wkid₂◐ σ)) (refl {x = N})))) refl≅) ⟩
ƛ ((sub (wkₛ σ ◐ idᵣ) M ∙ sub (wkₛ σ ◐ idᵣ) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² sub (sym (wk◐ σ idᵣ)) (refl {x = M}))) (≡→≅ (cong² sub (sym (wk◐ σ idᵣ)) (refl {x = N})))) refl≅) ⟩
ƛ ((sub (wkₛ (σ ◐ idᵣ)) M ∙ sub (wkₛ (σ ◐ idᵣ)) N) ∙ ` zero) ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (subliftwk◐ σ idᵣ M)) (≡→≅ (subliftwk◐ σ idᵣ N))) refl≅) ⟩
ƛ ((sub (liftₛ σ) (wk M) ∙ sub (liftₛ σ) (wk N)) ∙ ` zero) ∎
congsub≅ : ∀ {Γ Δ A} → {σ : Δ ⊢⋆ Γ} {M M′ : Γ ⊢ A}
→ M ≅ M′
→ sub σ M ≅ sub σ M′
congsub≅ refl≅ = refl≅
congsub≅ (sym≅ p) = sym≅ (congsub≅ p)
congsub≅ (trans≅ p q) = trans≅ (congsub≅ p) (congsub≅ q)
congsub≅ (congƛ≅ p) = congƛ≅ (congsub≅ p)
congsub≅ (cong∙≅ p q) = cong∙≅ (congsub≅ p) (congsub≅ q)
congsub≅ (redβ≅ σ M N) = congsubβ≅ σ M N
congsub≅ (expη≅ (` i)) = congsubη`≅ i
congsub≅ (expη≅ (ƛ M)) = congsubηƛ≅ M
congsub≅ (expη≅ (M ∙ N)) = congsubη∙≅ M N
--------------------------------------------------------------------------------
--
-- 7.1. Congruence of _≅⋆_
-- NOTE: Needs getₛ σ i ≅ getₛ σ′ i
-- cong◐≅⋆ : ∀ {Γ Δ Ξ} → {σ σ′ : Δ ⊢⋆ Γ} {η : Γ ∋⋆ Ξ}
-- → σ ≅⋆ σ′
-- → σ ◐ η ≅⋆ σ′ ◐ η
-- cong◐≅⋆ {η = []} ψ = []
-- cong◐≅⋆ {η = [ η , i ]} ψ = [ cong◐≅⋆ ψ , {!!} ]
cong◑≅⋆ : ∀ {Γ Δ Ξ} → {η : Δ ∋⋆ Γ} {σ σ′ : Γ ⊢⋆ Ξ}
→ σ ≅⋆ σ′
→ η ◑ σ ≅⋆ η ◑ σ′
cong◑≅⋆ [] = []
cong◑≅⋆ [ ψ , p ] = [ cong◑≅⋆ ψ , congsub≅ p ]
-- NOTE: Needs a more general congsub≅
-- cong●≅⋆ : ∀ {Γ Δ Ξ} → {σ₁ σ₁′ : Δ ⊢⋆ Γ} {σ₂ σ₂′ : Γ ⊢⋆ Ξ}
-- → σ₁ ≅⋆ σ₁′ → σ₂ ≅⋆ σ₂′
-- → σ₁ ● σ₂ ≅⋆ σ₁′ ● σ₂′
-- cong●≅⋆ ψ₁ [] = []
-- cong●≅⋆ ψ₁ [ ψ₂ , p ] = [ cong●≅⋆ ψ₁ ψ₂ , {!!} ]
--------------------------------------------------------------------------------
--
-- 8. Model
record 𝔐 : Set₁ where
field
𝒲 : Set
𝒢 : 𝒲 → Set
_⊒_ : 𝒲 → 𝒲 → Set
idₐ : ∀ {w} → w ⊒ w
_□_ : ∀ {w w′ w″} → w″ ⊒ w′ → w′ ⊒ w
→ w″ ⊒ w
id₁□ : ∀ {w w′} → (ξ : w′ ⊒ w)
→ idₐ □ ξ ≡ ξ
id₂□ : ∀ {w w′} → (ξ : w′ ⊒ w)
→ ξ □ idₐ ≡ ξ
assoc□ : ∀ {w w′ w″ w‴} → (ξ₁ : w‴ ⊒ w″) (ξ₂ : w″ ⊒ w′) (ξ₃ : w′ ⊒ w)
→ ξ₁ □ (ξ₂ □ ξ₃) ≡ (ξ₁ □ ξ₂) □ ξ₃
--------------------------------------------------------------------------------
--
-- 8.1. Semantic objects
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
infix 3 _⊩_
data _⊩_ : 𝒲 → 𝒯 → Set where
⟦G⟧ : ∀ {w} → (h : ∀ {w′} → (ξ : w′ ⊒ w)
→ 𝒢 w′)
→ w ⊩ •
⟦ƛ⟧ : ∀ {A B w} → (h : ∀ {w′} → (ξ : w′ ⊒ w) (a : w′ ⊩ A)
→ w′ ⊩ B)
→ w ⊩ A ⊃ B
⟦g⟧⟨_⟩ : ∀ {w w′} → w′ ⊒ w → w ⊩ •
→ 𝒢 w′
⟦g⟧⟨ ξ ⟩ (⟦G⟧ f) = f ξ
_◎⟨_⟩_ : ∀ {A B w w′} → w ⊩ A ⊃ B → w′ ⊒ w → w′ ⊩ A
→ w′ ⊩ B
(⟦ƛ⟧ f) ◎⟨ ξ ⟩ a = f ξ a
-- ⟦putᵣ⟧ can’t be stated here
-- ⟦getᵣ⟧ can’t be stated here
-- ⟦unwkᵣ⟧ can’t be stated here
-- ⟦wkᵣ⟧ can’t be stated here
-- ⟦liftᵣ⟧ can’t be stated here
-- idₐ = ⟦idᵣ⟧
-- acc = ⟦ren⟧
acc : ∀ {A w w′} → w′ ⊒ w → w ⊩ A
→ w′ ⊩ A
acc {•} ξ f = ⟦G⟧ (λ ξ′ → ⟦g⟧⟨ ξ′ □ ξ ⟩ f)
acc {A ⊃ B} ξ f = ⟦ƛ⟧ (λ ξ′ a → f ◎⟨ ξ′ □ ξ ⟩ a)
-- ⟦wk⟧ can’t be stated here
-- _□_ = _⟦○⟧_
--------------------------------------------------------------------------------
--
-- 8.2. Semantic equality
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
mutual
data Eq : ∀ {A w} → w ⊩ A → w ⊩ A → Set where
eq• : ∀ {w} → {f f′ : w ⊩ •}
→ (h : ∀ {w′} → (ξ : w′ ⊒ w)
→ ⟦g⟧⟨ ξ ⟩ f ≡ ⟦g⟧⟨ ξ ⟩ f′)
→ Eq f f′
eq⊃ : ∀ {A B w} → {f f′ : w ⊩ A ⊃ B}
→ (h : ∀ {w′} → (ξ : w′ ⊒ w) {a : w′ ⊩ A} (u : Un a)
→ Eq (f ◎⟨ ξ ⟩ a) (f′ ◎⟨ ξ ⟩ a))
→ Eq f f′
data Un : ∀ {A w} → w ⊩ A → Set where
un• : ∀ {w} → {f : w ⊩ •}
→ Un f
un⊃ : ∀ {A B w} → {f : w ⊩ A ⊃ B}
→ (h₁ : ∀ {w′} → (ξ : w′ ⊒ w) {a : w′ ⊩ A} (u : Un a)
→ Un (f ◎⟨ ξ ⟩ a))
→ (h₂ : ∀ {w′} → (ξ : w′ ⊒ w) {a a′ : w′ ⊩ A} (e : Eq a a′) (u₁ : Un a) (u₂ : Un a′)
→ Eq (f ◎⟨ ξ ⟩ a) (f ◎⟨ ξ ⟩ a′))
→ (h₃ : ∀ {w′ w″} → (ξ₁ : w″ ⊒ w′) (ξ₂ : w′ ⊒ w) {a : w′ ⊩ A} (u : Un a)
→ Eq (acc ξ₁ (f ◎⟨ ξ₂ ⟩ a)) (f ◎⟨ ξ₁ □ ξ₂ ⟩ (acc ξ₁ a)))
→ Un f
reflEq : ∀ {A w} → {a : w ⊩ A}
→ Un a
→ Eq a a
reflEq un• = eq• (λ ξ → refl)
reflEq (un⊃ h₁ h₂ h₃) = eq⊃ (λ ξ u → reflEq (h₁ ξ u))
symEq : ∀ {A w} → {a a′ : w ⊩ A}
→ Eq a a′
→ Eq a′ a
symEq {•} (eq• h) = eq• (λ ξ → sym (h ξ))
symEq {A ⊃ B} (eq⊃ h) = eq⊃ (λ ξ u → symEq (h ξ u))
transEq : ∀ {A w} → {a a′ a″ : w ⊩ A}
→ Eq a a′ → Eq a′ a″
→ Eq a a″
transEq {•} (eq• h₁) (eq• h₂) = eq• (λ ξ → trans (h₁ ξ) (h₂ ξ))
transEq {A ⊃ B} (eq⊃ h₁) (eq⊃ h₂) = eq⊃ (λ ξ u → transEq (h₁ ξ u) (h₂ ξ u))
≡→Eq : ∀ {A w} → {a a′ : w ⊩ A} → a ≡ a′ → Un a → Eq a a′
≡→Eq refl u = reflEq u
module Eq-Reasoning where
infix 1 begin_
begin_ : ∀ {A w} → {a a′ : w ⊩ A} → Eq a a′ → Eq a a′
begin e = e
infixr 2 _Eq⟨⟩_
_Eq⟨⟩_ : ∀ {A w} → (a {a′} : w ⊩ A) → Eq a a′ → Eq a a′
a Eq⟨⟩ e = e
infixr 2 _Eq⟨_⟩_
_Eq⟨_⟩_ : ∀ {A w} → (a {a′ a″} : w ⊩ A) → Eq a a′ → Eq a′ a″ → Eq a a″
a Eq⟨ e₁ ⟩ e₂ = transEq e₁ e₂
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ {A w} → (a {a′} : w ⊩ A) → Eq a a′ → Eq a a′
a ≡⟨⟩ e = e
infixr 2 _≡⟨_∣_⟩_
_≡⟨_∣_⟩_ : ∀ {A w} → (a {a′ a″} : w ⊩ A) → a ≡ a′ → Un a → Eq a′ a″ → Eq a a″
a ≡⟨ e₁ ∣ u ⟩ e₂ = transEq (≡→Eq e₁ u) e₂
infix 3 _∎⟨_⟩
_∎⟨_⟩ : ∀ {A w} → (a : w ⊩ A) → Un a → Eq a a
a ∎⟨ u ⟩ = reflEq u
--------------------------------------------------------------------------------
--
-- 8.3. Properties of semantic equality
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
-- cong◎Eq = cong◎⟨_⟩Eq
postulate
cong◎Eq : ∀ {A B w w′} → {f f′ : w ⊩ A ⊃ B} {a a′ : w′ ⊩ A}
→ (ξ : w′ ⊒ w) → Eq f f′ → Un f → Un f′ → Eq a a′ → Un a → Un a′
→ Eq (f ◎⟨ ξ ⟩ a)
(f′ ◎⟨ ξ ⟩ a′)
cong◎Un : ∀ {A B w w′} → {f : w ⊩ A ⊃ B} {a : w′ ⊩ A}
→ (ξ : w′ ⊒ w) → Un f → Un a
→ Un (f ◎⟨ ξ ⟩ a)
cong◎Un {f = f} {a} ξ (un⊃ h₁ h₂ h₃) u = h₁ ξ u
-- congaccEq = cong↑⟨_⟩Eq
postulate
congaccEq : ∀ {A w w′} → {a a′ : w ⊩ A}
→ (ξ : w′ ⊒ w) → Eq a a′
→ Eq (acc ξ a) (acc ξ a′)
-- congaccUn = cong↑⟨_⟩𝒰
postulate
congaccUn : ∀ {A w w′} → {a : w ⊩ A}
→ (ξ : w′ ⊒ w) → Un a
→ Un (acc ξ a)
-- id₁accEq = aux₄₁₁
postulate
id₁accEq : ∀ {A w} → {a : w ⊩ A}
→ Un a
→ Eq (acc idₐ a) a
-- acc□Eq = flip aux₄₁₂
postulate
acc□Eq : ∀ {A w w′ w″} → {a : w ⊩ A}
→ (ξ₁ : w″ ⊒ w′) (ξ₂ : w′ ⊒ w) → Un a
→ Eq (acc (ξ₁ □ ξ₂) a)
((acc ξ₁ ∘ acc ξ₂) a)
-- acc◎Eq = flip aux₄₁₃
postulate
acc◎idEq : ∀ {A B w w′} → {f : w ⊩ A ⊃ B} {a : w′ ⊩ A}
→ (ξ : w′ ⊒ w) → Un f → Un a
→ Eq (acc ξ f ◎⟨ idₐ ⟩ a)
(f ◎⟨ ξ ⟩ a)
acc◎Eq : ∀ {A B w w′ w″} → {f : w ⊩ A ⊃ B} {a : w′ ⊩ A}
→ (ξ₁ : w′ ⊒ w) (ξ₂ : w″ ⊒ w′) → Un f → Un a
→ Eq (acc ξ₁ f ◎⟨ ξ₂ ⟩ acc ξ₂ a)
(acc ξ₂ (f ◎⟨ ξ₁ ⟩ a))
acc◎Eq {f = f} {a} ξ₁ ξ₂ (un⊃ h₁ h₂ h₃) u = symEq (h₃ ξ₂ ξ₁ u)
--------------------------------------------------------------------------------
--
-- 8.4. Semantic environments
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
infix 3 _⊩⋆_
data _⊩⋆_ : 𝒲 → 𝒞 → Set where
[] : ∀ {w} →
w ⊩⋆ []
[_,_] : ∀ {Γ A w} →
(ρ : w ⊩⋆ Γ) (a : w ⊩ A) →
w ⊩⋆ [ Γ , A ]
-- ⟦putₛ⟧ can’t be stated here
-- getₑ = ⟦getₛ⟧ = lookup
getₑ : ∀ {Γ A w} → w ⊩⋆ Γ → Γ ∋ A
→ w ⊩ A
getₑ [ ρ , a ] zero = a
getₑ [ ρ , a ] (suc i) = getₑ ρ i
-- unwkₑ = ⟦unwkₛ⟧
unwkₑ : ∀ {Γ A w} → w ⊩⋆ [ Γ , A ]
→ w ⊩⋆ Γ
unwkₑ [ ρ , a ] = ρ
-- ⟦wkₛ⟧ can’t be stated here
-- ⟦liftₛ⟧ can’t be stated here
-- ⟦idₛ⟧ can’t be stated here
-- ⟦sub⟧ can’t be stated here
-- ⟦cut⟧ can’t be stated here
-- _■_ can’t be stated here
--------------------------------------------------------------------------------
--
-- 8.5. Compositions of renaming and semantic environments
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
-- _◨_ = ⟦_◑_⟧ = ↑⟨_⟩⊩⋆
_◨_ : ∀ {Γ w w′} → w′ ⊒ w → w ⊩⋆ Γ
→ w′ ⊩⋆ Γ
ξ ◨ [] = []
ξ ◨ [ ρ , a ] = [ ξ ◨ ρ , acc ξ a ]
-- _◧_ = ⟦_◐_⟧ = flip ↓⟨_⟩⊩⋆
_◧_ : ∀ {Γ Δ w} → w ⊩⋆ Δ → Δ ∋⋆ Γ
→ w ⊩⋆ Γ
ρ ◧ [] = []
ρ ◧ [ η , i ] = [ ρ ◧ η , getₑ ρ i ]
--------------------------------------------------------------------------------
--
-- 8.6. Basic properties of _◧_
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
zap◧ : ∀ {Γ Ξ A w} → (ρ : w ⊩⋆ Γ) (η : Γ ∋⋆ Ξ) (a : w ⊩ A)
→ [ ρ , a ] ◧ wkᵣ η ≡ ρ ◧ η
zap◧ ρ [] a = refl
zap◧ ρ [ η , i ] a = cong² [_,_] (zap◧ ρ η a) refl
id₂◧ : ∀ {Γ w} → (ρ : w ⊩⋆ Γ)
→ ρ ◧ idᵣ ≡ ρ
id₂◧ [] = refl
id₂◧ [ ρ , a ] = begin
[ [ ρ , a ] ◧ wkᵣ idᵣ , a ] ≡⟨ cong² [_,_] (zap◧ ρ idᵣ a) refl ⟩
[ ρ ◧ idᵣ , a ] ≡⟨ cong² [_,_] (id₂◧ ρ) refl ⟩
[ ρ , a ] ∎
where open ≡-Reasoning
--------------------------------------------------------------------------------
--
-- 8.7. Advanced properties of _◧_
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
get◧ : ∀ {Γ Ξ A w} → (ρ : w ⊩⋆ Γ) (η : Γ ∋⋆ Ξ) (i : Ξ ∋ A)
→ getₑ (ρ ◧ η) i ≡ (getₑ ρ ∘ getᵣ η) i
get◧ ρ [ η , j ] zero = refl
get◧ ρ [ η , j ] (suc i) = get◧ ρ η i
comp◧○ : ∀ {Γ Ξ Ω w} → (ρ : w ⊩⋆ Γ) (η₁ : Γ ∋⋆ Ξ) (η₂ : Ξ ∋⋆ Ω)
→ ρ ◧ (η₁ ○ η₂) ≡ (ρ ◧ η₁) ◧ η₂
comp◧○ σ η₁ [] = refl
comp◧○ σ η₁ [ η₂ , z ] = cong² [_,_] (comp◧○ σ η₁ η₂) (sym (get◧ σ η₁ z))
-- wk◧ can’t be stated here
-- lift◧ can’t be stated here
-- wkid₂◧ can’t be stated here
-- liftwkid₂◧ can’t be stated here
-- sub◧ can’t be stated here
-- subwk◧ can’t be stated here
-- sublift◧ can’t be stated here
-- subliftwk◧ can’t be stated here
--------------------------------------------------------------------------------
--
-- 8.8. Semantic equality of environments
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
data Eq⋆ : ∀ {Γ w} → w ⊩⋆ Γ → w ⊩⋆ Γ → Set where
[] : ∀ {w} → Eq⋆ ([] {w}) []
[_,_] : ∀ {Γ A w} → {ρ ρ′ : w ⊩⋆ Γ} {a a′ : w ⊩ A}
→ (ε : Eq⋆ ρ ρ′) (e : Eq a a′)
→ Eq⋆ [ ρ , a ] [ ρ′ , a′ ]
data Un⋆ : ∀ {Γ w} → w ⊩⋆ Γ → Set where
[] : ∀ {w} → Un⋆ ([] {w})
[_,_] : ∀ {Γ A w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
→ (υ : Un⋆ ρ) (u : Un a)
→ Un⋆ [ ρ , a ]
reflEq⋆ : ∀ {Γ w} → {ρ : w ⊩⋆ Γ}
→ Un⋆ ρ
→ Eq⋆ ρ ρ
reflEq⋆ [] = []
reflEq⋆ [ υ , u ] = [ reflEq⋆ υ , reflEq u ]
symEq⋆ : ∀ {Γ w} → {ρ ρ′ : w ⊩⋆ Γ}
→ Eq⋆ ρ ρ′
→ Eq⋆ ρ′ ρ
symEq⋆ [] = []
symEq⋆ [ ε , e ] = [ symEq⋆ ε , symEq e ]
transEq⋆ : ∀ {Γ w} → {ρ ρ′ ρ″ : w ⊩⋆ Γ}
→ Eq⋆ ρ ρ′ → Eq⋆ ρ′ ρ″
→ Eq⋆ ρ ρ″
transEq⋆ [] [] = []
transEq⋆ [ ε₁ , e₁ ] [ ε₂ , e₂ ] = [ transEq⋆ ε₁ ε₂ , transEq e₁ e₂ ]
≡→Eq⋆ : ∀ {Γ w} → {ρ ρ′ : w ⊩⋆ Γ} → ρ ≡ ρ′ → Un⋆ ρ → Eq⋆ ρ ρ′
≡→Eq⋆ refl υ = reflEq⋆ υ
module Eq⋆-Reasoning where
infix 1 begin_
begin_ : ∀ {Γ w} → {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
begin ε = ε
infixr 2 _Eq⋆⟨⟩_
_Eq⋆⟨⟩_ : ∀ {Γ w} → (ρ {ρ′} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
ρ Eq⋆⟨⟩ ε = ε
infixr 2 _Eq⋆⟨_⟩_
_Eq⋆⟨_⟩_ : ∀ {Γ w} → (ρ {ρ′ ρ″} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ′ ρ″ → Eq⋆ ρ ρ″
ρ Eq⋆⟨ ε₁ ⟩ ε₂ = transEq⋆ ε₁ ε₂
infixr 2 _≡⟨⟩_
_≡⟨⟩_ : ∀ {Γ w} → (ρ {ρ′} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
ρ ≡⟨⟩ ε = ε
infixr 2 _≡⟨_∣_⟩_
_≡⟨_∣_⟩_ : ∀ {Γ w} → (ρ {ρ′ ρ″} : w ⊩⋆ Γ) → ρ ≡ ρ′ → Un⋆ ρ → Eq⋆ ρ′ ρ″ → Eq⋆ ρ ρ″
ρ ≡⟨ ε₁ ∣ υ ⟩ ε₂ = transEq⋆ (≡→Eq⋆ ε₁ υ) ε₂
infix 3 _∎⟨_⟩
_∎⟨_⟩ : ∀ {Γ w} → (ρ : w ⊩⋆ Γ) → Un⋆ ρ → Eq⋆ ρ ρ
ρ ∎⟨ υ ⟩ = reflEq⋆ υ
--------------------------------------------------------------------------------
--
-- 8.9. Properties of semantic equality on environments
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
-- conggetEq = conglookupEq
postulate
conggetEq : ∀ {Γ A w} → {ρ ρ′ : w ⊩⋆ Γ}
→ (i : Γ ∋ A) → Eq⋆ ρ ρ′
→ Eq (getₑ ρ i) (getₑ ρ′ i)
-- cong◨Eq⋆ = cong↑⟨_⟩Eq⋆
postulate
cong◨Eq⋆ : ∀ {Γ w w′} → {ρ ρ′ : w ⊩⋆ Γ}
→ (ξ : w′ ⊒ w) → Eq⋆ ρ ρ′
→ Eq⋆ (ξ ◨ ρ) (ξ ◨ ρ′)
-- cong◧Eq⋆ = cong↓⟨_⟩Eq⋆
postulate
cong◧Eq⋆ : ∀ {Γ Δ w} → {ρ ρ′ : w ⊩⋆ Δ}
→ (η : Δ ∋⋆ Γ) → Eq⋆ ρ ρ′
→ Eq⋆ (ρ ◧ η) (ρ′ ◧ η)
-- conggetUn = conglookup𝒰
postulate
conggetUn : ∀ {Γ A w} → {ρ : w ⊩⋆ Γ}
→ (i : Γ ∋ A) → Un⋆ ρ
→ Un (getₑ ρ i)
-- cong◨Un⋆ = cong↑⟨_⟩𝒰⋆
postulate
cong◨Un⋆ : ∀ {Γ w w′} → {ρ : w ⊩⋆ Γ}
→ (ξ : w′ ⊒ w) → Un⋆ ρ
→ Un⋆ (ξ ◨ ρ)
-- cong◧Un⋆ = cong↓⟨_⟩𝒰⋆
postulate
cong◧Un⋆ : ∀ {Γ Δ w} → {ρ : w ⊩⋆ Δ}
→ (η : Δ ∋⋆ Γ) → Un⋆ ρ
→ Un⋆ (ρ ◧ η)
--------------------------------------------------------------------------------
--
-- TODO
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
-- get◧Eq = symEq ∘ aux₄₂₁
postulate
get◧Eq : ∀ {Γ Δ A w} → {ρ : w ⊩⋆ Δ}
→ (η : Δ ∋⋆ Γ) (i : Δ ∋ A) (j : Γ ∋ A) → Un⋆ ρ
→ Eq (getₑ (ρ ◧ η) j)
(getₑ ρ i)
-- get◨Eq = symEq conglookup↑⟨_⟩Eq
postulate
get◨Eq : ∀ {Γ A w w′} → {ρ : w ⊩⋆ Γ}
→ (ξ : w′ ⊒ w) (i : Γ ∋ A) → Un⋆ ρ
→ Eq (getₑ (ξ ◨ ρ) i)
(acc ξ (getₑ ρ i))
-- zap◧Eq⋆ = aux₄₂₃
postulate
zap◧Eq⋆ : ∀ {Γ Δ A w} → {ρ : w ⊩⋆ Δ} {a : w ⊩ A}
→ (η₁ : [ Δ , A ] ∋⋆ Γ) (η₂ : Δ ∋⋆ Γ) → Un⋆ ρ
→ Eq⋆ ([ ρ , a ] ◧ η₁)
(ρ ◧ η₂)
-- id₂◧Eq⋆ = aux₄₂₄
postulate
id₂◧Eq⋆ : ∀ {Γ w} → {ρ : w ⊩⋆ Γ}
→ Un⋆ ρ
→ Eq⋆ (ρ ◧ idᵣ) ρ
-- id₁◨Eq⋆ = aux₄₂₅
postulate
id₁◨Eq⋆ : ∀ {Γ w} → {ρ : w ⊩⋆ Γ}
→ Un⋆ ρ
→ Eq⋆ (idₐ ◨ ρ) ρ
-- comp◧○Eq⋆ = symEq⋆ ∘ aux₄₂₆
postulate
comp◧○Eq⋆ : ∀ {Γ Δ Ξ w} → {ρ : w ⊩⋆ Δ}
→ (η₁ : Δ ∋⋆ Γ) (η₂ : Γ ∋⋆ Ξ) → Un⋆ ρ
→ Eq⋆ (ρ ◧ (η₁ ○ η₂))
((ρ ◧ η₁) ◧ η₂)
-- comp◨□Eq⋆ = aux₄₂₇
postulate
comp◨□Eq⋆ : ∀ {Γ w w′ w″} → {ρ : w ⊩⋆ Γ}
→ (ξ₁ : w″ ⊒ w′) (ξ₂ : w′ ⊒ w) → Un⋆ ρ
→ Eq⋆ (ξ₁ ◨ (ξ₂ ◨ ρ))
((ξ₁ □ ξ₂) ◨ ρ)
-- comp◨◧Eq⋆ = flip aux₄₂₈
postulate
comp◨◧Eq⋆ : ∀ {Γ Δ w w′} → {ρ : w ⊩⋆ Δ}
→ (ξ : w′ ⊒ w) (η : Δ ∋⋆ Γ) → Un⋆ ρ
→ Eq⋆ (ξ ◨ (ρ ◧ η))
((ξ ◨ ρ) ◧ η)
--------------------------------------------------------------------------------
--
-- Evaluation
module _ {{𝔪 : 𝔐}} where
open 𝔐 𝔪
⟦_⟧ : ∀ {Γ A w} → Γ ⊢ A → w ⊩⋆ Γ
→ w ⊩ A
⟦ ` i ⟧ ρ = getₑ ρ i
⟦ ƛ M ⟧ ρ = ⟦ƛ⟧ (λ ξ a → ⟦ M ⟧ [ ξ ◨ ρ , a ])
⟦ M ∙ N ⟧ ρ = ⟦ M ⟧ ρ ◎⟨ idₐ ⟩ ⟦ N ⟧ ρ
⟦_⟧⋆ : ∀ {Γ Δ w} → Δ ⊢⋆ Γ → w ⊩⋆ Δ
→ w ⊩⋆ Γ
⟦ [] ⟧⋆ ρ = []
⟦ [ σ , M ] ⟧⋆ ρ = [ ⟦ σ ⟧⋆ ρ , ⟦ M ⟧ ρ ]
--------------------------------------------------------------------------------
instance
canon : 𝔐
canon = record
{ 𝒲 = 𝒞
; 𝒢 = _⊢ •
; _⊒_ = _∋⋆_
; idₐ = idᵣ
; _□_ = _○_
; id₁□ = id₁○
; id₂□ = id₂○
; assoc□ = assoc○
}
--------------------------------------------------------------------------------
mutual
reify : ∀ {A Γ} → Γ ⊩ A
→ Γ ⊢ A
reify {•} f = ⟦g⟧⟨ idᵣ ⟩ f
reify {A ⊃ B} f = ƛ (reify (f ◎⟨ wkᵣ idᵣ ⟩ ⟪` zero ⟫))
⟪_⟫ : ∀ {A Γ} → (∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A)
→ Γ ⊩ A
⟪_⟫ {•} f = ⟦G⟧ (λ η → f η)
⟪_⟫ {A ⊃ B} f = ⟦ƛ⟧ (λ η a → ⟪ (λ η′ → f (η′ ○ η) ∙ reify (acc η′ a)) ⟫)
⟪`_⟫ : ∀ {Γ A} → Γ ∋ A
→ Γ ⊩ A
⟪` i ⟫ = ⟪ (λ η → ren η (` i)) ⟫
postulate
aux₄₄₁ : ∀ {A Γ} → (f f′ : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A)
→ (∀ {Δ} → (η : Δ ∋⋆ Γ) → f η ≡ f′ η)
→ Eq (⟪ f ⟫) (⟪ f′ ⟫)
postulate
aux₄₄₂ : ∀ {A Γ Δ} → (η : Δ ∋⋆ Γ) (f : (∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A))
→ Eq (acc η ⟪ f ⟫) (⟪ (λ η′ → f (η′ ○ η)) ⟫)
--------------------------------------------------------------------------------
-- Theorem 1.
mutual
postulate
thm₁ : ∀ {Γ A} → {a a′ : Γ ⊩ A}
→ Eq a a′
→ reify a ≡ reify a′
postulate
⟪`_⟫ᵤ : ∀ {Γ A} → (i : Γ ∋ A)
→ Un (⟪` i ⟫)
postulate
aux₄₄₃ : ∀ {A Γ} → (f : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A)
→ Un (⟪ f ⟫)
--------------------------------------------------------------------------------
⌊_⌋ₑ : ∀ {Γ Δ} → Δ ∋⋆ Γ
→ Δ ⊩⋆ Γ
⌊ [] ⌋ₑ = []
⌊ [ η , i ] ⌋ₑ = [ ⌊ η ⌋ₑ , ⟪` i ⟫ ]
idₑ : ∀ {Γ} → Γ ⊩⋆ Γ
idₑ = ⌊ idᵣ ⌋ₑ
nf : ∀ {Γ A} → Γ ⊢ A
→ Γ ⊢ A
nf M = reify (⟦ M ⟧ idₑ)
-- Corollary 1.
postulate
cor₁ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ idₑ) (⟦ M′ ⟧ idₑ)
→ nf M ≡ nf M′
--------------------------------------------------------------------------------
--
-- TODO
data CV : ∀ {Γ A} → Γ ⊢ A → Γ ⊩ A → Set where
cv• : ∀ {Γ} → {M : Γ ⊢ •} {f : Γ ⊩ •}
→ (h : ∀ {Δ} → (η : Δ ∋⋆ Γ)
→ sub ⌊ η ⌋ M ≅ ⟦g⟧⟨ η ⟩ f)
→ CV M f
cv⊃ : ∀ {Γ A B} → {M : Γ ⊢ A ⊃ B} {f : Γ ⊩ A ⊃ B}
→ (h : ∀ {Δ N a} → (η : Δ ∋⋆ Γ) → CV N a
→ CV (sub ⌊ η ⌋ M ∙ N) (f ◎⟨ η ⟩ a))
→ CV M f
data CV⋆ : ∀ {Γ Δ} → Δ ⊢⋆ Γ → Δ ⊩⋆ Γ → Set where
[] : ∀ {Γ} → {σ : Γ ⊢⋆ []}
→ CV⋆ σ []
[_,_] : ∀ {Γ Δ A} → {σ : Δ ⊢⋆ [ Γ , A ]} {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A}
→ (κ : CV⋆ (σ ◐ wkᵣ {A} idᵣ) ρ) (k : CV (sub σ (` zero)) a)
→ CV⋆ σ [ ρ , a ]
--------------------------------------------------------------------------------
postulate
congCV : ∀ {Γ A} → {M M′ : Γ ⊢ A} {a : Γ ⊩ A}
→ M ≅ M′ → CV M′ a
→ CV M a
-- cong↑⟨_⟩CV
postulate
accCV : ∀ {Γ Δ A} → {M : Γ ⊢ A} {a : Γ ⊩ A}
→ (η : Δ ∋⋆ Γ) → CV M a
→ CV (sub ⌊ η ⌋ M) (acc η a)
-- flip conglookupCV
postulate
getCV : ∀ {Γ Δ A} → {σ : Δ ⊢⋆ Γ} {ρ : Δ ⊩⋆ Γ}
→ (i : Γ ∋ A) → CV⋆ σ ρ
→ CV (sub σ (` i)) (getₑ ρ i)
-- cong↑⟨_⟩CV⋆
postulate
accCV⋆ : ∀ {Γ Δ Ξ} → {σ : Γ ⊢⋆ Ξ} {ρ : Γ ⊩⋆ Ξ}
→ (η : Δ ∋⋆ Γ) → CV⋆ σ ρ
→ CV⋆ (η ◑ σ) (η ◨ ρ)
-- cong↓⟨_⟩CV⋆
postulate
getCV⋆ : ∀ {Γ Δ Ξ} → {σ : Δ ⊢⋆ Γ} {ρ : Δ ⊩⋆ Γ}
→ (η : Γ ∋⋆ Ξ) → CV⋆ σ ρ
→ CV⋆ (σ ◐ η) (ρ ◧ η)
--------------------------------------------------------------------------------
-- Lemma 8.
postulate
⟦_⟧CV : ∀ {Γ Δ A} → {σ : Δ ⊢⋆ Γ} {ρ : Δ ⊩⋆ Γ}
→ (M : Γ ⊢ A) → CV⋆ σ ρ
→ CV (sub σ M) (⟦ M ⟧ ρ)
postulate
⟦_⟧CV⋆ : ∀ {Γ Δ Ξ} → {σ₁ : Δ ⊢⋆ Γ} {ρ : Δ ⊩⋆ Γ}
→ (σ₂ : Γ ⊢⋆ Ξ) → CV⋆ σ₁ ρ
→ CV⋆ (σ₁ ● σ₂) (⟦ σ₂ ⟧⋆ ρ)
--------------------------------------------------------------------------------
-- Lemma 9.
mutual
postulate
lem₉ : ∀ {Γ A} → {M : Γ ⊢ A} {a : Γ ⊩ A}
→ CV M a
→ M ≅ reify a
postulate
aux₄₆₈ : ∀ {A Γ} → {M : Γ ⊢ A} {f : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A}
→ (∀ {Δ} → (η : Δ ∋⋆ Γ) → sub ⌊ η ⌋ M ≅ f η)
→ CV M (⟪ f ⟫)
postulate
⌊_⌋ₖ : ∀ {Γ Δ} → (η : Δ ∋⋆ Γ)
→ CV⋆ ⌊ η ⌋ ⌊ η ⌋ₑ
idₖ : ∀ {Γ} → CV⋆ ⌊ idᵣ ⌋ (idₑ {Γ})
idₖ = ⌊ idᵣ ⌋ₖ
postulate
aux₄₆₉ : ∀ {Γ A} → (M : Γ ⊢ A)
→ sub ⌊ idᵣ ⌋ M ≅ nf M
--------------------------------------------------------------------------------
-- Theorem 2.
postulate
thm₂ : ∀ {Γ A} → (M : Γ ⊢ A)
→ M ≅ nf M
-- Theorem 3.
thm₃ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ idₑ) (⟦ M′ ⟧ idₑ)
→ M ≅ M′
thm₃ M M′ e =
begin
M
≅⟨ thm₂ M ⟩
nf M
≡⟨ cor₁ M M′ e ⟩
nf M′
≅⟨ sym≅ (thm₂ M′) ⟩
M′
∎
where open ≅-Reasoning
--------------------------------------------------------------------------------
reify⋆ : ∀ {Γ Δ} → Δ ⊩⋆ Γ
→ Δ ⊢⋆ Γ
reify⋆ [] = []
reify⋆ [ ρ , a ] = [ reify⋆ ρ , reify a ]
nf⋆ : ∀ {Γ Δ} → Δ ⊢⋆ Γ
→ Δ ⊢⋆ Γ
nf⋆ σ = reify⋆ (⟦ σ ⟧⋆ idₑ)
thm₁⋆ : ∀ {Γ Δ} → {ρ ρ′ : Δ ⊩⋆ Γ}
→ Eq⋆ ρ ρ′
→ reify⋆ ρ ≡ reify⋆ ρ′
thm₁⋆ [] = refl
thm₁⋆ [ ε , e ] = cong² [_,_] (thm₁⋆ ε) (thm₁ e)
cor₁⋆ : ∀ {Γ Δ} → (σ σ′ : Δ ⊢⋆ Γ) → Eq⋆ (⟦ σ ⟧⋆ idₑ) (⟦ σ′ ⟧⋆ idₑ)
→ nf⋆ σ ≡ nf⋆ σ′
cor₁⋆ σ σ′ = thm₁⋆
-- TODO: Do we need _≅⋆_?
-- lem₉⋆ : ∀ {Γ Δ} → {σ : Δ ⊢⋆ Γ} {ρ : Δ ⊩⋆ Γ}
-- → CV⋆ σ ρ
-- → σ ≅⋆ reify⋆ ρ
-- lem₉⋆ [] = {!!}
-- lem₉⋆ [ κ , k ] = {!!}
-- aux₄₆₉⋆⟨_⟩ : ∀ {Γ Δ} → (c : Δ ⊇ Δ) (γ : Δ ⋙ Γ)
-- → γ ● π⟨ c ⟩ ≅⋆ nf⋆ γ
-- thm₂⋆ : ∀ {Γ Δ} → (γ : Δ ⋙ Γ)
-- → γ ≅⋆ nf⋆ γ
-- thm₃⋆ : ∀ {Γ Δ} → (γ γ′ : Δ ⋙ Γ) → Eq⋆ (⟦ γ ⟧⋆ refl⊩⋆) (⟦ γ′ ⟧⋆ refl⊩⋆)
-- → γ ≅⋆ γ′
--------------------------------------------------------------------------------
--
-- TODO
module _ where
open Eq-Reasoning
-- Un⟦_⟧
postulate
⟦_⟧Un : ∀ {Γ Δ A} → {ρ : Δ ⊩⋆ Γ}
→ (M : Γ ⊢ A) → Un⋆ ρ
→ Un (⟦ M ⟧ ρ)
-- 𝒰⋆⟦_⟧ₛ
postulate
⟦_⟧Un⋆ : ∀ {Γ Δ Ξ} → {ρ : Δ ⊩⋆ Γ}
→ (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ
→ Un⋆ (⟦ σ ⟧⋆ ρ)
postulate
⟦_⟧Eq : ∀ {Γ Δ A} → {ρ ρ′ : Δ ⊩⋆ Γ}
→ (M : Γ ⊢ A) → Eq⋆ ρ ρ′ → Un⋆ ρ → Un⋆ ρ′
→ Eq (⟦ M ⟧ ρ) (⟦ M ⟧ ρ′)
-- Eq⋆⟦_⟧ₛ
postulate
⟦_⟧Eq⋆ : ∀ {Γ Δ Ξ} → {ρ ρ′ : Δ ⊩⋆ Γ}
→ (σ : Γ ⊢⋆ Ξ) → Eq⋆ ρ ρ′ → Un⋆ ρ → Un⋆ ρ′
→ Eq⋆ (⟦ σ ⟧⋆ ρ) (⟦ σ ⟧⋆ ρ′)
-- ⟦_⟧◨Eq = symEq ∘ ↑⟨_⟩Eq⟦_⟧
⟦_⟧◨Eq : ∀ {Γ Δ Ω A} → {ρ : Δ ⊩⋆ Γ}
→ (M : Γ ⊢ A) (η : Ω ∋⋆ Δ) → Un⋆ ρ
→ Eq (⟦ M ⟧ (η ◨ ρ))
(acc η (⟦ M ⟧ ρ))
⟦_⟧◨Eq {ρ = ρ} (` i) η υ = get◨Eq η i υ
⟦_⟧◨Eq {ρ = ρ} (ƛ M) η υ = begin
⟦ƛ⟧ (λ η′ a → ⟦ M ⟧ [ η′ ◨ (η ◨ ρ) , a ]) Eq⟨ eq⊃ (λ η′ u → ⟦ M ⟧Eq [ comp◨□Eq⋆ η′ η υ , reflEq u ]
[ cong◨Un⋆ η′ (cong◨Un⋆ η υ) , u ]
[ cong◨Un⋆ (η′ ○ η) υ , u ]) ⟩
⟦ƛ⟧ (λ η′ a → ⟦ M ⟧ [ (η′ ○ η) ◨ ρ , a ]) ∎⟨ un⊃ (λ η″ u → ⟦ M ⟧Un [ cong◨Un⋆ (η″ ○ η) υ , u ])
(λ η″ e u₁ u₂ → ⟦ M ⟧Eq [ cong◨Eq⋆ (η″ ○ η) (reflEq⋆ υ) , e ]
[ cong◨Un⋆ (η″ ○ η) υ , u₁ ]
[ cong◨Un⋆ (η″ ○ η) υ , u₂ ])
(λ η″₁ η″₂ {a} u → begin
acc η″₁ (⟦ M ⟧ [ (η″₂ ○ η) ◨ ρ , a ]) Eq⟨ symEq (⟦ M ⟧◨Eq η″₁ [ cong◨Un⋆ (η″₂ ○ η) υ , u ]) ⟩
⟦ M ⟧ (η″₁ ◨ [ (η″₂ ○ η) ◨ ρ , a ]) Eq⟨ ⟦ M ⟧Eq [ comp◨□Eq⋆ η″₁ (η″₂ ○ η) υ , reflEq (congaccUn η″₁ u) ]
[ cong◨Un⋆ η″₁ (cong◨Un⋆ (η″₂ ○ η) υ) , congaccUn η″₁ u ]
[ cong◨Un⋆ (η″₁ ○ (η″₂ ○ η)) υ , (congaccUn η″₁ u) ] ⟩
⟦ M ⟧ [ (η″₁ ○ (η″₂ ○ η)) ◨ ρ , acc η″₁ a ] ≡⟨ cong² ⟦_⟧ (refl {x = M}) (cong² [_,_] (cong² _◨_ (assoc○ η″₁ η″₂ η) refl) refl)
∣ ⟦ M ⟧Un [ cong◨Un⋆ (η″₁ ○ (η″₂ ○ η)) υ , congaccUn η″₁ u ] ⟩
⟦ M ⟧ [ ((η″₁ ○ η″₂) ○ η) ◨ ρ , acc η″₁ a ] ∎⟨ ⟦ M ⟧Un [ cong◨Un⋆ ((η″₁ ○ η″₂) ○ η) υ , congaccUn η″₁ u ] ⟩) ⟩
⟦_⟧◨Eq {ρ = ρ} (M ∙ N) η υ = begin
⟦ M ⟧ (η ◨ ρ) ◎⟨ idᵣ ⟩ ⟦ N ⟧ (η ◨ ρ) Eq⟨ cong◎Eq idᵣ (⟦ M ⟧◨Eq η υ) (⟦ M ⟧Un (cong◨Un⋆ η υ)) (congaccUn η (⟦ M ⟧Un υ))
(⟦ N ⟧◨Eq η υ) (⟦ N ⟧Un (cong◨Un⋆ η υ)) (congaccUn η (⟦ N ⟧Un υ)) ⟩
acc η (⟦ M ⟧ ρ) ◎⟨ idᵣ ⟩ acc η (⟦ N ⟧ ρ) Eq⟨ acc◎idEq η (⟦ M ⟧Un υ) (congaccUn η (⟦ N ⟧Un υ)) ⟩
⟦ M ⟧ ρ ◎⟨ η ⟩ acc η (⟦ N ⟧ ρ) Eq⟨ cong◎Eq η (symEq (id₁accEq (⟦ M ⟧Un υ))) (⟦ M ⟧Un υ) (congaccUn idᵣ (⟦ M ⟧Un υ))
(reflEq (congaccUn η (⟦ N ⟧Un υ))) (congaccUn η (⟦ N ⟧Un υ)) (congaccUn η (⟦ N ⟧Un υ)) ⟩
acc idᵣ (⟦ M ⟧ ρ) ◎⟨ η ⟩ acc η (⟦ N ⟧ ρ) Eq⟨ acc◎Eq idᵣ η (⟦ M ⟧Un υ) (⟦ N ⟧Un υ) ⟩
acc η (⟦ M ⟧ ρ ◎⟨ idᵣ ⟩ ⟦ N ⟧ ρ) ∎⟨ congaccUn η (cong◎Un idᵣ (⟦ M ⟧Un υ) (⟦ N ⟧Un υ)) ⟩
-- ⟦_⟧◨Eq⋆ = symEq ∘ ↑⟨_⟩Eq⋆⟦_⟧ₛ
⟦_⟧◨Eq⋆ : ∀ {Γ Δ Ξ Ω} → {ρ : Δ ⊩⋆ Γ}
→ (σ : Γ ⊢⋆ Ξ) (η : Ω ∋⋆ Δ) → Un⋆ ρ
→ Eq⋆ (⟦ σ ⟧⋆ (η ◨ ρ))
(η ◨ ⟦ σ ⟧⋆ ρ)
⟦_⟧◨Eq⋆ {ρ = ρ} [] η υ = []
⟦_⟧◨Eq⋆ {ρ = ρ} [ σ , M ] η υ = [ ⟦ σ ⟧◨Eq⋆ η υ , ⟦ M ⟧◨Eq η υ ]
--------------------------------------------------------------------------------
-- TODO: Generalise to zap◧
postulate
aux₄₈₁ : ∀ {Γ Δ A} → {ρ : Δ ⊩⋆ Γ} {a : Δ ⊩ A}
→ Un⋆ ρ
→ Eq⋆ ([ ρ , a ] ◧ wkᵣ idᵣ) ρ
-- TODO
-- Basic properties of _□_
-- Advanced properties of _□_
-- Basic properties of _◨_
-- Basic properties of _■_
-- Advanced properties of _◨_
-- Advanced properties of _■_
--------------------------------------------------------------------------------
-- TODO: Fix the instance argument problem; abstract over models; rename η to ξ
module _ where
open Eq-Reasoning
--------------------------------------------------------------------------------
renlift⟦_⟧Eq : ∀ {Γ Δ A B w w′} → {ρ : w ⊩⋆ Δ} {a : w′ ⊩ A}
→ (M : [ Γ , A ] ⊢ B) (η₁ : Δ ∋⋆ Γ) (η₂ : w′ ∋⋆ w) → Un⋆ ρ → Un a
→ Eq (⟦ ren (liftᵣ {A} η₁) M ⟧ [ η₂ ◨ ρ , a ])
(⟦ M ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ])
renlift⟦_⟧Eq {ρ = ρ} {a} (` zero) η₁ η₂ υ u = reflEq u
renlift⟦_⟧Eq {ρ = ρ} {a} (` (suc i)) η₁ η₂ υ u = begin
⟦ ren (liftᵣ η₁) (` (suc i)) ⟧ [ η₂ ◨ ρ , a ] ≡⟨⟩
getₑ [ η₂ ◨ ρ , a ] (getᵣ (wkᵣ η₁) i) ≡⟨ cong² getₑ refl (wkgetᵣ η₁ i) ∣ conggetUn (getᵣ (wkᵣ η₁) i) [ cong◨Un⋆ η₂ υ , u ] ⟩
getₑ [ η₂ ◨ ρ , a ] (suc (getᵣ η₁ i)) ≡⟨⟩
getₑ (η₂ ◨ ρ) (getᵣ η₁ i) Eq⟨ symEq (get◧Eq η₁ (getᵣ η₁ i) i (cong◨Un⋆ η₂ υ)) ⟩
getₑ ((η₂ ◨ ρ) ◧ η₁) i Eq⟨ conggetEq i (symEq⋆ (comp◨◧Eq⋆ η₂ η₁ υ)) ⟩
getₑ (η₂ ◨ (ρ ◧ η₁)) i ≡⟨⟩
⟦ ` (suc i) ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ] ∎⟨ ⟦ ` (suc i) ⟧Un [ cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ) , u ] ⟩
renlift⟦_⟧Eq {ρ = ρ} {a} (ƛ M) η₁ η₂ υ u = begin
⟦ ren (liftᵣ η₁) (ƛ M) ⟧ [ η₂ ◨ ρ , a ] ≡⟨⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ ren (liftᵣ (liftᵣ η₁)) M ⟧ [ [ η′ ◨ (η₂ ◨ ρ) , acc η′ a ] , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → renlift⟦ M ⟧Eq (liftᵣ η₁) η′ [ cong◨Un⋆ η₂ υ , u ] u′) ⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ M ⟧ [ η′ ◨ ([ η₂ ◨ ρ , a ] ◧ (liftᵣ η₁)) , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → ⟦ M ⟧Eq [ [ cong◨Eq⋆ η′ (symEq⋆ (transEq⋆ (comp◨◧Eq⋆ η₂ η₁ υ)
(symEq⋆ (zap◧Eq⋆ (wkᵣ η₁) η₁ (cong◨Un⋆ η₂ υ))))) , reflEq (congaccUn η′ u) ] , reflEq u′ ]
[ [ cong◨Un⋆ η′ (cong◧Un⋆ (wkᵣ η₁) [ cong◨Un⋆ η₂ υ , u ]) , congaccUn η′ u ] , u′ ]
[ [ cong◨Un⋆ η′ (cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ)) , congaccUn η′ u ] , u′ ]) ⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ M ⟧ [ [ η′ ◨ (η₂ ◨ (ρ ◧ η₁)) , acc η′ a ] , a′ ]) ≡⟨⟩
⟦ ƛ M ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ] ∎⟨ ⟦ ƛ M ⟧Un [ cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ) , u ] ⟩
renlift⟦_⟧Eq {ρ = ρ} {a} (M ∙ N) η₁ η₂ υ u = begin
⟦ ren (liftᵣ η₁) (M ∙ N) ⟧ [ η₂ ◨ ρ , a ] ≡⟨⟩
⟦ ren (liftᵣ η₁) M ⟧ [ η₂ ◨ ρ , a ] ◎⟨ idᵣ ⟩ ⟦ ren (liftᵣ η₁) N ⟧ [ η₂ ◨ ρ , a ] Eq⟨ cong◎Eq idᵣ (renlift⟦ M ⟧Eq η₁ η₂ υ u) (⟦ ren (liftᵣ η₁) M ⟧Un [ cong◨Un⋆ η₂ υ , u ]) (⟦ M ⟧Un [ cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ) , u ])
(renlift⟦ N ⟧Eq η₁ η₂ υ u) (⟦ ren (liftᵣ η₁) N ⟧Un [ cong◨Un⋆ η₂ υ , u ]) (⟦ N ⟧Un [ cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ) , u ]) ⟩
⟦ M ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ] ◎⟨ idᵣ ⟩ ⟦ N ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ] ≡⟨⟩
⟦ M ∙ N ⟧ [ η₂ ◨ (ρ ◧ η₁) , a ] ∎⟨ ⟦ M ∙ N ⟧Un [ cong◨Un⋆ η₂ (cong◧Un⋆ η₁ υ) , u ] ⟩
--------------------------------------------------------------------------------
renwk⟦_⟧Eq : ∀ {Γ Δ A C w} → {ρ : w ⊩⋆ Δ} {a : w ⊩ A}
→ (M : Γ ⊢ C) (η : Δ ∋⋆ Γ) → Un⋆ ρ → Un a
→ Eq (⟦ ren (wkᵣ {A} η) M ⟧ [ ρ , a ])
(⟦ M ⟧ (ρ ◧ η))
renwk⟦_⟧Eq {ρ = ρ} {a} (` i) η υ u = begin
⟦ ren (wkᵣ η) (` i) ⟧ [ ρ , a ] ≡⟨⟩
getₑ [ ρ , a ] (getᵣ (wkᵣ η) i) Eq⟨ symEq (get◧Eq (wkᵣ η) (getᵣ (wkᵣ η) i) i [ υ , u ]) ⟩
getₑ ([ ρ , a ] ◧ wkᵣ η) i Eq⟨ conggetEq i (zap◧Eq⋆ (wkᵣ η) η υ) ⟩
getₑ (ρ ◧ η) i ≡⟨⟩
⟦ ` i ⟧ (ρ ◧ η) ∎⟨ ⟦ ` i ⟧Un (cong◧Un⋆ η υ) ⟩
renwk⟦_⟧Eq {ρ = ρ} {a} (ƛ M) η υ u = begin
⟦ ren (wkᵣ η) (ƛ M) ⟧ [ ρ , a ] ≡⟨⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ ren (liftᵣ (wkᵣ η)) M ⟧ [ [ η′ ◨ ρ , acc η′ a ] , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → renlift⟦ M ⟧Eq (wkᵣ η) η′ [ υ , u ] u′) ⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ M ⟧ [ η′ ◨ ([ ρ , a ] ◧ wkᵣ η) , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → ⟦ M ⟧Eq [ cong◨Eq⋆ η′ (zap◧Eq⋆ (wkᵣ η) η υ) , reflEq u′ ]
[ cong◨Un⋆ η′ (cong◧Un⋆ (wkᵣ η) [ υ , u ]) , u′ ]
[ cong◨Un⋆ η′ (cong◧Un⋆ η υ) , u′ ]) ⟩
⟦ƛ⟧ (λ η′ a′ → ⟦ M ⟧ [ η′ ◨ (ρ ◧ η) , a′ ]) ≡⟨⟩
⟦ ƛ M ⟧ (ρ ◧ η) ∎⟨ ⟦ ƛ M ⟧Un (cong◧Un⋆ η υ) ⟩
renwk⟦_⟧Eq {ρ = ρ} {a} (M ∙ N) η υ u = begin
⟦ ren (wkᵣ η) (M ∙ N) ⟧ [ ρ , a ] ≡⟨⟩
(⟦ ren (wkᵣ η) M ⟧ [ ρ , a ] ◎⟨ idᵣ ⟩ ⟦ ren (wkᵣ η) N ⟧ [ ρ , a ]) Eq⟨ cong◎Eq idᵣ (renwk⟦ M ⟧Eq η υ u) (⟦ ren (wkᵣ η) M ⟧Un [ υ , u ]) (⟦ M ⟧Un (cong◧Un⋆ η υ))
(renwk⟦ N ⟧Eq η υ u) (⟦ ren (wkᵣ η) N ⟧Un [ υ , u ]) (⟦ N ⟧Un (cong◧Un⋆ η υ)) ⟩
(⟦ M ⟧ (ρ ◧ η) ◎⟨ idᵣ ⟩ ⟦ N ⟧ (ρ ◧ η)) ≡⟨⟩
⟦ M ∙ N ⟧ (ρ ◧ η) ∎⟨ ⟦ M ∙ N ⟧Un (cong◧Un⋆ η υ) ⟩
--------------------------------------------------------------------------------
wk⟦_⟧Eq : ∀ {Γ A C w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
→ (M : Γ ⊢ C) → Un⋆ ρ → Un a
→ Eq (⟦ wk {A} M ⟧ [ ρ , a ])
(⟦ M ⟧ ρ)
wk⟦_⟧Eq {ρ = ρ} {a} M υ u = begin
⟦ wk M ⟧ [ ρ , a ] Eq⟨ renwk⟦ M ⟧Eq idᵣ υ u ⟩
⟦ M ⟧ (ρ ◧ idᵣ) Eq⟨ ⟦ M ⟧Eq (id₂◧Eq⋆ υ) (cong◧Un⋆ idᵣ υ) υ ⟩
⟦ M ⟧ ρ ∎⟨ ⟦ M ⟧Un υ ⟩
wk⟦_⟧Eq⋆ : ∀ {Γ Ξ A w} → {ρ : w ⊩⋆ Γ} {a : w ⊩ A}
→ (σ : Γ ⊢⋆ Ξ) → Un⋆ ρ → Un a
→ Eq⋆ (⟦ wkₛ {A} σ ⟧⋆ [ ρ , a ])
(⟦ σ ⟧⋆ ρ)
wk⟦_⟧Eq⋆ {ρ = ρ} {a} [] υ u = []
wk⟦_⟧Eq⋆ {ρ = ρ} {a} [ σ , M ] υ u = [ wk⟦ σ ⟧Eq⋆ υ u , wk⟦ M ⟧Eq υ u ]
--------------------------------------------------------------------------------
get⟦_⟧Eq : ∀ {Γ Δ A w} → {ρ : w ⊩⋆ Δ}
→ (σ : Δ ⊢⋆ Γ) (i : Γ ∋ A) → Un⋆ ρ
→ Eq (⟦ getₛ σ i ⟧ ρ)
(getₑ (⟦ σ ⟧⋆ ρ) i)
get⟦_⟧Eq {ρ = ρ} [ σ , M ] zero υ = reflEq (⟦ M ⟧Un υ)
get⟦_⟧Eq {ρ = ρ} [ σ , M ] (suc i) υ = get⟦ σ ⟧Eq i υ
--------------------------------------------------------------------------------
sublift⟦_⟧Eq : ∀ {Γ Δ A B w} → {ρ : w ⊩⋆ Δ} {a : w ⊩ A}
→ (M : [ Γ , A ] ⊢ B) (σ : Δ ⊢⋆ Γ) → Un⋆ ρ → Un a
→ Eq (⟦ sub (liftₛ {A} σ) M ⟧ [ ρ , a ])
(⟦ M ⟧ [ ⟦ σ ⟧⋆ ρ , a ])
sublift⟦_⟧Eq {ρ = ρ} {a} (` zero) σ υ u = reflEq u
sublift⟦_⟧Eq {ρ = ρ} {a} (` (suc i)) σ υ u = begin
⟦ getₛ (wkₛ σ) i ⟧ [ ρ , a ] ≡⟨ cong² ⟦_⟧ (wkgetₛ σ i) refl ∣ ⟦ getₛ (wkₛ σ) i ⟧Un [ υ , u ] ⟩
⟦ wk (getₛ σ i) ⟧ [ ρ , a ] Eq⟨ wk⟦ getₛ σ i ⟧Eq υ u ⟩
⟦ getₛ σ i ⟧ ρ Eq⟨ get⟦ σ ⟧Eq i υ ⟩
getₑ (⟦ σ ⟧⋆ ρ) i ∎⟨ conggetUn i (⟦ σ ⟧Un⋆ υ) ⟩
sublift⟦_⟧Eq {ρ = ρ} {a} (ƛ M) σ υ u = begin
⟦ƛ⟧ (λ η a′ → ⟦ sub (liftₛ (liftₛ σ)) M ⟧ [ [ η ◨ ρ , acc η a ] , a′ ]) ≡⟨⟩
⟦ƛ⟧ (λ η a′ → ⟦ sub (liftₛ (liftₛ σ)) M ⟧ [ η ◨ [ ρ , a ] , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → sublift⟦ M ⟧Eq (liftₛ σ) [ cong◨Un⋆ η′ υ , congaccUn η′ u ] u′) ⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ ⟦ liftₛ σ ⟧⋆ (η ◨ [ ρ , a ]) , a′ ]) Eq⟨ eq⊃ (λ η′ u′ → ⟦ M ⟧Eq [ [ ⟦ wkₛ σ ⟧◨Eq⋆ η′ [ υ , u ] , reflEq (congaccUn η′ u) ] , reflEq u′ ]
[ [ ⟦ wkₛ σ ⟧Un⋆ [ cong◨Un⋆ η′ υ , congaccUn η′ u ] , congaccUn η′ u ] , u′ ]
[ [ cong◨Un⋆ η′ (⟦ wkₛ σ ⟧Un⋆ [ υ , u ]) , congaccUn η′ u ] , u′ ]) ⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ η ◨ ⟦ liftₛ σ ⟧⋆ [ ρ , a ] , a′ ]) ≡⟨⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ η ◨ ⟦ [ wkₛ σ , ` zero ] ⟧⋆ [ ρ , a ] , a′ ]) ≡⟨⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ η ◨ [ ⟦ wkₛ σ ⟧⋆ [ ρ , a ] , ⟦ ` zero ⟧ [ ρ , a ] ] , a′ ]) Eq⟨ eq⊃ (λ η u′ → ⟦ M ⟧Eq [ [ cong◨Eq⋆ η (wk⟦ σ ⟧Eq⋆ υ u) , reflEq (congaccUn η u) ] , reflEq u′ ]
[ [ cong◨Un⋆ η (⟦ wkₛ σ ⟧Un⋆ [ υ , u ]) , congaccUn η u ] , u′ ]
[ [ cong◨Un⋆ η (⟦ σ ⟧Un⋆ υ) , congaccUn η u ] , u′ ]) ⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ η ◨ [ ⟦ σ ⟧⋆ ρ , a ] , a′ ]) ≡⟨⟩
⟦ƛ⟧ (λ η a′ → ⟦ M ⟧ [ [ η ◨ ⟦ σ ⟧⋆ ρ , acc η a ] , a′ ]) ∎⟨ un⊃ (λ η′ u′ → ⟦ M ⟧Un [ [ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , congaccUn η′ u ] , u′ ])
(λ η′ e u′₁ u′₂ → ⟦ M ⟧Eq [ [ cong◨Eq⋆ η′ (reflEq⋆ (⟦ σ ⟧Un⋆ υ)) , reflEq (congaccUn η′ u) ] , e ]
[ [ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , congaccUn η′ u ] , u′₁ ]
[ [ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , congaccUn η′ u ] , u′₂ ])
(λ η′₁ η′₂ {a′} u′ → begin
acc η′₁ (⟦ M ⟧ [ [ η′₂ ◨ ⟦ σ ⟧⋆ ρ , acc η′₂ a ] , a′ ]) Eq⟨ symEq (⟦ M ⟧◨Eq η′₁ [ [ cong◨Un⋆ η′₂ (⟦ σ ⟧Un⋆ υ) , congaccUn η′₂ u ] , u′ ]) ⟩
⟦ M ⟧ (η′₁ ◨ [ [ η′₂ ◨ ⟦ σ ⟧⋆ ρ , acc η′₂ a ] , a′ ]) Eq⟨ ⟦ M ⟧Eq [ [ comp◨□Eq⋆ η′₁ η′₂ (⟦ σ ⟧Un⋆ υ) , symEq (acc□Eq η′₁ η′₂ u) ] , reflEq (congaccUn η′₁ u′) ]
[ [ cong◨Un⋆ η′₁ (cong◨Un⋆ η′₂ (⟦ σ ⟧Un⋆ υ)) , congaccUn η′₁ (congaccUn η′₂ u) ] , congaccUn η′₁ u′ ]
[ [ cong◨Un⋆ (η′₁ ○ η′₂) (⟦ σ ⟧Un⋆ υ) , congaccUn (η′₁ ○ η′₂) u ] , congaccUn η′₁ u′ ] ⟩
⟦ M ⟧ [ [ (η′₁ ○ η′₂) ◨ ⟦ σ ⟧⋆ ρ , acc (η′₁ ○ η′₂) a ] , acc η′₁ a′ ] ∎⟨ ⟦ M ⟧Un [ [ cong◨Un⋆ (η′₁ ○ η′₂) (⟦ σ ⟧Un⋆ υ) , congaccUn (η′₁ ○ η′₂) u ] , congaccUn η′₁ u′ ] ⟩) ⟩
sublift⟦_⟧Eq {ρ = ρ} {a} (M ∙ N) σ υ u = begin
⟦ sub (liftₛ σ) M ⟧ [ ρ , a ] ◎⟨ idᵣ ⟩ ⟦ sub (liftₛ σ) N ⟧ [ ρ , a ] Eq⟨ cong◎Eq idᵣ (sublift⟦ M ⟧Eq σ υ u) (⟦ sub (liftₛ σ) M ⟧Un [ υ , u ]) (⟦ M ⟧Un [ ⟦ σ ⟧Un⋆ υ , u ])
(sublift⟦ N ⟧Eq σ υ u) (⟦ sub (liftₛ σ) N ⟧Un [ υ , u ]) (⟦ N ⟧Un [ ⟦ σ ⟧Un⋆ υ , u ]) ⟩
⟦ M ⟧ [ ⟦ σ ⟧⋆ ρ , a ] ◎⟨ idᵣ ⟩ ⟦ N ⟧ [ ⟦ σ ⟧⋆ ρ , a ] ∎⟨ cong◎Un idᵣ (⟦ M ⟧Un [ ⟦ σ ⟧Un⋆ υ , u ]) (⟦ N ⟧Un [ ⟦ σ ⟧Un⋆ υ , u ]) ⟩
--------------------------------------------------------------------------------
subliftwk⟦_⟧Eq : ∀ {Γ Δ A A′ B w w′} → {ρ : w ⊩⋆ Δ} {a : w ⊩ A} {a′ : w′ ⊩ A′}
→ (M : [ Γ , A′ ] ⊢ B) (σ : Δ ⊢⋆ Γ) (η : w′ ∋⋆ w) → Un⋆ ρ → Un a → Un a′
→ Eq (⟦ sub (liftₛ (wkₛ σ)) M ⟧ [ [ η ◨ ρ , acc η a ] , a′ ])
(⟦ sub (liftₛ σ) M ⟧ [ η ◨ ρ , a′ ])
subliftwk⟦_⟧Eq {ρ = ρ} {a} {a′} M σ η υ u u′ = begin
⟦ sub (liftₛ (wkₛ σ)) M ⟧ [ [ η ◨ ρ , acc η a ] , a′ ] Eq⟨ sublift⟦ M ⟧Eq (wkₛ σ) [ cong◨Un⋆ η υ , congaccUn η u ] u′ ⟩
⟦ M ⟧ [ ⟦ wkₛ σ ⟧⋆ [ η ◨ ρ , acc η a ] , a′ ] Eq⟨ ⟦ M ⟧Eq [ wk⟦ σ ⟧Eq⋆ (cong◨Un⋆ η υ) (congaccUn η u) , reflEq u′ ]
[ ⟦ wkₛ σ ⟧Un⋆ [ cong◨Un⋆ η υ , congaccUn η u ] , u′ ]
[ ⟦ σ ⟧Un⋆ (cong◨Un⋆ η υ) , u′ ] ⟩
⟦ M ⟧ [ ⟦ σ ⟧⋆ (η ◨ ρ) , a′ ] Eq⟨ symEq (sublift⟦ M ⟧Eq σ (cong◨Un⋆ η υ) u′) ⟩
⟦ sub (liftₛ σ) M ⟧ [ η ◨ ρ , a′ ] ∎⟨ ⟦ sub (liftₛ σ) M ⟧Un [ cong◨Un⋆ η υ , u′ ] ⟩
--------------------------------------------------------------------------------
subwk⟦_⟧Eq : ∀ {Γ Δ Ω A C} → {ρ : Ω ⊩⋆ Δ} {a : Ω ⊩ A}
→ (M : Γ ⊢ C) (σ : Δ ⊢⋆ Γ) → Un⋆ ρ → Un a
→ Eq (⟦ sub (wkₛ {A} σ) M ⟧ [ ρ , a ])
(⟦ sub σ M ⟧ ρ)
subwk⟦_⟧Eq {ρ = ρ} {a} (` i) σ υ u = begin
⟦ getₛ (wkₛ σ) i ⟧ [ ρ , a ] ≡⟨ cong² ⟦_⟧ (wkgetₛ σ i) refl ∣ ⟦ getₛ (wkₛ σ) i ⟧Un [ υ , u ] ⟩
⟦ wk (getₛ σ i) ⟧ [ ρ , a ] Eq⟨ wk⟦ getₛ σ i ⟧Eq υ u ⟩
⟦ getₛ σ i ⟧ ρ ∎⟨ ⟦ getₛ σ i ⟧Un υ ⟩
subwk⟦_⟧Eq {ρ = ρ} {a} (ƛ {A = A′} M) σ υ u = begin
⟦ƛ⟧ (λ η a′ → ⟦ sub (liftₛ (wkₛ σ)) M ⟧ [ [ η ◨ ρ , acc η a ] , a′ ]) Eq⟨ eq⊃ (λ η u′ → subliftwk⟦ M ⟧Eq σ η υ u u′) ⟩
⟦ƛ⟧ (λ η a′ → ⟦ sub (liftₛ σ) M ⟧ [ η ◨ ρ , a′ ]) ∎⟨ ⟦ sub σ (ƛ M) ⟧Un υ ⟩
subwk⟦_⟧Eq {ρ = ρ} {a} (M ∙ N) σ υ u = begin
⟦ sub (wkₛ σ) (M ∙ N) ⟧ [ ρ , a ] ≡⟨⟩
⟦ sub (wkₛ σ) M ⟧ [ ρ , a ] ◎⟨ idᵣ ⟩ ⟦ sub (wkₛ σ) N ⟧ [ ρ , a ] Eq⟨ cong◎Eq idᵣ (subwk⟦ M ⟧Eq σ υ u) (⟦ sub (wkₛ σ) M ⟧Un [ υ , u ]) (⟦ sub σ M ⟧Un υ)
(subwk⟦ N ⟧Eq σ υ u) (⟦ sub (wkₛ σ) N ⟧Un [ υ , u ]) (⟦ sub σ N ⟧Un υ) ⟩
⟦ sub σ M ⟧ ρ ◎⟨ idᵣ ⟩ ⟦ sub σ N ⟧ ρ ≡⟨⟩
⟦ sub σ (M ∙ N) ⟧ ρ ∎⟨ ⟦ sub σ (M ∙ N) ⟧Un υ ⟩
--------------------------------------------------------------------------------
sub⟦_⟧Eq : ∀ {Γ Δ Ω A} → {ρ : Ω ⊩⋆ Δ}
→ (M : Γ ⊢ A) (σ : Δ ⊢⋆ Γ) → Un⋆ ρ
→ Eq (⟦ sub σ M ⟧ ρ)
(⟦ M ⟧ (⟦ σ ⟧⋆ ρ))
sub⟦_⟧Eq {ρ = ρ} (` i) σ υ = get⟦ σ ⟧Eq i υ
sub⟦_⟧Eq {ρ = ρ} (ƛ M) σ υ = begin
⟦ƛ⟧ (λ η a → ⟦ sub (liftₛ σ) M ⟧ [ η ◨ ρ , a ]) Eq⟨ eq⊃ (λ η u → sublift⟦ M ⟧Eq σ (cong◨Un⋆ η υ) u) ⟩
⟦ƛ⟧ (λ η a → ⟦ M ⟧ [ ⟦ σ ⟧⋆ (η ◨ ρ) , a ]) Eq⟨ eq⊃ (λ η u → ⟦ M ⟧Eq [ ⟦ σ ⟧◨Eq⋆ η υ , reflEq u ]
[ ⟦ σ ⟧Un⋆ (cong◨Un⋆ η υ) , u ]
[ cong◨Un⋆ η (⟦ σ ⟧Un⋆ υ) , u ]) ⟩
⟦ƛ⟧ (λ η a → ⟦ M ⟧ [ η ◨ ⟦ σ ⟧⋆ ρ , a ]) ∎⟨ un⊃ (λ η′ u → ⟦ M ⟧Un [ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , u ])
(λ η′ e u₁ u₂ → ⟦ M ⟧Eq [ cong◨Eq⋆ η′ (reflEq⋆ (⟦ σ ⟧Un⋆ υ)) , e ]
[ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , u₁ ]
[ cong◨Un⋆ η′ (⟦ σ ⟧Un⋆ υ) , u₂ ])
(λ η′₁ η′₂ {a} u → begin
acc η′₁ (⟦ M ⟧ [ η′₂ ◨ ⟦ σ ⟧⋆ ρ , a ]) Eq⟨ symEq (⟦ M ⟧◨Eq η′₁ [ cong◨Un⋆ η′₂ (⟦ σ ⟧Un⋆ υ) , u ]) ⟩
⟦ M ⟧ (η′₁ ◨ [ η′₂ ◨ ⟦ σ ⟧⋆ ρ , a ]) ≡⟨⟩
⟦ M ⟧ [ η′₁ ◨ (η′₂ ◨ ⟦ σ ⟧⋆ ρ) , acc η′₁ a ] Eq⟨ ⟦ M ⟧Eq [ comp◨□Eq⋆ η′₁ η′₂ (⟦ σ ⟧Un⋆ υ) , (reflEq (congaccUn η′₁ u)) ]
[ cong◨Un⋆ η′₁ (cong◨Un⋆ η′₂ (⟦ σ ⟧Un⋆ υ)) , congaccUn η′₁ u ]
[ cong◨Un⋆ (η′₁ ○ η′₂) (⟦ σ ⟧Un⋆ υ) , congaccUn η′₁ u ] ⟩
⟦ M ⟧ [ (η′₁ ○ η′₂) ◨ ⟦ σ ⟧⋆ ρ , acc η′₁ a ] ∎⟨ ⟦ M ⟧Un [ cong◨Un⋆ (η′₁ ○ η′₂) (⟦ σ ⟧Un⋆ υ) , congaccUn η′₁ u ] ⟩) ⟩
sub⟦_⟧Eq {ρ = ρ} (M ∙ N) σ υ = cong◎Eq idᵣ (sub⟦ M ⟧Eq σ υ) (⟦ sub σ M ⟧Un υ) (⟦ M ⟧Un (⟦ σ ⟧Un⋆ υ))
(sub⟦ N ⟧Eq σ υ) (⟦ sub σ N ⟧Un υ) (⟦ N ⟧Un (⟦ σ ⟧Un⋆ υ))
--------------------------------------------------------------------------------
-- TODO: Rename this
sublift⟦⟧Eq⁈ : ∀ {Γ Δ A B w} → {ρ : w ⊩⋆ Δ}
→ (σ : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A) → Un⋆ ρ
→ Eq (⟦ sub (liftₛ {A} σ) M ⟧ [ ρ , ⟦ N ⟧ ρ ])
(⟦ sub [ σ , N ] M ⟧ ρ)
sublift⟦⟧Eq⁈ {ρ = ρ} σ M N υ = begin
⟦ sub (liftₛ σ) M ⟧ [ ρ , ⟦ N ⟧ ρ ] Eq⟨ sublift⟦ M ⟧Eq σ υ (⟦ N ⟧Un υ) ⟩
⟦ M ⟧ [ ⟦ σ ⟧⋆ ρ , ⟦ N ⟧ ρ ] ≡⟨⟩
⟦ M ⟧ (⟦ [ σ , N ] ⟧⋆ ρ) Eq⟨ symEq (sub⟦ M ⟧Eq [ σ , N ] υ) ⟩
⟦ sub [ σ , N ] M ⟧ ρ ∎⟨ ⟦ sub [ σ , N ] M ⟧Un υ ⟩
--------------------------------------------------------------------------------
-- TODO: Generalise theorem 4 over models
module _ where
open 𝔐 canon
open Eq-Reasoning
mutual
lemƛ : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ} {M M′ : [ Γ , A ] ⊢ B}
→ M ≅ M′ → Un⋆ ρ
→ Eq (⟦ ƛ M ⟧ ρ) (⟦ ƛ M′ ⟧ ρ)
lemƛ p υ = eq⊃ (λ xs u → cong⟦ p ⟧Eq [ cong◨Un⋆ xs υ , u ])
lem∙ : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ} {M M′ : Γ ⊢ A ⊃ B} {N N′ : Γ ⊢ A}
→ M ≅ M′ → N ≅ N′ → Un⋆ ρ
→ Eq (⟦ M ∙ N ⟧ ρ) (⟦ M′ ∙ N′ ⟧ ρ)
lem∙ {M = M} {M′} {N} {N′} p q υ = cong◎Eq idᵣ (cong⟦ p ⟧Eq υ) (⟦ M ⟧Un υ) (⟦ M′ ⟧Un υ)
(cong⟦ q ⟧Eq υ) (⟦ N ⟧Un υ) (⟦ N′ ⟧Un υ)
lemβ : ∀ {Γ Δ A B w} → {ρ : w ⊩⋆ Γ}
→ (σ : Γ ⊢⋆ Δ) (M : [ Δ , A ] ⊢ B) (N : Γ ⊢ A) → Un⋆ ρ
→ Eq (⟦ sub σ (ƛ M) ∙ N ⟧ ρ) (⟦ sub [ σ , N ] M ⟧ ρ)
lemβ {ρ = ρ} σ M N υ = begin
⟦ sub (liftₛ σ) M ⟧ [ idᵣ ◨ ρ , ⟦ N ⟧ ρ ] Eq⟨ ⟦ sub (liftₛ σ) M ⟧Eq [ id₁◨Eq⋆ υ , reflEq (⟦ N ⟧Un υ) ]
[ cong◨Un⋆ idᵣ υ , ⟦ N ⟧Un υ ]
[ υ , ⟦ N ⟧Un υ ] ⟩
⟦ sub (liftₛ σ) M ⟧ [ ρ , ⟦ N ⟧ ρ ] Eq⟨ sublift⟦⟧Eq⁈ σ M N υ ⟩
⟦ sub [ σ , N ] M ⟧ ρ ∎⟨ ⟦ sub [ σ , N ] M ⟧Un υ ⟩
lemη : ∀ {Γ A B w} → {ρ : w ⊩⋆ Γ}
→ (M : Γ ⊢ A ⊃ B) → Un⋆ ρ
→ Eq (⟦ M ⟧ ρ) (⟦ ƛ (wk M ∙ ` zero) ⟧ ρ)
lemη {ρ = ρ} M υ =
eq⊃ (λ η {a} u → begin
⟦ M ⟧ ρ ◎⟨ η ⟩ a Eq⟨ symEq (acc◎idEq η (⟦ M ⟧Un υ) u) ⟩
acc η (⟦ M ⟧ ρ) ◎⟨ idᵣ ⟩ a Eq⟨ cong◎Eq idᵣ (symEq (⟦ M ⟧◨Eq η υ)) (congaccUn η (⟦ M ⟧Un υ)) (⟦ M ⟧Un (cong◨Un⋆ η υ))
(reflEq u) u u ⟩
⟦ M ⟧ (η ◨ ρ) ◎⟨ idᵣ ⟩ a Eq⟨ cong◎Eq idᵣ (symEq (wk⟦ M ⟧Eq (cong◨Un⋆ η υ) u)) (⟦ M ⟧Un (cong◨Un⋆ η υ)) (⟦ wk M ⟧Un [ cong◨Un⋆ η υ , u ])
(reflEq u) u u ⟩
⟦ ren (wkᵣ idᵣ) M ⟧ [ η ◨ ρ , a ] ◎⟨ idᵣ ⟩ a ≡⟨⟩
⟦ wk M ⟧ [ η ◨ ρ , a ] ◎⟨ idᵣ ⟩ a ∎⟨ case ⟦ wk M ⟧Un [ cong◨Un⋆ η υ , u ] of
(λ { (un⊃ h₀ h₁ h₂) → h₀ idᵣ u }) ⟩)
-- Theorem 4.
cong⟦_⟧Eq : ∀ {Γ A w} → {M M′ : Γ ⊢ A} {ρ : w ⊩⋆ Γ}
→ M ≅ M′ → Un⋆ ρ
→ Eq (⟦ M ⟧ ρ) (⟦ M′ ⟧ ρ)
cong⟦ refl≅ {M = M} ⟧Eq υ = reflEq (⟦ M ⟧Un υ)
cong⟦ sym≅ p ⟧Eq υ = symEq (cong⟦ p ⟧Eq υ)
cong⟦ trans≅ p q ⟧Eq υ = transEq (cong⟦ p ⟧Eq υ) (cong⟦ q ⟧Eq υ)
cong⟦ congƛ≅ p ⟧Eq υ = lemƛ p υ
cong⟦ cong∙≅ p q ⟧Eq υ = lem∙ p q υ
cong⟦ redβ≅ σ M N ⟧Eq υ = lemβ σ M N υ
cong⟦ expη≅ M ⟧Eq υ = lemη M υ
--------------------------------------------------------------------------------
-- Theorem 5.
thm₅ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → nf M ≡ nf M′
→ M ≅ M′
thm₅ M M′ p = begin
M ≅⟨ thm₂ M ⟩
nf M ≡⟨ p ⟩
nf M′ ≅⟨ sym≅ (thm₂ M′) ⟩
M′ ∎
where open ≅-Reasoning
--------------------------------------------------------------------------------
-- proj⟨_⟩𝒰⋆
⌊_⌋ᵤ : ∀ {Γ Δ} → (η : Δ ∋⋆ Γ)
→ Un⋆ ⌊ η ⌋ₑ
⌊ [] ⌋ᵤ = []
⌊ [ η , i ] ⌋ᵤ = [ ⌊ η ⌋ᵤ , ⟪` i ⟫ᵤ ]
-- refl𝒰⋆
idᵤ : ∀ {Γ} → Un⋆ (idₑ {Γ})
idᵤ = ⌊ idᵣ ⌋ᵤ
-- Theorem 6.
thm₆ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → M ≅ M′
→ nf M ≡ nf M′
thm₆ M M′ p = cor₁ M M′ (cong⟦ p ⟧Eq idᵤ)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment