diff options
Diffstat (limited to 'src/CBPV/Frex')
| -rw-r--r-- | src/CBPV/Frex/Comp.agda | 335 |
1 files changed, 108 insertions, 227 deletions
diff --git a/src/CBPV/Frex/Comp.agda b/src/CBPV/Frex/Comp.agda index 1ae5b4d..843ea52 100644 --- a/src/CBPV/Frex/Comp.agda +++ b/src/CBPV/Frex/Comp.agda @@ -11,6 +11,7 @@ module CBPV.Frex.Comp open import Function.Base using (_∘_; _$_) open import Function.Nary.NonDependent using (congₙ) open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning) open ≡-Reasoning @@ -34,81 +35,54 @@ private 𝔐 : Context 𝔐 = [< 𝔪 :- ⟦T⟧ ] --- Cast and Expand substitutions +-- Helper -cast : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐 +cast : Γ ~[ δᵗ 𝔐 A.Val ]↝ Δ → Γ ~[ A.Val ]↝ Δ ++ 𝔐 cast σ = σ ⨾ λ ◌ → ◌ -expand : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ → Γ :< (𝔪 :- ⟦T⟧) ~[ A.Val ]↝ Δ :< (𝔪 :- ⟦T⟧) -expand σ = cast σ :< 𝔪 ↦ A.var (%% 𝔪) - -cast-comm : - (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (f : ∀ {A} → δᵛ 𝔐 A.Val A Δ → δᵛ 𝔐 A.Val A Π) → - cast σ ⨾ f ≡ cast (σ ⨾ f) -cast-comm σ f = begin - cast σ ⨾ f ≡⟨ ⨾-assoc σ (λ ◌ → ◌) f ⟩ - σ ⨾ f ≡˘⟨ ⨾-assoc σ f (λ ◌ → ◌) ⟩ - cast (σ ⨾ f) ∎ - -lookup-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : VarPos x A′ Γ) → lookup (cast σ) i ≡ lookup σ i -lookup-cast σ i = lookup-⨾ σ (λ ◌ → ◌) i - -＠-cast : (σ : Γ ~[ δᵛ 𝔐 A.Val ]↝ Δ) (i : Var A′ Γ) → cast σ ＠ i ≡ σ ＠ i -＠-cast σ i = ＠-⨾ σ (λ ◌ → ◌) i - -expand-wkn : expand (id {Γ = Γ} ⨾ (A.var ∘ ThereVar)) ≡ (id ⨾ A.var) -expand-wkn = cong (_:< 𝔪 ↦ A.var (%% 𝔪)) $ begin - cast (id ⨾ (A.var ∘ ThereVar)) ≡⟨ ⨾-assoc id (A.var ∘ ThereVar) (λ ◌ → ◌) ⟩ - id ⨾ (A.var ∘ ThereVar) ≡˘⟨ ⨾-assoc {W = Var} id ThereVar A.var ⟩ - id ⨾ ThereVar ⨾ A.var ≡⟨ cong (_⨾ A.var) (tabulate-⨾ (λ ◌ → ◌) ThereVar) ⟩ - tabulate ThereVar ⨾ A.var ∎ +cast≈ : {σ ς : Γ ~[ δᵗ 𝔐 A.Val ]↝ Δ} → σ ≈ ς → cast σ ≈ cast ς +cast≈ σ≈ς ＠ i = σ≈ς ＠ i -- Monoid Structure open RawMonoid frexMonoid : RawMonoid -frexMonoid .Val = δᵛ 𝔐 A.Val -frexMonoid .Comp = δᶜ 𝔐 A.Comp -frexMonoid .var i = A.var (ThereVar i) -frexMonoid .subᵛ v σ = A.subᵛ v (expand σ) -frexMonoid .subᶜ c σ = A.subᶜ c (expand σ) +frexMonoid .Val = δᵗ 𝔐 A.Val +frexMonoid .Comp = δᵗ 𝔐 A.Comp +frexMonoid .var i = A.var (i ↑) +frexMonoid .subᵛ v σ = A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexMonoid .subᶜ c σ = A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) open IsMonoid frexIsMonoid : IsMonoid frexMonoid -frexIsMonoid .subᵛ-var i σ = begin - A.subᵛ (A.var $ ThereVar i) (expand σ) ≡⟨ A.subᵛ-var (ThereVar i) (expand σ) ⟩ - expand σ ＠ ThereVar i ≡⟨⟩ - cast σ ＠ i ≡⟨ ＠-cast σ i ⟩ - σ ＠ i ∎ +frexIsMonoid .subᵛ-cong v σ≈ς = A.subᵛ-cong v (cast≈ σ≈ς :< 𝔪 ⇒ refl) +frexIsMonoid .subᶜ-cong c σ≈ς = A.subᶜ-cong c (cast≈ σ≈ς :< 𝔪 ⇒ refl) +frexIsMonoid .subᵛ-var i σ = A.subᵛ-var (i ↑) _ frexIsMonoid .renᵛ-id v = begin - A.subᵛ v (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᵛ v) expand-wkn ⟩ - A.renᵛ v id ≡⟨ A.renᵛ-id v ⟩ - v ∎ + A.subᵛ v (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩ + A.renᵛ v id ≡⟨ A.renᵛ-id v ⟩ + v ∎ frexIsMonoid .subᵛ-assoc v σ ς = begin - A.subᵛ (A.subᵛ v (expand σ)) (expand ς) - ≡⟨ A.subᵛ-assoc v (expand σ) (expand ς) ⟩ - A.subᵛ v (expand σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)) - ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᵛ v (◌ᵃ :< 𝔪 ↦ ◌ᵇ)) - (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς))) - (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩ - A.subᵛ v (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς))) + A.subᵛ (A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪)) + ≡⟨ A.subᵛ-assoc v _ _ ⟩ + A.subᵛ v ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) + ≡⟨ A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩ + A.subᵛ v (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪)) ∎ frexIsMonoid .renᶜ-id c = begin - A.subᶜ c (expand (id ⨾ λ ◌ → A.var $ ThereVar ◌)) ≡⟨ cong (A.subᶜ c) expand-wkn ⟩ - A.renᶜ c id ≡⟨ A.renᶜ-id c ⟩ - c ∎ + A.subᶜ c (tabulate (A.var ∘ _↑[ 𝔪 ]) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) ⟩ + A.renᶜ c id ≡⟨ A.renᶜ-id c ⟩ + c ∎ frexIsMonoid .subᶜ-assoc c σ ς = begin - A.subᶜ (A.subᶜ c (expand σ)) (expand ς) - ≡⟨ A.subᶜ-assoc c (expand σ) (expand ς) ⟩ - A.subᶜ c ((cast σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς)) :< 𝔪 ↦ A.subᵛ (A.var $ %% 𝔪) (expand ς)) - ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → A.subᶜ c (◌ᵃ :< 𝔪 ↦ ◌ᵇ)) - (cast-comm σ (λ ◌ → A.subᵛ ◌ (expand ς))) - (A.subᵛ-var (%% 𝔪) (expand ς)) ⟩ - A.subᶜ c (expand (σ ⨾ λ ◌ → A.subᵛ ◌ (expand ς))) + A.subᶜ (A.subᶜ c (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) (cast ς :< 𝔪 ↦ A.var (%% 𝔪)) + ≡⟨ A.subᶜ-assoc c _ _ ⟩ + A.subᶜ c ((cast σ :< 𝔪 ↦ A.var (%% 𝔪)) ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) + ≡⟨ A.subᶜ-cong c (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ A.subᵛ-var (%% 𝔪) (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) ⟩ + A.subᶜ c (cast (σ ⨾ λ ◌ → A.subᵛ ◌ (cast ς :< 𝔪 ↦ A.var (%% 𝔪))) :< 𝔪 ↦ A.var (%% 𝔪)) ∎ open RawAlgebra @@ -123,202 +97,109 @@ open RawAlgebra ; push_then_ to [_]push_then_ ) +pull₁ : Γ :< x :- A′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′ +pull₁ {x = x} = weakl _ :< x ↦ %% x :< 𝔪 ↦ %% 𝔪 + +pull₂ : Γ :< x :- A′ :< y :- A′′ :< 𝔪 :- ⟦T⟧ ↝ Γ :< 𝔪 :- ⟦T⟧ :< x :- A′ :< y :- A′′ +pull₂ {x = x} {y = y} = weakl _ :< x ↦ %% x :< y ↦ %% y :< 𝔪 ↦ %% 𝔪 + frexAlgebra : RawAlgebra frexAlgebra .monoid = frexMonoid -[ frexAlgebra ]have v be c = A.have v be A.renᶜ c (pull [< _ :- _ ] 𝔐) +[ frexAlgebra ]have v be c = A.have v be A.renᶜ c pull₁ frexAlgebra .thunk c = A.thunk c frexAlgebra .force v = A.force v frexAlgebra .point = A.point [ frexAlgebra ]drop v then c = A.drop v then c [ frexAlgebra ]⟨ v , w ⟩ = A.⟨ v , w ⟩ -[ frexAlgebra ]split v then c = A.split v then A.renᶜ c (pull [< _ :- _ , _ :- _ ] 𝔐) +[ frexAlgebra ]split v then c = A.split v then A.renᶜ c pull₂ frexAlgebra .inl v = A.inl v frexAlgebra .inr v = A.inr v [ frexAlgebra ]case v of c or d = A.case v - of A.renᶜ c (pull [< _ :- _ ] 𝔐) - or A.renᶜ d (pull [< _ :- _ ] 𝔐) + of A.renᶜ c pull₁ + or A.renᶜ d pull₁ frexAlgebra .ret v = A.ret v -[ frexAlgebra ]bind c to d = A.bind c to A.renᶜ d (pull [< _ :- _ ] 𝔐) +[ frexAlgebra ]bind c to d = A.bind c to A.renᶜ d pull₁ [ frexAlgebra ]⟪ c , d ⟫ = A.⟪ c , d ⟫ frexAlgebra .fst c = A.fst c frexAlgebra .snd c = A.snd c -frexAlgebra .pop c = A.pop (A.renᶜ c (pull [< _ :- _ ] 𝔐)) +frexAlgebra .pop c = A.pop (A.renᶜ c pull₁) [ frexAlgebra ]push v then c = A.push v then c private module X = RawAlgebra frexAlgebra open IsAlgebra -lemma₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) -lemma₀ {A′ = A′} v ρ = begin - X.renᵛ v ρ ≡⟨⟩ - X.subᵛ v (ρ ⨾ X.var) ≡⟨⟩ - A.subᵛ v (expand (ρ ⨾ X.var)) ≡⟨⟩ - A.subᵛ v (cast (ρ ⨾ X.var) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨⟩ - A.subᵛ v (cast (ρ ⨾ (A.var ∘ ThereVar)) :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ (A.var ∘ ThereVar) (λ ◌ → ◌)) ⟩ - A.subᵛ v (ρ ⨾ (A.var ∘ ThereVar) :< 𝔪 ↦ A.var (%% 𝔪)) ≡˘⟨ cong (λ ◌ → A.subᵛ v (◌ :< 𝔪 ↦ A.var (toVar Here))) (⨾-assoc ρ ThereVar A.var) ⟩ - A.subᵛ v (ρ ⨾ ThereVar ⨾ A.var :< 𝔪 ↦ A.var (%% 𝔪)) ≡⟨⟩ - A.subᵛ v ((ρ ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ A.var) ≡⟨⟩ - A.renᵛ v (ρ ⨾ ThereVar {y = 𝔪} :< 𝔪 ↦ %% 𝔪) ∎ +lemma₀ : (v : X.Val A′ Γ) (ρ : Γ ↝ Δ) → X.renᵛ v ρ ≡ A.renᵛ v (lift′ [< 𝔪 :- ⟦T⟧ ] ρ) +lemma₀ v ρ = A.subᵛ-cong v (tabulate≈ (λ _ → refl) :< 𝔪 ⇒ refl) lemma₁ : - (c : δᶜ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) → - A.subᶜ (A.renᶜ c (pull [< x :- A′ ] 𝔐)) (A.lift [< x :- A′ ] (expand σ)) ≡ - A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) (pull [< x :- A′ ] 𝔐) + (c : δᵗ [< x :- A′ ] X.Comp B Γ) (σ : Γ ~[ X.Val ]↝ Δ) → + A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- A′ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) ≡ + A.renᶜ (X.subᶜ c (X.lift [< x :- A′ ] σ)) pull₁ lemma₁ {x = x} c σ = begin - A.subᶜ (A.renᶜ c (pull [< x :- _ ] 𝔐)) (A.lift [< x :- _ ] (expand σ)) - ≡⟨ A.subᶜ-renᶜ c (pull [< x :- _ ] 𝔐) (A.lift [< x :- _ ] (expand σ)) ⟩ - A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ (A.lift [< x :- _ ] (expand σ) ＠_)) - ≡⟨ congₙ 3 (λ ◌ᵃ ◌ᵇ ◌ᶜ → A.subᶜ c (◌ᵃ :< x ↦ ◌ᵇ :< 𝔪 ↦ ◌ᶜ)) - (begin - weakl 𝔐 ⨾ (weakl [< x :- _ ] ＠_) ⨾ (A.lift [< x :- _ ] (expand σ) ＠_) - ≡⟨ cong (_⨾ (A.lift [< x :- _ ] (expand σ) ＠_)) (⨾-cong (weakl 𝔐) (＠-tabulate Var ThereVar)) ⟩ - weakl 𝔐 ⨾ ThereVar ⨾ (A.lift [< x :- _ ] (expand σ) ＠_) - ≡⟨ ⨾-assoc (weakl 𝔐) ThereVar (A.lift [< x :- _ ] (expand σ) ＠_) ⟩ - weakl 𝔐 ⨾ (λ ◌ → A.lift [< x :- _ ] (expand σ) ＠ ThereVar ◌) - ≡⟨ ⨾-cong (weakl 𝔐) (＠-⨾ (expand σ) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) ⟩ - weakl 𝔐 ⨾ (λ ◌ → A.renᵛ (expand σ ＠ ◌) (weakl [< x :- _ ])) - ≡˘⟨ ⨾-assoc (weakl 𝔐) (expand σ ＠_) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩ - ([ A.Val ] (weakl 𝔐 ⨾ (expand σ ＠_)) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) - ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-⨾ (weaklF 𝔐) (expand σ ＠_)) ⟩ - tabulate (cast σ ＠_) ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) - ≡⟨ cong (_⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ]))) (tabulate-＠ (cast σ)) ⟩ - cast σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) - ≡⟨ ⨾-assoc σ (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) ⟩ - σ ⨾ (λ ◌ → A.renᵛ ◌ (weakl [< x :- _ ])) - ≡⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ v (◌ :< 𝔪 ↦ %% 𝔪)) $ - begin - tabulate (ThereVar ∘ ThereVar) ≡˘⟨ tabulate-cong Var (λ i → pull-left [< x :- _ ] 𝔐 (i .pos)) ⟩ - (tabulate ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar ∘ ThereVar)) ≡˘⟨ tabulate-⨾ {V = Var} ThereVar ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar) ⟩ - (tabulate ThereVar ⨾ ((pull [< x :- _ ] 𝔐 ＠_) ∘ ThereVar)) ≡˘⟨ ⨾-assoc (tabulate ThereVar) ThereVar (pull [< x :- _ ] 𝔐 ＠_) ⟩ - (tabulate ThereVar ⨾ ThereVar ⨾ (pull [< x :- _ ] 𝔐 ＠_)) ∎) ⟩ - σ ⨾ (λ ◌ → A.renᵛ ◌ ((weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) ⨾ (pull [< x :- _ ] 𝔐 ＠_))) - ≡˘⟨ ⨾-cong σ (λ v → A.renᵛ-assoc v (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪) (pull [< x :- _ ] 𝔐)) ⟩ - σ ⨾ (λ ◌ → A.renᵛ (A.renᵛ ◌ (weakl [< x :- _ ] ⨾ ThereVar :< 𝔪 ↦ %% 𝔪)) (pull [< x :- _ ] 𝔐)) - ≡˘⟨ ⨾-cong σ (λ v → cong (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) (lemma₀ v (weakl [< x :- _ ]))) ⟩ - σ ⨾ (λ ◌ → A.renᵛ (X.renᵛ ◌ (weakl [< x :- _ ])) (pull [< x :- _ ] 𝔐)) - ≡˘⟨ ⨾-assoc σ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩ - σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) - ≡˘⟨ ⨾-assoc (σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ]))) (λ ◌ → ◌) (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) ⟩ - σ ⨾ (λ ◌ → X.renᵛ ◌ (weakl [< x :- _ ])) ⨾ (λ ◌ → ◌) ⨾ (λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) - ∎) - (begin - A.var (%% x) ≡˘⟨ A.renᵛ-var (%% x) (pull [< x :- _ ] 𝔐) ⟩ - A.renᵛ (A.var (%% x)) (pull [< x :- _ ] 𝔐) ∎) - {!!} ⟩ - A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.renᵛ ◌ (pull [< x :- _ ] 𝔐)) - ≡˘⟨ A.subᶜ-assoc c (expand $ X.lift [< x :- _ ] σ) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩ - A.renᶜ (A.subᶜ c (expand $ X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐) - ≡⟨⟩ - A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐) + A.subᶜ (A.renᶜ c pull₁) (A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) + ≡⟨ A.subᶜ-renᶜ c _ _ ⟩ + A.subᶜ c (pull₁ ⨾′ A.lift [< x :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪))) + ≡˘⟨ A.subᶜ-cong c + ( tabulate≈ (λ i → + begin + A.renᵛ + (A.subᵛ (σ ＠ i) (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪))) + pull₁ + ≡⟨ A.subᵛ-assoc (σ ＠ i) _ _ ⟩ + A.subᵛ (σ ＠ i) + ( (cast (weakl [< x :- _ , 𝔪 :- _ ] ⨾ A.var) :< 𝔪 ↦ A.var (%% 𝔪)) + ⨾ λ ◌ → A.renᵛ ◌ pull₁) + ≡⟨ A.subᵛ-cong (σ ＠ i) + ( tabulate≈ (λ i → A.renᵛ-var (i ↑ ↑) pull₁) + :< 𝔪 ⇒ A.renᵛ-var (%% 𝔪) pull₁) ⟩ + A.renᵛ (σ ＠ i) (weakl [< x :- _ ]) + ∎) + :< x ⇒ A.renᵛ-var (%% x) pull₁ + :< 𝔪 ⇒ (begin + A.renᵛ (A.var $ %% 𝔪) pull₁ ≡⟨ A.renᵛ-var (%% 𝔪) pull₁ ⟩ + A.var (%% 𝔪) ≡˘⟨ A.renᵛ-var (MkVar 𝔪 Here) (weakl [< x :- _ ]) ⟩ + A.renᵛ (A.var $ MkVar 𝔪 Here) (weakl [< x :- _ ]) ∎) + ) ⟩ + A.subᶜ c + ( (cast (X.lift [< x :- _ ] σ) :< 𝔪 ↦ A.var (%% 𝔪)) + ⨾ λ ◌ → A.renᵛ ◌ pull₁ + ) + ≡˘⟨ A.subᶜ-assoc c _ _ ⟩ + A.renᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) pull₁ ∎ --- lemma₁ {x = x} {A′} c σ = --- begin --- A.subᶜ (A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var)) (A.lift [< x :- _ ] (expand σ)) --- ≡⟨ A.subᶜ-assoc c (pull [< x :- _ ] 𝔐 ⨾ A.var) (A.lift [< x :- _ ] (expand σ)) ⟩ --- A.subᶜ c (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- _ ] (expand σ))) --- ≡⟨ cong (A.subᶜ c) (subst-ext _ _ (λ i → helper (i .pos))) ⟩ --- A.subᶜ c (expand (X.lift [< x :- _ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- _ ] 𝔐 ⨾ A.var)) --- ≡˘⟨ A.subᶜ-assoc c (expand (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var) ⟩ --- A.subᶜ (X.subᶜ c (X.lift [< x :- _ ] σ)) (pull [< x :- _ ] 𝔐 ⨾ A.var) --- ∎ --- where --- helper : --- (i : VarPos y A′′ _) → --- lookup --- (pull [< x :- A′ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) --- i --- ≡ --- lookup {V = A.Val} --- (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) --- i --- helper Here = begin --- A.subᵛ (A.var $ toVar $ There Here) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩ --- A.subᵛ (A.var $ %% 𝔪) (weakl [< x :- A′ ] ⨾ A.var) ≡⟨ A.subᵛ-var _ _ ⟩ --- A.var (%% 𝔪) ≡˘⟨ A.subᵛ-var _ _ ⟩ --- A.subᵛ (A.var $ %% 𝔪) (pull [< x :- _ ] 𝔐 ⨾ A.var) ∎ --- helper (There Here) = begin --- A.subᵛ (A.var $ %% x) (A.lift [< x :- _ ] (expand σ)) ≡⟨ A.subᵛ-var _ _ ⟩ --- A.var (%% x) ≡˘⟨ A.subᵛ-var _ _ ⟩ --- A.subᵛ (A.var $ %% x) (pull [< x :- _ ] 𝔐 ⨾ A.var) ∎ --- helper (There (There i)) = --- begin --- lookup --- (pull [< x :- _ ] 𝔐 ⨾ A.var ⨾ λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) --- (There $ There i) --- ≡⟨ lookup-⨾ (pull [< x :- _ ] 𝔐 ⨾ A.var) (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (There $ There i) ⟩ --- A.subᵛ --- (lookup {V = A.Val} --- (pull [< x :- _ ] 𝔐 ⨾ A.var) --- (There $ There i)) --- (A.lift [< x :- A′ ] (expand σ)) --- ≡⟨ cong (λ ◌ → A.subᵛ ◌ (A.lift [< x :- A′ ] (expand σ))) (lookup-⨾ (pull [< x :- _ ] 𝔐) A.var (There $ There i)) ⟩ --- A.subᵛ --- (A.var $ lookup (pull [< x :- _ ] 𝔐) (There $ There i)) --- (A.lift [< x :- A′ ] (expand σ)) --- ≡⟨ A.subᵛ-var (lookup (pull [< x :- _ ] 𝔐) (There $ There i)) (A.lift [< x :- A′ ] (expand σ)) ⟩ --- A.lift [< x :- A′ ] (expand σ) ＠ --- lookup (pull [< x :- _ ] 𝔐) (There $ There i) --- ≡⟨ cong (A.lift [< x :- _ ] (expand σ) ＠_) (pull-left [< x :- _ ] 𝔐 i) ⟩ --- lookup (A.lift [< x :- A′ ] (expand σ)) (There $ There i) --- ≡⟨ A.lift-left [< x :- A′ ] (expand σ) (There i) ⟩ --- A.subᵛ (lookup (cast σ) i) (weakl [< x :- A′ ] ⨾ A.var) --- ≡⟨ cong (λ ◌ → A.subᵛ ◌ (weakl [< x :- A′ ] ⨾ A.var)) (lookup-cast σ i) ⟩ --- A.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ A.var) --- ≡⟨ {!!} ⟩ --- A.subᵛ (lookup σ i) --- (expand (weakl [< x :- A′ ] ⨾ X.var) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) --- ≡˘⟨ A.subᵛ-assoc (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var)) (pull [< x :- A′ ] 𝔐 ⨾ A.var) ⟩ --- A.subᵛ --- (A.subᵛ (lookup σ i) (expand (weakl [< x :- A′ ] ⨾ X.var))) --- (pull [< x :- A′ ] 𝔐 ⨾ A.var) --- ≡⟨⟩ --- A.subᵛ --- (X.subᵛ (lookup σ i) (weakl [< x :- A′ ] ⨾ X.var)) --- (pull [< x :- A′ ] 𝔐 ⨾ A.var) --- ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (X.lift-left [< x :- A′ ] σ i) ⟩ --- A.subᵛ --- (lookup (X.lift [< x :- A′ ] σ) (There i)) --- (pull [< x :- A′ ] 𝔐 ⨾ A.var) --- ≡˘⟨ cong (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (lookup-cast (X.lift [< x :- A′ ] σ) (There i)) ⟩ --- A.subᵛ --- (lookup (cast $ X.lift [< x :- A′ ] σ) (There i)) --- (pull [< x :- A′ ] 𝔐 ⨾ A.var) --- ≡˘⟨ lookup-⨾ (expand (X.lift [< x :- A′ ] σ)) (λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) (There $ There i) ⟩ --- lookup {V = A.Val} --- (expand (X.lift [< x :- A′ ] σ) ⨾ λ ◌ → A.subᵛ ◌ (pull [< x :- A′ ] 𝔐 ⨾ A.var)) --- (There $ There i) --- ∎ --- frexIsAlgebra : IsAlgebra frexAlgebra --- frexIsAlgebra .isMonoid = frexIsMonoid --- frexIsAlgebra .sub-have v c σ = --- begin --- A.subᶜ --- (A.have v be A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) --- (expand σ) --- ≡⟨ A.sub-have v (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (expand σ) ⟩ --- (A.have A.subᵛ v (expand σ) be --- A.subᶜ (A.subᶜ c (pull [< _ :- _ ] 𝔐 ⨾ A.var)) (A.lift [< _ :- _ ] (expand σ))) --- ≡⟨ cong (λ ◌ → A.have A.subᵛ v (expand σ) be ◌) (lemma₁ c σ) ⟩ --- (A.have A.subᵛ v (expand σ) be --- A.subᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) (pull [< _ :- _ ] 𝔐 ⨾ A.var)) --- ∎ --- frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (expand σ) --- frexIsAlgebra .sub-force v σ = A.sub-force v (expand σ) --- frexIsAlgebra .sub-point σ = A.sub-point (expand σ) --- frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (expand σ) --- frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (expand σ) --- frexIsAlgebra .sub-split = {!!} --- frexIsAlgebra .sub-inl v σ = A.sub-inl v (expand σ) --- frexIsAlgebra .sub-inr v σ = A.sub-inr v (expand σ) --- frexIsAlgebra .sub-case = {!!} --- frexIsAlgebra .sub-ret v σ = A.sub-ret v (expand σ) --- frexIsAlgebra .sub-bind = {!!} --- frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (expand σ) --- frexIsAlgebra .sub-fst c σ = A.sub-fst c (expand σ) --- frexIsAlgebra .sub-snd c σ = A.sub-snd c (expand σ) --- frexIsAlgebra .sub-pop = {!!} --- frexIsAlgebra .sub-push v c σ = A.sub-push v c (expand σ) +frexIsAlgebra : IsAlgebra frexAlgebra +frexIsAlgebra .isMonoid = frexIsMonoid +frexIsAlgebra .sub-have v c σ = + begin + A.subᶜ + (A.have v be A.renᶜ c pull₁) + (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) + ≡⟨ A.sub-have v (A.renᶜ c pull₁) _ ⟩ + (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be + A.subᶜ + (A.renᶜ c pull₁) + (A.lift [< _ :- _ ] (cast σ :< 𝔪 ↦ A.var (%% 𝔪)))) + ≡⟨ cong (λ ◌ → A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be ◌) (lemma₁ c σ) ⟩ + (A.have A.subᵛ v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) be + A.renᶜ (X.subᶜ c (X.lift [< _ :- _ ] σ)) pull₁) + ∎ +frexIsAlgebra .sub-thunk c σ = A.sub-thunk c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-force v σ = A.sub-force v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-point σ = A.sub-point (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-drop v c σ = A.sub-drop v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-pair v w σ = A.sub-pair v w (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-split v c σ = {!A.sub-split!} +frexIsAlgebra .sub-inl v σ = A.sub-inl v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-inr v σ = A.sub-inr v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-case = {!!} +frexIsAlgebra .sub-ret v σ = A.sub-ret v (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-bind = {!!} +frexIsAlgebra .sub-bundle c d σ = A.sub-bundle c d (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-fst c σ = A.sub-fst c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-snd c σ = A.sub-snd c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) +frexIsAlgebra .sub-pop = {!!} +frexIsAlgebra .sub-push v c σ = A.sub-push v c (cast σ :< 𝔪 ↦ A.var (%% 𝔪)) |