From 7e0169f7b6b9cb4c4323c320982c93e622999943 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Mon, 26 Feb 2024 13:19:53 +0000 Subject: WIP: concrete families --- src/CBPV/Frex/Comp.agda | 324 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 324 insertions(+) create mode 100644 src/CBPV/Frex/Comp.agda (limited to 'src/CBPV/Frex') diff --git a/src/CBPV/Frex/Comp.agda b/src/CBPV/Frex/Comp.agda new file mode 100644 index 0000000..1ae5b4d --- /dev/null +++ b/src/CBPV/Frex/Comp.agda @@ -0,0 +1,324 @@ +open import Data.List using (List) + +open import CBPV.Structure +open import CBPV.Type + +module CBPV.Frex.Comp + {A : RawAlgebra} (Aᴹ : IsModel A) + (Θ : List ValType) (Ψ : List CompType) (T : CompType) + where + +open import Function.Base using (_∘_; _$_) +open import Function.Nary.NonDependent using (congₙ) +open import Relation.Binary.PropositionalEquality.Core + +open ≡-Reasoning + +open import CBPV.Context +open import CBPV.Family + +private + variable + Γ Δ Π : Context + x y : Name + A′ A′′ : ValType + B : CompType + + module A where + open RawAlgebra A public + open IsModel Aᴹ public + + ⟦T⟧ : ValType + ⟦T⟧ = U (Θ ⟶⋆ Ψ ⟶′⋆ T) + + 𝔐 : Context + 𝔐 = [< 𝔪 :- ⟦T⟧ ] + +-- Cast and Expand substitutions + +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 ∎ + +-- 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 σ) + +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 .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 ∎ +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 ς))) + ∎ +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 ∎ +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 ς))) + ∎ + +open RawAlgebra + renaming + ( have_be_ to [_]have_be_ + ; drop_then_ to [_]drop_then_ + ; ⟨_,_⟩ to [_]⟨_,_⟩ + ; split_then_ to [_]split_then_ + ; case_of_or_ to [_]case_of_or_ + ; bind_to_ to [_]bind_to_ + ; ⟪_,_⟫ to [_]⟪_,_⟫ + ; push_then_ to [_]push_then_ + ) + +frexAlgebra : RawAlgebra +frexAlgebra .monoid = frexMonoid +[ 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 .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 [< _ :- _ ] 𝔐) +frexAlgebra .ret v = A.ret v +[ 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 ]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₁ : + (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′ ] 𝔐) +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 :- _ ] 𝔐) + ∎ +-- 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 σ) -- cgit v1.2.3