diff options
| -rw-r--r-- | src/CBPV/Context.agda | 35 | ||||
| -rw-r--r-- | src/CBPV/Family.agda | 594 | ||||
| -rw-r--r-- | src/CBPV/Frex/Comp.agda | 335 | ||||
| -rw-r--r-- | src/CBPV/Structure.agda | 279 |
4 files changed, 587 insertions, 656 deletions
diff --git a/src/CBPV/Context.agda b/src/CBPV/Context.agda index d1aafc4..0ab5093 100644 --- a/src/CBPV/Context.agda +++ b/src/CBPV/Context.agda @@ -1,6 +1,7 @@ module CBPV.Context where open import Data.Bool using (Bool) +open import Data.List using (List; []; _∷_) open import Data.String using (String) import Data.String.Properties as String @@ -15,23 +16,41 @@ abstract 𝔪 : Name 𝔪 = "𝔪" -record Named : Set where +record GenNamed (A : Set) : Set where constructor _:-_ field name : Name - ofType : ValType + ofType : A -open Named public +open GenNamed public -infixl 5 _:<_ _++_ +Named : Set +Named = GenNamed ValType -data Context : Set where - [<] : Context - _:<_ : Context → (ex : Named) → Context +infixl 5 _:<_ _++_ _<><_ + +data GenContext (A : Set) : Set where + [<] : GenContext A + _:<_ : GenContext A → (ex : GenNamed A) → GenContext A + +Context : Set +Context = GenContext ValType + +map : {A B : Set} → (A → B) → GenContext A → GenContext B +map f [<] = [<] +map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty) + +foldr : {A B : Set} → (A → B → B) → B → GenContext A → B +foldr f z [<] = z +foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ pattern [<_:-_] x A = [<] :< (x :- A) pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′) -_++_ : Context → Context → Context +_++_ : {A : Set} → GenContext A → GenContext A → GenContext A Γ ++ [<] = Γ Γ ++ (Δ :< ex) = Γ ++ Δ :< ex + +_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A +Γ <>< [] = Γ +Γ <>< (x ∷ xs) = Γ :< x <>< xs diff --git a/src/CBPV/Family.agda b/src/CBPV/Family.agda index 4a64726..dd01777 100644 --- a/src/CBPV/Family.agda +++ b/src/CBPV/Family.agda @@ -1,362 +1,396 @@ module CBPV.Family where -open import Data.List as List using (List; []; _∷_; map) +open import Data.List as List using (List; []; _∷_; foldr) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.Sum as ⊎ using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Unit using (⊤) -open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_return_of_) +open import Function.Base using (_∘_; _$_; _⟨_⟩_; flip; case_returning_of_) open import Reflection hiding (name; Name; _≟_) -open import Reflection.Argument using (_⟨∷⟩_) -open import Reflection.Term as Term using (_⋯⟅∷⟆_) -open import Relation.Binary.PropositionalEquality +open import Reflection.AST.Argument using (_⟨∷⟩_; _⟅∷⟆_) +open import Reflection.AST.Term as Term using (_⋯⟅∷⟆_) +open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning) open import Relation.Nullary using (yes; no) -open import CBPV.Context +import Data.Sum.Properties as ⊎ + +open import CBPV.Context hiding (foldr) open import CBPV.Type -- Families and Morphisms ----------------------------------------------------- -infix 4 _⇾_ _⇾ᵛ_ _⇾ᶜ_ +infix 4 _⇾_ _⇾ᵗ_ + +_-Family : Set → Set₁ +A -Family = GenContext A → Set + +_-Sorted-_-Family : Set → Set → Set₁ +A -Sorted- B -Family = A → B -Family -Family : Set₁ -Family = Context → Set +_-SortedFamily : Set → Set₁ +A -SortedFamily = A -Sorted- A -Family ValFamily : Set₁ -ValFamily = ValType → Family +ValFamily = ValType -SortedFamily CompFamily : Set₁ -CompFamily = CompType → Family +CompFamily = CompType -Sorted- ValType -Family -_⇾_ : Family → Family → Set -X ⇾ Y = {Γ : Context} → X Γ → Y Γ +_⇾_ : {A : Set} → A -Family → A -Family → Set +X ⇾ Y = {Γ : _} → X Γ → Y Γ -_⇾ᵛ_ : ValFamily → ValFamily → Set -V ⇾ᵛ W = {A : ValType} → V A ⇾ W A - -_⇾ᶜ_ : CompFamily → CompFamily → Set -C ⇾ᶜ D = {B : CompType} → C B ⇾ D B +_⇾ᵗ_ : {A B : Set} → A -Sorted- B -Family → A -Sorted- B -Family → Set +V ⇾ᵗ W = {τ : _} → V τ ⇾ W τ -- Variables ------------------------------------------------------------------- private variable - Γ Δ Θ Π : Context - A A′ : ValType x y : Name - V W X : ValFamily + A B C : Set + Γ Δ Θ Π : GenContext A + τ τ′ : A + X Y : A -Sorted- B -Family -data VarPos (x : Name) (A : ValType) : Context → Set where - Here : VarPos x A (Γ :< (x :- A)) - There : VarPos x A Γ → VarPos x A (Γ :< (y :- A′)) +data VarPos (x : Name) (τ : A) : GenContext A → Set where + Here : VarPos x τ (Γ :< (x :- τ)) + There : VarPos x τ Γ → VarPos x τ (Γ :< (y :- τ′)) -weaklPos : (Δ : Context) → VarPos x A Γ → VarPos x A (Γ ++ Δ) -weaklPos [<] i = i -weaklPos (Δ :< (x :- A)) i = There (weaklPos Δ i) +record Var (τ : A) (Γ : GenContext A) : Set where + constructor MkVar + field + name : Name + pos : VarPos name τ Γ --- Reflection +open Var public -wknTerm : Term → Term -wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ [] +toVar : VarPos x τ Γ → Var τ Γ +toVar pos = MkVar _ pos -weaklTerm : Term → Term → Term -weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ [] +-- Substitutions -------------------------------------------------------------- -searchCtx : - (wkn : Term → Term) → - (hole : Term) → - (name : Term) → - (Γ : Term) → - TC ⊤ -searchCtx wkn hole name (meta m _) = blockOnMeta m -searchCtx wkn hole name (con (quote [<]) []) = - typeError (termErr name ∷ strErr " not in context." ∷ []) -searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (meta x _ ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) = - blockOnMeta x -searchCtx wkn hole name (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) = - catchTC - (do - debugPrint "squid" 10 (strErr "checking name " ∷ termErr x ∷ strErr "..." ∷ []) - unify name x - let soln = wkn (quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ []) - debugPrint "squid" 10 (strErr "testing solution " ∷ termErr soln ∷ strErr "..." ∷ []) - unify soln hole - debugPrint "squid" 10 (strErr "success!" ∷ [])) - (searchCtx (wkn ∘ wknTerm) hole name Γ) -searchCtx wkn hole name (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) = - catchTC - (searchCtx wkn hole name Δ) - (searchCtx (wkn ∘ weaklTerm Δ) hole name Γ) -searchCtx wkn hole name Γ = - typeError (termErr name ∷ strErr " not in context " ∷ termErr Γ ∷ []) --- searchCtx (con (quote [<]) []) y = return [] --- searchCtx (con (quote _:<_) (Γ ⟨∷⟩ con (quote _:-_) (x ⟨∷⟩ A ∷ []) ⟨∷⟩ [])) y = --- -- with x Term.≟ y --- -- ... | yes _ = --- do --- let head = quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ [] --- tail ← searchCtx Γ y --- return (head ∷ map wknTerm tail) --- -- ... | no _ = --- -- do --- -- tail ← searchCtx Γ y --- -- return (map wknTerm tail) --- searchCtx (def (quote _++_) (Γ ⟨∷⟩ Δ ⟨∷⟩ [])) y = --- do --- right ← searchCtx Δ y --- left ← searchCtx Γ y --- return (right List.++ map (weaklTerm Δ) left) - --- searchCtx (meta m _) y = blockOnMeta m --- searchCtx Γ y = --- do --- debugPrint "squid" 10 (strErr "stuck matching term " ∷ termErr Γ ∷ []) --- return [] - --- tryEach : List Term → Term → TC ⊤ --- tryEach [] hole = typeError (strErr "not in context" ∷ []) --- tryEach (t ∷ []) hole = --- do --- debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ []) --- unify t hole --- debugPrint "squid" 10 (strErr "success!" ∷ []) --- tryEach (t ∷ ts@(_ ∷ _)) hole = --- do --- debugPrint "squid" 10 (strErr "trying term " ∷ termErr t ∷ []) --- catchTC --- (do --- unify t hole --- debugPrint "squid" 10 (strErr "success!" ∷ [])) --- (tryEach ts hole) - -searchVarPos : Context → Name → Term → TC ⊤ -searchVarPos Γ x hole = - do - Γ ← quoteTC Γ - x ← quoteTC x - case x return (λ _ → TC ⊤) of λ - { (meta x _) → blockOnMeta x - ; _ → return _ - } - debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) - debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) - searchCtx (λ t → t) hole x Γ +infixl 9 _⨾_ [_]_⨾_ _⨾′_ _≈⨾_ _≈⨾′_ _⨾≈_ +infixl 4 copair _∥ˡ_ _∥ʳ_ +infixl 5 _:<_↦_ subst-step +infix 4 _~[_]↝_ _↝_ [_]_≈_ _≈_ --- searchVarPos : Context → Name → Term → TC ⊤ --- searchVarPos Γ x hole = --- do --- Γ ← quoteTC Γ --- (case Γ return (λ _ → TC ⊤) of λ --- { (meta m _) → blockOnMeta m --- ; _ → return _ --- }) --- x ← quoteTC x --- debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) --- debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) --- guesses ← searchCtx Γ x --- tryEach guesses hole - --- Back to business as normal - -record Var (A : ValType) (Γ : Context) : Set where - constructor %%_ +record _~[_]↝_ (Γ : GenContext A) (X : A -Sorted- B -Family) (Δ : GenContext B) : Set where + constructor tabulate + infixr 8 _＠_ field - name : Name - @(tactic searchVarPos Γ name) {pos} : VarPos name A Γ + _＠_ : Var τ Γ → X τ Δ -open Var public +open _~[_]↝_ public -toVar : VarPos x A Γ → Var A Γ -toVar pos = (%% _) {pos} +_↝_ : GenContext A → GenContext A → Set +Γ ↝ Δ = Γ ~[ Var ]↝ Δ -ThereVar : Var A Γ → Var A (Γ :< (y :- A′)) -ThereVar i = toVar $ There (i .pos) +[_]_＠_ : (X : A -Sorted- B -Family) → Γ ~[ X ]↝ Δ → Var τ Γ → X τ Δ +[ X ] σ ＠ i = σ ＠ i --- Substitutions -------------------------------------------------------------- +-- Equality -infixl 9 _⨾_ [_]_⨾_ -infixr 8 _＠_ -infixl 5 _:<_↦_ -infix 4 Subst _↝_ +record _≈_ (σ ς : Γ ~[ X ]↝ Δ) : Set where + constructor tabulate≈ + infixr 8 _＠_ + field + _＠_ : (i : Var τ Γ) → σ ＠ i ≡ ς ＠ i -data Subst (V : ValFamily) (Δ : Context) : Context → Set where - [<] : Subst V Δ [<] - _:<_↦_ : Subst V Δ Γ → (x : Name) → V A Δ → Subst V Δ (Γ :< (x :- A)) +open _≈_ public -syntax Subst V Δ Γ = Γ ~[ V ]↝ Δ +[_]_≈_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → Γ ~[ X ]↝ Δ → Set +[ V ] σ ≈ ς = σ ≈ ς -_↝_ : Context → Context → Set -Γ ↝ Δ = Γ ~[ Var ]↝ Δ +trans≈ : {σ₁ σ₂ σ₃ : Γ ~[ X ]↝ Δ} → σ₁ ≈ σ₂ → σ₂ ≈ σ₃ → σ₁ ≈ σ₃ +trans≈ σ₁≈σ₂ σ₂≈σ₃ ＠ i = trans (σ₁≈σ₂ ＠ i) (σ₂≈σ₃ ＠ i) + +-- Combinators + +_⨾_ : Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ +(σ ⨾ f) ＠ i = f (σ ＠ i) -_⨾_ : Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ -[<] ⨾ f = [<] -(σ :< x ↦ v) ⨾ f = (σ ⨾ f) :< x ↦ f v +_⨾′_ : Γ ↝ Δ → Δ ~[ X ]↝ Θ → Γ ~[ X ]↝ Θ +(ρ ⨾′ f) ＠ i = f ＠ (ρ ＠ i) -[_]_⨾_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → (∀ {A} → V A Δ → W A Θ) → Γ ~[ W ]↝ Θ +[_]_⨾_ : (X : A -SortedFamily) → Γ ~[ X ]↝ Δ → (∀ {τ} → X τ Δ → Y τ Θ) → Γ ~[ Y ]↝ Θ [ V ] σ ⨾ f = σ ⨾ f -tabulate : (∀ {A} → Var A Γ → V A Δ) → Γ ~[ V ]↝ Δ -tabulate {Γ = [<]} f = [<] -tabulate {Γ = Γ :< (x :- A)} f = tabulate (f ∘ ThereVar) :< x ↦ f (toVar Here) +_≈⨾_ : {σ ς : Γ ~[ X ]↝ Δ} → σ ≈ ς → (f : ∀ {τ} → X τ Δ → Y τ Θ) → [ Y ] (σ ⨾ f) ≈ (ς ⨾ f) +(σ≈ς ≈⨾ f) ＠ i = cong f (σ≈ς ＠ i) -lookup : Γ ~[ V ]↝ Δ → VarPos x A Γ → V A Δ -lookup (σ :< x ↦ v) Here = v -lookup (σ :< x ↦ v) (There i) = lookup σ i +_≈⨾′_ : {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → (σ : Δ ~[ X ]↝ Θ) → ρ ⨾′ σ ≈ ϱ ⨾′ σ +(ρ≈ϱ ≈⨾′ σ) ＠ i = cong (σ ＠_) (ρ≈ϱ ＠ i) -_＠_ : Γ ~[ V ]↝ Δ → Var A Γ → V A Δ -σ ＠ i = lookup σ (i .pos) +_⨾≈_ : (ρ : Γ ↝ Δ) → {σ ς : Δ ~[ X ]↝ Θ} → σ ≈ ς → ρ ⨾′ σ ≈ ρ ⨾′ ς +(ρ ⨾≈ σ≈ς) ＠ i = σ≈ς ＠ ρ ＠ i -[_]_＠_ : (V : ValFamily) → Γ ~[ V ]↝ Δ → Var A Γ → V A Δ -[ V ] σ ＠ i = σ ＠ i +-- Particular Substitutions + +-- id id : Γ ↝ Γ id = tabulate (λ x → x) -weakrPos : VarPos x A Δ → VarPos x A (Γ ++ Δ) +-- empty + +empty : [<] ~[ X ]↝ Γ +empty = tabulate (λ ()) + +-- weakr + +weakrPos : VarPos x τ Δ → VarPos x τ (Γ ++ Δ) weakrPos Here = Here weakrPos (There i) = There (weakrPos i) -weakrF : Var A Δ → Var A (Γ ++ Δ) +weakrF : Var τ Δ → Var τ (Γ ++ Δ) weakrF i = toVar $ weakrPos $ i .pos weakr : Δ ↝ Γ ++ Δ weakr = tabulate weakrF -weaklF : (Δ : Context) → Var A Γ → Var A (Γ ++ Δ) +-- weakl + +weaklPos : (Δ : GenContext A) → VarPos x τ Γ → VarPos x τ (Γ ++ Δ) +weaklPos [<] i = i +weaklPos (Δ :< (x :- τ)) i = There (weaklPos Δ i) + +weaklF : (Δ : GenContext A) → Var τ Γ → Var τ (Γ ++ Δ) weaklF Δ i = toVar $ weaklPos Δ $ i .pos -weakl : (Δ : Context) → Γ ↝ Γ ++ Δ +weakl : (Δ : GenContext A) → Γ ↝ Γ ++ Δ weakl Δ = tabulate (weaklF Δ) -copair : Γ ~[ V ]↝ Θ → Δ ~[ V ]↝ Θ → Γ ++ Δ ~[ V ]↝ Θ -copair σ [<] = σ -copair σ (ς :< x ↦ v) = copair σ ς :< x ↦ v +-- copair + +splitPos : (Δ : GenContext A) → VarPos x τ (Γ ++ Δ) → VarPos x τ Γ ⊎ VarPos x τ Δ +splitPos [<] i = inj₁ i +splitPos (Δ :< _) Here = inj₂ Here +splitPos (Δ :< _) (There i) = ⊎.map₂ There (splitPos Δ i) + +splitF : (Δ : GenContext A) → Var τ (Γ ++ Δ) → Var τ Γ ⊎ Var τ Δ +splitF Δ i = ⊎.map toVar toVar $ splitPos Δ $ i .pos + +copair : Γ ~[ X ]↝ Θ → Δ ~[ X ]↝ Θ → Γ ++ Δ ~[ X ]↝ Θ +copair σ ς ＠ i = [ σ ＠_ , ς ＠_ ] $ splitF _ i + +syntax copair σ ς = σ ∥ ς + +copairₙ : {Γs : List (GenContext A)} → All (_~[ X ]↝ Θ) Γs → foldr _++_ [<] Γs ~[ X ]↝ Θ +copairₙ [] ＠ () +copairₙ (σ ∷ σs) = σ ∥ copairₙ σs -pull : (Δ Θ : Context) → Γ ++ Δ ++ Θ ↝ Γ ++ Θ ++ Δ -pull Δ Θ = - copair {Δ = Θ} - (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) - (weakr ⨾ (weakl Δ ＠_)) +-- singleton + +singleton : (x : Name) → X τ Γ → [< x :- τ ] ~[ X ]↝ Γ +singleton x v ＠ (MkVar .x Here) = v + +-- snoc + +_:<_↦_ : Γ ~[ X ]↝ Δ → (x : Name) → X τ Δ → Γ :< (x :- τ) ~[ X ]↝ Δ +σ :< x ↦ v = σ ∥ singleton x v + +-- weakening + +data Path {A : Set} : GenContext A → GenContext A → Set where + ⌞_⌟ : (Γ : GenContext A) → Path Γ Γ + _∥ˡ_ : Path Γ Δ → (Θ : GenContext A) → Path Γ (Δ ++ Θ) + _∥ʳ_ : (Θ : GenContext A) → Path Γ Δ → Path Γ (Θ ++ Δ) + +wkn : Path Γ Δ → Γ ↝ Δ +wkn ⌞ Γ ⌟ = id +wkn (path ∥ˡ Θ) = wkn path ⨾′ weakl Θ +wkn (Θ ∥ʳ path) = wkn path ⨾′ weakr + +-- lift + +lift′ : (Θ : GenContext A) → Γ ↝ Δ → Γ ++ Θ ↝ Δ ++ Θ +lift′ Θ ρ = ρ ⨾ weaklF Θ ∥ weakr + +-- weakening variables + +_↑_ : Var τ Γ → (Δ : GenContext A) → Var τ (Γ ++ Δ) +i ↑ Δ = weakl Δ ＠ i + +_↑[_] : Var τ Γ → (x : Name) → Var τ (Γ :< (x :- τ′)) +i ↑[ x ] = i ↑ [< x :- _ ] + +_↑ : Var τ Γ → Var τ (Γ :< (x :- τ′)) +i ↑ = i ↑[ _ ] + +-- interaction with map + +map⁺Pos : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → VarPos x τ (map f Γ) → X τ Δ +map⁺Pos {Γ = Γ :< (x :- τ)} σ Here = σ ＠ toVar Here +map⁺Pos {Γ = Γ :< (x :- τ)} {X = X} σ (There i) = map⁺Pos {X = X} (tabulate (λ i → σ ＠ (i ↑))) i + +map⁺ : {f : A → B} → Γ ~[ X ∘ f ]↝ Δ → map f Γ ~[ X ]↝ Δ +map⁺ σ ＠ i = map⁺Pos σ (i .pos) + +varPosMap⁺ : {f : A → B} → VarPos x τ Γ → VarPos x (f τ) (map f Γ) +varPosMap⁺ Here = Here +varPosMap⁺ (There i) = There (varPosMap⁺ i) + +varMap⁺ : {f : A → B} → Var τ Γ → Var (f τ) (map f Γ) +varMap⁺ v = toVar (varPosMap⁺ $ v .pos) + +map⁻ : {f : A → B} → map f Γ ~[ X ]↝ Δ → Γ ~[ X ∘ f ]↝ Δ +map⁻ σ ＠ i = σ ＠ varMap⁺ i -- Properties -subst-ext : (σ ς : Γ ~[ V ]↝ Δ) → (∀ {A} → (i : Var A Γ) → σ ＠ i ≡ ς ＠ i) → σ ≡ ς -subst-ext [<] [<] ext = refl -subst-ext (σ :< x ↦ v) (ς :< .x ↦ w) ext = - cong₂ (_:< x ↦_) (subst-ext σ ς $ λ i → ext $ ThereVar i) (ext $ %% x) - -⨾-assoc : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (g : ∀ {A} → W A Θ → X A Π) → - _⨾_ {V = W} {W = X} (σ ⨾ f) g ≡ σ ⨾ (g ∘ f) -⨾-assoc [<] f g = refl -⨾-assoc (σ :< x ↦ v) f g = cong (_:< x ↦ g (f v)) (⨾-assoc σ f g) - -⨾-cong : - (σ : Γ ~[ V ]↝ Δ) {f g : ∀ {A} → V A Δ → W A Θ} → - (∀ {A} → (v : V A Δ) → f v ≡ g v) → - _⨾_ {W = W} σ f ≡ σ ⨾ g -⨾-cong [<] ext = refl -⨾-cong (σ :< x ↦ v) ext = cong₂ (_:< x ↦_) (⨾-cong σ ext) (ext v) - -lookup-⨾ : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : VarPos x A Γ) → - lookup {V = W} (σ ⨾ f) i ≡ f (lookup σ i) -lookup-⨾ (σ :< x ↦ v) f Here = refl -lookup-⨾ (σ :< x ↦ v) f (There i) = lookup-⨾ σ f i - -lookup-tabulate : - (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : VarPos x A Γ) → - lookup {V = V} (tabulate f) i ≡ f (toVar i) -lookup-tabulate V f Here = refl -lookup-tabulate V f (There i) = lookup-tabulate V (f ∘ ThereVar) i - -＠-⨾ : - (σ : Γ ~[ V ]↝ Δ) (f : ∀ {A} → V A Δ → W A Θ) (i : Var A Γ) → - _＠_ {V = W} (σ ⨾ f) i ≡ f (σ ＠ i) -＠-⨾ σ f i = lookup-⨾ σ f (i .pos) - -＠-tabulate : - (V : ValFamily) (f : ∀ {A} → Var A Γ → V A Δ) (i : Var A Γ) → - _＠_ {V = V} (tabulate f) i ≡ f i -＠-tabulate V f i = lookup-tabulate V f (i .pos) - -tabulate-cong : - (V : ValFamily) → - {f g : ∀ {A} → Var A Γ → V A Δ} → - (∀ {A} → (v : Var A Γ) → f v ≡ g v) → - tabulate {V = V} f ≡ tabulate g -tabulate-cong {Γ = [<]} V ext = refl -tabulate-cong {Γ = Γ :< (x :- A)} V ext = - cong₂ (_:< x ↦_) (tabulate-cong V (ext ∘ ThereVar)) (ext $ %% x) - -tabulate-⨾ : - (f : ∀ {A} → Var A Γ → V A Δ) (g : ∀ {A} → V A Δ → W A Θ) → - tabulate {V = V} f ⨾ g ≡ tabulate {V = W} (g ∘ f) -tabulate-⨾ {Γ = [<]} f g = refl -tabulate-⨾ {Γ = Γ :< (x :- A)} f g = cong (_:< x ↦ g (f $ toVar Here)) (tabulate-⨾ (f ∘ ThereVar) g) - -tabulate-＠ : (σ : Γ ~[ V ]↝ Δ) → tabulate (σ ＠_) ≡ σ -tabulate-＠ [<] = refl -tabulate-＠ (σ :< x ↦ v) = cong (_:< x ↦ v) (tabulate-＠ σ) - -copair-⨾ : - (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (f : ∀ {A} → V A Θ → W A Π) → - copair {V = W} (σ ⨾ f) (ς ⨾ f) ≡ copair {V = V} σ ς ⨾ f -copair-⨾ σ [<] f = refl -copair-⨾ σ (ς :< x ↦ v) f = cong (_:< x ↦ f v) (copair-⨾ σ ς f) - -copair-left : - (σ : Γ ~[ V ]↝ Θ) (ς : Δ ~[ V ]↝ Θ) (i : VarPos x A Γ) → - lookup (copair σ ς) (weaklPos Δ i) ≡ lookup σ i -copair-left σ [<] i = refl -copair-left σ (ς :< x ↦ v) i = copair-left σ ς i - -pull-left : - (Δ Θ : Context) (i : VarPos x A Γ) → - lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i) ≡ toVar (weaklPos Δ $ weaklPos Θ i) -pull-left {Γ = Γ} Δ Θ i = - begin - lookup (pull Δ Θ) (weaklPos Θ $ weaklPos Δ i) - ≡⟨ copair-left (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weakr {Γ = Γ} ⨾ (weakl Δ ＠_)) (weaklPos Δ i) ⟩ - lookup (copair {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr) (weaklPos Δ i) - ≡⟨ copair-left {Δ = Δ} (weakl Θ ⨾ (weakl Δ ＠_)) weakr i ⟩ - lookup (weakl Θ ⨾ (weakl Δ ＠_)) i - ≡⟨ lookup-⨾ (weakl Θ) (weakl Δ ＠_) i ⟩ - weakl Δ ＠ lookup (weakl Θ) i - ≡⟨ cong (weakl Δ ＠_) (lookup-tabulate Var (weaklF Θ) i) ⟩ - lookup (weakl Δ) (weaklPos Θ i) - ≡⟨ lookup-tabulate Var (weaklF Δ) (weaklPos Θ i) ⟩ - toVar (weaklPos Δ $ weaklPos Θ i) - ∎ +subst-step : + {x : Name} {σ ς : Γ :< (x :- τ) ~[ X ]↝ Δ} → + weakl [< x :- τ ] ⨾′ σ ≈ weakl [< x :- τ ] ⨾′ ς → + σ ＠ MkVar x Here ≡ ς ＠ MkVar x Here → + σ ≈ ς +subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x Here = σ₀≡ς₀ +subst-step σ↑≈ς↑ σ₀≡ς₀ ＠ MkVar x (There pos) = σ↑≈ς↑ ＠ MkVar x pos + +syntax subst-step {x = x} σ≈ς v≡w = σ≈ς :< x ⇒ v≡w + +-- weakl [<] is id + +weakl[<]≈id : weakl {Γ = Γ} [<] ≈ id +weakl[<]≈id = tabulate≈ (λ i → refl) + +-- copair is coslice coproduct + +splitPos-weaklPos : (Δ : GenContext A) → (i : VarPos x τ Γ) → splitPos Δ (weaklPos Δ i) ≡ inj₁ i +splitPos-weaklPos [<] i = refl +splitPos-weaklPos (Δ :< _) i = cong (⊎.map₂ There) (splitPos-weaklPos Δ i) + +splitF-weaklF : (Δ : GenContext A) (i : Var τ Γ) → splitF Δ (weaklF Δ i) ≡ inj₁ i +splitF-weaklF Δ i = cong (⊎.map toVar toVar) (splitPos-weaklPos Δ $ i .pos) + +copair-weakl : + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) → + [ X ] weakl Δ ⨾′ (σ ∥ ς) ≈ σ +copair-weakl σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weaklF _ i) + +splitPos-weakrPos : + (Γ : GenContext A) → (i : VarPos x τ Δ) → + splitPos {Γ = Γ} Δ (weakrPos i) ≡ inj₂ i +splitPos-weakrPos Γ Here = refl +splitPos-weakrPos Γ (There i) = cong (⊎.map₂ There) (splitPos-weakrPos Γ i) + +splitF-weakrF : (Γ : GenContext A) (i : Var τ Δ) → splitF Δ (weakrF i) ≡ inj₂ i +splitF-weakrF Γ i = cong (⊎.map toVar toVar) (splitPos-weakrPos Γ $ i .pos) + +copair-weakr : + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) → + [ X ] weakr {Γ = Γ} ⨾′ (σ ∥ ς) ≈ ς +copair-weakr σ ς ＠ i = cong [ σ ＠_ , ς ＠_ ] (splitF-weakrF _ i) + +weakPos-splitPos : + (Δ : GenContext A) (i : VarPos x τ (Γ ++ Δ)) → + [ weaklPos Δ , weakrPos ] (splitPos Δ i) ≡ i +weakPos-splitPos [<] i = refl +weakPos-splitPos (Δ :< _) Here = refl +weakPos-splitPos (Δ :< _) (There i) = begin + [ There ∘ weaklPos Δ , weakrPos ]′ (⊎.map₂ There $ splitPos Δ i) ≡⟨ ⊎.[,]-map (splitPos Δ i) ⟩ + [ There ∘ weaklPos Δ , weakrPos ∘ There ]′ (splitPos Δ i) ≡⟨⟩ + [ There ∘ weaklPos Δ , There ∘ weakrPos ]′ (splitPos Δ i) ≡˘⟨ ⊎.[,]-∘ There (splitPos Δ i) ⟩ + There ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ i) ≡⟨ cong There (weakPos-splitPos Δ i) ⟩ + There i ∎ + where open ≡-Reasoning + +weakF-splitF : (Δ : GenContext A) (i : Var τ (Γ ++ Δ)) → [ weaklF Δ , weakrF ] (splitF Δ i) ≡ i +weakF-splitF Δ i = begin + [ weaklF Δ , weakrF ] (splitF Δ i) ≡⟨ ⊎.[,]-map (splitPos Δ $ i .pos) ⟩ + [ weaklF Δ ∘ toVar , weakrF ∘ toVar ] (splitPos Δ $ i .pos) ≡⟨⟩ + [ toVar ∘ weaklPos Δ , toVar ∘ weakrPos ] (splitPos Δ $ i .pos) ≡˘⟨ ⊎.[,]-∘ toVar (splitPos Δ $ i .pos) ⟩ + toVar ([ weaklPos Δ , weakrPos ]′ $ splitPos Δ $ i .pos) ≡⟨ cong toVar (weakPos-splitPos Δ (i .pos)) ⟩ + toVar (i .pos) ≡⟨⟩ + i ∎ + where open ≡-Reasoning + +copair-unique : + {X : A -Sorted- B -Family} → + (σ : Γ ~[ X ]↝ Θ) (ς : Δ ~[ X ]↝ Θ) (s : Γ ++ Δ ~[ X ]↝ Θ) → + (weakl Δ ⨾′ s ≈ σ) → (weakr ⨾′ s ≈ ς) → + (σ ∥ ς) ≈ s +copair-unique {Δ = Δ} σ ς s wkl⨾s≈σ wkr⨾s≈ς ＠ i = begin + [ σ ＠_ , ς ＠_ ] (splitF Δ i) ≡˘⟨ ⊎.[,]-cong (wkl⨾s≈σ ＠_) (wkr⨾s≈ς ＠_) (splitF Δ i) ⟩ + [ (weakl Δ ⨾′ s) ＠_ , (weakr ⨾′ s) ＠_ ] (splitF Δ i) ≡˘⟨ ⊎.[,]-∘ (s ＠_) (splitF Δ i) ⟩ + s ＠ ([ weaklF Δ , weakrF ] $ splitF Δ i) ≡⟨ cong (s ＠_) (weakF-splitF Δ i) ⟩ + s ＠ i ∎ where open ≡-Reasoning -- Special Families ----------------------------------------------------------- infixr 5 _⇒_ -_⇒_ : Family → Family → Family +_⇒_ : A -Family → A -Family → A -Family (X ⇒ Y) Γ = X Γ → Y Γ -_^_ : Family → ValFamily → Family -(X ^ V) Γ = {Δ : Context} → Γ ~[ V ]↝ Δ → X Δ - -_^ᵛ_ : ValFamily → ValFamily → ValFamily -(W ^ᵛ V) A = W A ^ V +_^_ : A -Family → B -Sorted- A -Family → B -Family +(X ^ V) Γ = {Δ : GenContext _} → Γ ~[ V ]↝ Δ → X Δ -_^ᶜ_ : CompFamily → ValFamily → CompFamily -(C ^ᶜ V) B = C B ^ V +_^ᵗ_ : A -Sorted- B -Family → C -Sorted- B -Family → A -Sorted- C -Family +(W ^ᵗ V) τ = W τ ^ V -□_ : Family → Family +□_ : A -Family → A -Family □_ = _^ Var -□ᵛ_ : ValFamily → ValFamily -□ᵛ_ = _^ᵛ Var +□ᵗ_ : A -Sorted- B -Family → A -Sorted- B -Family +□ᵗ_ = _^ᵗ Var -□ᶜ_ : CompFamily → CompFamily -□ᶜ_ = _^ᶜ Var - -δ : Context → Family → Family +δ : GenContext A → A -Family → A -Family δ Δ X Γ = X (Γ ++ Δ) -δᵛ : Context → ValFamily → ValFamily -δᵛ Δ V A = δ Δ (V A) +δᵗ : GenContext B → A -Sorted- B -Family → A -Sorted- B -Family +δᵗ Δ V τ = δ Δ (V τ) + +-- Reflection ------------------------------------------------------------------ + +wknTerm : Term → Term +wknTerm t = quote There ⟨ con ⟩ 5 ⋯⟅∷⟆ t ⟨∷⟩ [] + +weaklTerm : Term → Term → Term +weaklTerm Δ t = quote weaklPos ⟨ def ⟩ 3 ⋯⟅∷⟆ Δ ⟨∷⟩ t ⟨∷⟩ [] + +searchCtx : + (wkn : Term → Term) → + (hole : Term) → + (name : Term) → + (Γ : Term) → + TC ⊤ +searchCtx wkn hole name (meta m _) = blockOnMeta m +searchCtx wkn hole name (con (quote _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ meta x _ ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) = + blockOnMeta x +searchCtx wkn hole name (con (quote _:<_) (_ ⟅∷⟆ Γ ⟨∷⟩ con (quote _:-_) (_ ⟅∷⟆ x ⟨∷⟩ ty ∷ []) ⟨∷⟩ [])) = + catchTC + (do + debugPrint "squid" 10 (strErr "checking name " ∷ termErr x ∷ strErr "..." ∷ []) + unify name x + let soln = wkn (quote Here ⟨ con ⟩ 3 ⋯⟅∷⟆ []) + debugPrint "squid" 10 (strErr "testing solution " ∷ termErr soln ∷ strErr "..." ∷ []) + unify soln hole + debugPrint "squid" 10 (strErr "success!" ∷ [])) + (searchCtx (wkn ∘ wknTerm) hole name Γ) +searchCtx wkn hole name (con (quote [<]) (_ ⟅∷⟆ [])) = + typeError (termErr name ∷ strErr " not in context." ∷ []) +searchCtx wkn hole name (def (quote _++_) (_ ⟅∷⟆ Γ ⟨∷⟩ Δ ⟨∷⟩ [])) = + catchTC + (searchCtx wkn hole name Δ) + (searchCtx (wkn ∘ weaklTerm Δ) hole name Γ) +searchCtx wkn hole name Γ = + typeError (termErr name ∷ strErr " not in context " ∷ termErr Γ ∷ []) + +searchVarPos : {A : Set} → GenContext A → Name → Term → TC ⊤ +searchVarPos Γ x hole = + do + Γ ← quoteTC Γ + x ← quoteTC x + case x returning (λ _ → TC ⊤) of λ + { (meta x _) → blockOnMeta x + ; _ → pure _ + } + debugPrint "squid" 10 (strErr "Γ = " ∷ termErr Γ ∷ []) + debugPrint "squid" 10 (strErr "x = " ∷ termErr x ∷ []) + searchCtx (λ t → t) hole x Γ -δᶜ : Context → CompFamily → CompFamily -δᶜ Δ C B = δ Δ (C B) +%%_ : + {A : Set} → {ty : A} → {Γ : GenContext A} → + (x : Name) → {@(tactic searchVarPos Γ x) pos : VarPos x ty Γ} → Var ty Γ +%%_ x {pos} = MkVar x pos 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 (%% 𝔪)) diff --git a/src/CBPV/Structure.agda b/src/CBPV/Structure.agda index 0f64b1c..1c51e0e 100644 --- a/src/CBPV/Structure.agda +++ b/src/CBPV/Structure.agda @@ -1,6 +1,6 @@ module CBPV.Structure where -open import CBPV.Context +open import CBPV.Context hiding (map) open import CBPV.Family open import CBPV.Type @@ -10,6 +10,7 @@ open import Data.List.Relation.Unary.All using (All; map) open import Function.Base using (_∘_; _$_) open import Relation.Binary.PropositionalEquality.Core +open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning) private variable @@ -24,31 +25,23 @@ record RawMonoid : Set₁ where field Val : ValFamily Comp : CompFamily - var : Var ⇾ᵛ Val - subᵛ : Val ⇾ᵛ Val ^ᵛ Val - subᶜ : Comp ⇾ᶜ Comp ^ᶜ Val + var : Var ⇾ᵗ Val + subᵛ : Val ⇾ᵗ Val ^ᵗ Val + subᶜ : Comp ⇾ᵗ Comp ^ᵗ Val - renᵛ : Val ⇾ᵛ □ᵛ Val + renᵛ : Val ⇾ᵗ □ᵗ Val renᵛ v ρ = subᵛ v (ρ ⨾ var) - renᶜ : Comp ⇾ᶜ □ᶜ Comp + renᶜ : Comp ⇾ᵗ □ᵗ Comp renᶜ c ρ = subᶜ c (ρ ⨾ var) lift : (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) → Γ ++ Θ ~[ Val ]↝ Δ ++ Θ - lift Θ σ = copair (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var) + lift Θ σ = σ ⨾ (λ ◌ → renᵛ ◌ (weakl Θ)) ∥ weakr ⨾ var - lift-left : - (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) (i : VarPos x A Γ) → - lookup (lift Θ σ) (weaklPos Θ i) ≡ renᵛ (lookup σ i) (weakl Θ) - lift-left Θ σ i = - begin - lookup (lift Θ σ) (weaklPos Θ i) - ≡⟨ copair-left {V = Val} {Δ = Θ} (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var) i ⟩ - lookup (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) i - ≡⟨ lookup-⨾ σ (λ ◌ → renᵛ ◌ (weakl Θ)) i ⟩ - renᵛ (lookup σ i) (weakl Θ) - ∎ - where open ≡-Reasoning + lift-weakl : + (Θ : Context) (σ : Γ ~[ Val ]↝ Δ) → + weakl Θ ⨾′ lift Θ σ ≈ σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ) + lift-weakl Θ σ = copair-weakl {X = Val} {Δ = Θ} (σ ⨾ λ ◌ → renᵛ ◌ (weakl Θ)) (weakr ⨾ var) record RawAlgebra : Set₁ where infixr 1 have_be_ drop_then_ split_then_ bind_to_ push_then_ @@ -61,41 +54,41 @@ record RawAlgebra : Set₁ where open RawMonoid monoid public field - have_be_ : Val A ⇾ δᶜ [< x :- A ] Comp B ⇒ Comp B + have_be_ : Val A ⇾ δᵗ [< x :- A ] Comp B ⇒ Comp B thunk : Comp B ⇾ Val (U B) force : Val (U B) ⇾ Comp B point : Val 𝟙 Γ drop_then_ : Val 𝟙 ⇾ Comp B ⇒ Comp B ⟨_,_⟩ : Val A ⇾ Val A′ ⇒ Val (A × A′) - split_then_ : Val (A × A′) ⇾ δᶜ [< x :- A , y :- A′ ] Comp B ⇒ Comp B + split_then_ : Val (A × A′) ⇾ δᵗ [< x :- A , y :- A′ ] Comp B ⇒ Comp B inl : Val A ⇾ Val (A + A′) inr : Val A′ ⇾ Val (A + A′) - case_of_or_ : Val (A + A′) ⇾ δᶜ [< x :- A ] Comp B ⇒ δᶜ [< y :- A′ ] Comp B ⇒ Comp B + case_of_or_ : Val (A + A′) ⇾ δᵗ [< x :- A ] Comp B ⇒ δᵗ [< y :- A′ ] Comp B ⇒ Comp B ret : Val A ⇾ Comp (F A) - bind_to_ : Comp (F A) ⇾ δᶜ [< x :- A ] Comp B ⇒ Comp B + bind_to_ : Comp (F A) ⇾ δᵗ [< x :- A ] Comp B ⇒ Comp B ⟪_,_⟫ : Comp B ⇾ Comp B′ ⇒ Comp (B × B′) fst : Comp (B × B′) ⇾ Comp B snd : Comp (B × B′) ⇾ Comp B′ - pop : δᶜ [< x :- A ] Comp B ⇾ Comp (A ⟶ B) + pop : δᵗ [< x :- A ] Comp B ⇾ Comp (A ⟶ B) push_then_ : Val A ⇾ Comp (A ⟶ B) ⇒ Comp B - have_be[_]_ : Val A Γ → (x : Name) → δᶜ [< x :- A ] Comp B Γ → Comp B Γ + have_be[_]_ : Val A Γ → (x : Name) → δᵗ [< x :- A ] Comp B Γ → Comp B Γ have v be[ x ] c = have v be c - split_then[_,_]_ : Val (A × A′) Γ → (x y : Name) → δᶜ [< x :- A , y :- A′ ] Comp B Γ → Comp B Γ + split_then[_,_]_ : Val (A × A′) Γ → (x y : Name) → δᵗ [< x :- A , y :- A′ ] Comp B Γ → Comp B Γ split v then[ x , y ] c = split v then c case_of[_]_or[_]_ : Val (A + A′) Γ → - (x : Name) → δᶜ [< x :- A ] Comp B Γ → - (y : Name) → δᶜ [< y :- A′ ] Comp B Γ → + (x : Name) → δᵗ [< x :- A ] Comp B Γ → + (y : Name) → δᵗ [< y :- A′ ] Comp B Γ → Comp B Γ case v of[ x ] c or[ y ] d = case v of c or d - bind_to[_]_ : Comp (F A) Γ → (x : Name) → δᶜ [< x :- A ] Comp B Γ → Comp B Γ + bind_to[_]_ : Comp (F A) Γ → (x : Name) → δᵗ [< x :- A ] Comp B Γ → Comp B Γ bind c to[ x ] d = bind c to d - pop[_] : (x : Name) → δᶜ [< x :- A ] Comp B ⇾ Comp (A ⟶ B) + pop[_] : (x : Name) → δᵗ [< x :- A ] Comp B ⇾ Comp (A ⟶ B) pop[ x ] c = pop c open RawAlgebra @@ -106,8 +99,8 @@ record RawCompExtension where field X : RawAlgebra - staᵛ : A .Val ⇾ᵛ X .Val - staᶜ : A .Comp ⇾ᶜ X .Comp + staᵛ : A .Val ⇾ᵗ X .Val + staᶜ : A .Comp ⇾ᵗ X .Comp dyn : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Comp T Γ record RawValExtension @@ -116,8 +109,8 @@ record RawValExtension where field X : RawAlgebra - staᵛ : A .Val ⇾ᵛ X .Val - staᶜ : A .Comp ⇾ᶜ X .Comp + staᵛ : A .Val ⇾ᵗ X .Val + staᶜ : A .Comp ⇾ᵗ X .Comp dyn : All (λ A → X .Val A Γ) Θ → All (λ B → X .Comp B Γ) Ψ → X .Val T Γ record RawFreeCompExtension @@ -130,8 +123,8 @@ record RawFreeCompExtension open RawCompExtension field - evalᵛ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Val ⇾ᵛ ext .X .Val - evalᶜ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Comp ⇾ᶜ ext .X .Comp + evalᵛ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Val ⇾ᵗ ext .X .Val + evalᶜ : (ext : RawCompExtension A Θ Ψ T) → extension .X .Comp ⇾ᵗ ext .X .Comp record RawFreeValExtension (A : RawAlgebra) @@ -143,14 +136,16 @@ record RawFreeValExtension open RawValExtension field - evalᵛ : (ext : RawValExtension A Θ Ψ T) → extension .X .Val ⇾ᵛ ext .X .Val - evalᶜ : (ext : RawValExtension A Θ Ψ T) → extension .X .Comp ⇾ᶜ ext .X .Comp + evalᵛ : (ext : RawValExtension A Θ Ψ T) → extension .X .Val ⇾ᵗ ext .X .Val + evalᶜ : (ext : RawValExtension A Θ Ψ T) → extension .X .Comp ⇾ᵗ ext .X .Comp -- Structures ----------------------------------------------------------------- record IsMonoid (M : RawMonoid) : Set where private module M = RawMonoid M field + subᵛ-cong : (v : M.Val A Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᵛ v σ ≡ M.subᵛ v ς + subᶜ-cong : (c : M.Comp B Γ) → {σ ς : Γ ~[ M.Val ]↝ Δ} → σ ≈ ς → M.subᶜ c σ ≡ M.subᶜ c ς subᵛ-var : (i : Var A Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ (M.var i) σ ≡ σ ＠ i renᵛ-id : (v : M.Val A Γ) → M.renᵛ v id ≡ v subᵛ-assoc : @@ -163,71 +158,64 @@ record IsMonoid (M : RawMonoid) : Set where open ≡-Reasoning + renᵛ-cong : (v : M.Val A Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᵛ v ρ ≡ M.renᵛ v ϱ + renᵛ-cong v ρ≈ϱ = subᵛ-cong v (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_)) + + renᶜ-cong : (c : M.Comp B Γ) → {ρ ϱ : Γ ↝ Δ} → ρ ≈ ϱ → M.renᶜ c ρ ≡ M.renᶜ c ϱ + renᶜ-cong c ρ≈ϱ = subᶜ-cong c (tabulate≈ $ cong M.var ∘ (ρ≈ϱ ＠_)) + renᵛ-var : (i : Var A Γ) (ρ : Γ ↝ Δ) → M.renᵛ (M.var i) ρ ≡ M.var (ρ ＠ i) renᵛ-var i ρ = begin M.renᵛ (M.var i) ρ ≡⟨ subᵛ-var i (ρ ⨾ M.var) ⟩ - (ρ ⨾ M.var) ＠ i ≡⟨ ＠-⨾ ρ M.var i ⟩ M.var (ρ ＠ i) ∎ subᵛ-renᵛ : (v : M.Val A Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) → - M.subᵛ (M.renᵛ v ρ) σ ≡ M.subᵛ v (ρ ⨾ (σ ＠_)) + M.subᵛ (M.renᵛ v ρ) σ ≡ M.subᵛ v (ρ ⨾′ σ) subᵛ-renᵛ v ρ σ = begin M.subᵛ (M.renᵛ v ρ) σ ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) σ ⟩ - M.subᵛ v (ρ ⨾ M.var ⨾ λ ◌ → M.subᵛ ◌ σ) ≡⟨ cong (M.subᵛ v) (⨾-assoc ρ M.var (λ ◌ → M.subᵛ ◌ σ)) ⟩ - M.subᵛ v (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ cong (M.subᵛ v) (⨾-cong ρ (λ v → subᵛ-var v σ)) ⟩ - M.subᵛ v (ρ ⨾ (σ ＠_)) ∎ + M.subᵛ v (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩ + M.subᵛ v (ρ ⨾′ σ) ∎ subᶜ-renᶜ : (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (σ : Δ ~[ M.Val ]↝ Θ) → - M.subᶜ (M.renᶜ c ρ) σ ≡ M.subᶜ c (ρ ⨾ (σ ＠_)) + M.subᶜ (M.renᶜ c ρ) σ ≡ M.subᶜ c (ρ ⨾′ σ) subᶜ-renᶜ c ρ σ = begin M.subᶜ (M.renᶜ c ρ) σ ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) σ ⟩ - M.subᶜ c (ρ ⨾ M.var ⨾ λ ◌ → M.subᵛ ◌ σ) ≡⟨ cong (M.subᶜ c) (⨾-assoc ρ M.var (λ ◌ → M.subᵛ ◌ σ)) ⟩ - M.subᶜ c (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ cong (M.subᶜ c) (⨾-cong ρ (λ v → subᵛ-var v σ)) ⟩ - M.subᶜ c (ρ ⨾ (σ ＠_)) ∎ - - private - lemma : - (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) → - (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡ (ρ ⨾ (ϱ ＠_) ⨾ M.var) - lemma ρ ϱ = begin - (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ ⨾-assoc ρ M.var (λ ◌ → M.renᵛ ◌ ϱ) ⟩ - (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ ⨾-cong ρ (λ v → renᵛ-var v ϱ) ⟩ - (ρ ⨾ λ ◌ → M.var (ϱ ＠ ◌)) ≡˘⟨ ⨾-assoc ρ (ϱ ＠_) M.var ⟩ - (ρ ⨾ (ϱ ＠_) ⨾ M.var) ∎ + M.subᶜ c (ρ ⨾ λ ◌ → M.subᵛ (M.var ◌) σ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → subᵛ-var (ρ ＠ i) σ) ⟩ + M.subᶜ c (ρ ⨾′ σ) ∎ renᵛ-assoc : (v : M.Val A Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) → - M.renᵛ (M.renᵛ v ρ) ϱ ≡ M.renᵛ v (ρ ⨾ (ϱ ＠_)) + M.renᵛ (M.renᵛ v ρ) ϱ ≡ M.renᵛ v (ρ ⨾′ ϱ) renᵛ-assoc v ρ ϱ = begin M.renᵛ (M.renᵛ v ρ) ϱ ≡⟨ subᵛ-assoc v (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩ - M.subᵛ v (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ cong (M.subᵛ v) (lemma ρ ϱ) ⟩ - M.renᵛ v (ρ ⨾ (ϱ ＠_)) ∎ + M.subᵛ v (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᵛ-cong v (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩ + M.renᵛ v (ρ ⨾′ ϱ) ∎ renᶜ-assoc : (c : M.Comp B Γ) (ρ : Γ ↝ Δ) (ϱ : Δ ↝ Θ) → - M.renᶜ (M.renᶜ c ρ) ϱ ≡ M.renᶜ c (ρ ⨾ (ϱ ＠_)) + M.renᶜ (M.renᶜ c ρ) ϱ ≡ M.renᶜ c (ρ ⨾′ ϱ) renᶜ-assoc c ρ ϱ = begin M.renᶜ (M.renᶜ c ρ) ϱ ≡⟨ subᶜ-assoc c (ρ ⨾ M.var) (ϱ ⨾ M.var) ⟩ - M.subᶜ c (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ ϱ) ≡⟨ cong (M.subᶜ c) (lemma ρ ϱ) ⟩ - M.renᶜ c (ρ ⨾ (ϱ ＠_)) ∎ + M.subᶜ c (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) ϱ) ≡⟨ subᶜ-cong c (tabulate≈ $ λ i → renᵛ-var (ρ ＠ i) ϱ) ⟩ + M.renᶜ c (ρ ⨾′ ϱ) ∎ lift-ren : (Θ : Context) (ρ : Γ ↝ Δ) → - M.lift Θ (ρ ⨾ M.var) ≡ copair (ρ ⨾ weaklF Θ) weakr ⨾ M.var - lift-ren Θ ρ = begin - M.lift Θ (ρ ⨾ M.var) ≡⟨⟩ - copair (ρ ⨾ M.var ⨾ λ ◌ → M.renᵛ ◌ (weakl Θ)) (weakr ⨾ M.var) ≡⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-assoc ρ M.var (λ ◌ → M.renᵛ ◌ (weakl Θ))) ⟩ - copair (ρ ⨾ λ ◌ → M.renᵛ (M.var ◌) (weakl Θ)) (weakr ⨾ M.var) ≡⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-cong ρ (λ v → trans (renᵛ-var v (weakl Θ)) (cong M.var (＠-tabulate Var (weaklF Θ) v)))) ⟩ - copair (ρ ⨾ λ ◌ → M.var (weaklF Θ ◌)) (weakr ⨾ M.var) ≡˘⟨ cong (λ ◌ → copair ◌ (weakr ⨾ M.var)) (⨾-assoc ρ (weaklF Θ) M.var) ⟩ - copair (ρ ⨾ weaklF Θ ⨾ M.var) (weakr ⨾ M.var) ≡⟨ copair-⨾ (ρ ⨾ weaklF Θ) weakr M.var ⟩ - copair (ρ ⨾ weaklF Θ) weakr ⨾ M.var ∎ + M.lift Θ (ρ ⨾ M.var) ≈ lift′ Θ ρ ⨾ M.var + lift-ren Θ ρ = + copair-unique {X = M.Val} _ _ _ + (tabulate≈ $ λ i → begin + M.var ((ρ ⨾ weaklF Θ ∥ weakr) ＠ weakl Θ ＠ i) ≡⟨ cong M.var (copair-weakl {Δ = Θ} (ρ ⨾ weaklF Θ) weakr ＠ i) ⟩ + M.var (weaklF Θ $ ρ ＠ i) ≡˘⟨ renᵛ-var (ρ ＠ i) (weakl Θ) ⟩ + M.renᵛ (M.var $ ρ ＠ i) (weakl Θ) ∎) + (tabulate≈ $ λ i → cong M.var (copair-weakr (ρ ⨾ weaklF Θ) weakr ＠ i)) record IsMonoidArrow (M N : RawMonoid) - (fᵛ : RawMonoid.Val M ⇾ᵛ RawMonoid.Val N) - (fᶜ : RawMonoid.Comp M ⇾ᶜ RawMonoid.Comp N) : Set + (fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N) + (fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N) : Set where private module M = RawMonoid M @@ -241,20 +229,33 @@ record IsMonoidArrow (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → fᶜ (M.subᶜ c σ) ≡ N.subᶜ (fᶜ c) (σ ⨾ fᵛ) +module MonArrow + {M N} + {fᵛ : RawMonoid.Val M ⇾ᵗ RawMonoid.Val N} + {fᶜ : RawMonoid.Comp M ⇾ᵗ RawMonoid.Comp N} + (arr : IsMonoidArrow M N fᵛ fᶜ) + (Nᵐ : IsMonoid N) + where + + private + module M = RawMonoid M + module N where + open RawMonoid N public + open IsMonoid Nᵐ public + + open IsMonoidArrow arr open ≡-Reasoning ⟨renᵛ⟩ : (v : M.Val A Γ) (ρ : Γ ↝ Δ) → fᵛ (M.renᵛ v ρ) ≡ N.renᵛ (fᵛ v) ρ ⟨renᵛ⟩ v ρ = begin fᵛ (M.renᵛ v ρ) ≡⟨ ⟨subᵛ⟩ v (ρ ⨾ M.var) ⟩ - N.subᵛ (fᵛ v) (ρ ⨾ M.var ⨾ fᵛ) ≡⟨ cong (N.subᵛ (fᵛ v)) (⨾-assoc ρ M.var fᵛ) ⟩ - N.subᵛ (fᵛ v) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ cong (N.subᵛ (fᵛ v)) (⨾-cong ρ ⟨var⟩) ⟩ + N.subᵛ (fᵛ v) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᵛ-cong (fᵛ v) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩ N.renᵛ (fᵛ v) ρ ∎ ⟨renᶜ⟩ : (c : M.Comp B Γ) (ρ : Γ ↝ Δ) → fᶜ (M.renᶜ c ρ) ≡ N.renᶜ (fᶜ c) ρ ⟨renᶜ⟩ c ρ = begin fᶜ (M.renᶜ c ρ) ≡⟨ ⟨subᶜ⟩ c (ρ ⨾ M.var) ⟩ - N.subᶜ (fᶜ c) (ρ ⨾ M.var ⨾ fᵛ) ≡⟨ cong (N.subᶜ (fᶜ c)) (⨾-assoc ρ M.var fᵛ) ⟩ - N.subᶜ (fᶜ c) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ cong (N.subᶜ (fᶜ c)) (⨾-cong ρ ⟨var⟩) ⟩ + N.subᶜ (fᶜ c) (ρ ⨾ λ ◌ → fᵛ (M.var ◌)) ≡⟨ N.subᶜ-cong (fᶜ c) (tabulate≈ $ λ i → ⟨var⟩ (ρ ＠ i)) ⟩ N.renᶜ (fᶜ c) ρ ∎ record IsAlgebra (M : RawAlgebra) : Set where @@ -266,7 +267,7 @@ record IsAlgebra (M : RawAlgebra) : Set where field sub-have : - (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → + (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.have v be c) σ ≡ (M.have M.subᵛ v σ be M.subᶜ c (M.lift [< x :- A ] σ)) sub-thunk : (c : M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → @@ -282,7 +283,7 @@ record IsAlgebra (M : RawAlgebra) : Set where (v : M.Val A Γ) (w : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ M.⟨ v , w ⟩ σ ≡ M.⟨ M.subᵛ v σ , M.subᵛ w σ ⟩ sub-split : - (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → + (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.split v then c) σ ≡ (M.split M.subᵛ v σ then M.subᶜ c (M.lift [< x :- A , y :- A′ ] σ)) sub-inl : @@ -292,7 +293,7 @@ record IsAlgebra (M : RawAlgebra) : Set where (v : M.Val A′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᵛ (M.inr {A = A} v) σ ≡ M.inr (M.subᵛ v σ) sub-case : - (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) → + (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) → (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.case v of c or d) σ ≡ (M.case M.subᵛ v σ of M.subᶜ c (M.lift [< x :- A ] σ) or M.subᶜ d (M.lift [< y :- A′ ] σ)) @@ -300,7 +301,7 @@ record IsAlgebra (M : RawAlgebra) : Set where (v : M.Val A Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.ret v) σ ≡ M.ret (M.subᵛ v σ) sub-bind : - (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → + (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.bind c to d) σ ≡ (M.bind M.subᶜ c σ to M.subᶜ d (M.lift [< x :- A ] σ)) sub-bundle : (c : M.Comp B Γ) (d : M.Comp B′ Γ) (σ : Γ ~[ M.Val ]↝ Δ) → @@ -312,7 +313,7 @@ record IsAlgebra (M : RawAlgebra) : Set where (c : M.Comp (B × B′) Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.snd c) σ ≡ M.snd (M.subᶜ c σ) sub-pop : - (c : δᶜ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → + (c : δᵗ [< x :- A ] M.Comp B Γ) (σ : Γ ~[ M.Val ]↝ Δ) → M.subᶜ (M.pop c) σ ≡ M.pop (M.subᶜ c (M.lift [< x :- A ] σ)) sub-push : (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) (σ : Γ ~[ M.Val ]↝ Δ) → @@ -321,15 +322,15 @@ record IsAlgebra (M : RawAlgebra) : Set where open ≡-Reasoning ren-have : - (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → - M.renᶜ (M.have v be c) ρ ≡ (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)) + (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → + M.renᶜ (M.have v be c) ρ ≡ (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (lift′ [< x :- A ] ρ)) ren-have {x = x} v c ρ = begin M.renᶜ (M.have v be c) ρ ≡⟨ sub-have v c (ρ ⨾ M.var) ⟩ (M.have M.renᵛ v ρ be M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var))) - ≡⟨ cong (λ ◌ → M.have M.renᵛ v ρ be M.subᶜ c ◌) (lift-ren [< x :- _ ] ρ) ⟩ - (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)) + ≡⟨ cong (λ ◌ → M.have M.renᵛ v ρ be ◌) (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩ + (M.have M.renᵛ v ρ be[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ)) ∎ ren-thunk : @@ -356,20 +357,16 @@ record IsAlgebra (M : RawAlgebra) : Set where ren-pair v w ρ = sub-pair v w (ρ ⨾ M.var) ren-split : - (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) (ρ : Γ ↝ Δ) → + (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) (ρ : Γ ↝ Δ) → M.renᶜ (M.split v then c) ρ ≡ - ( M.split M.renᵛ v ρ - then[ x , y ] M.renᶜ c (ρ ⨾ (ThereVar ∘ ThereVar) :< x ↦ %% x :< y ↦ %% y) - ) + (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , y :- _ ] ρ)) ren-split {x = x} {y = y} v c ρ = begin M.renᶜ (M.split v then c) ρ ≡⟨ sub-split v c (ρ ⨾ M.var) ⟩ (M.split M.subᵛ v (ρ ⨾ M.var) then M.subᶜ c (M.lift [< x :- _ , y :- _ ] (ρ ⨾ M.var))) - ≡⟨ cong (λ ◌ → M.split M.subᵛ v (ρ ⨾ M.var) then M.subᶜ c ◌) (lift-ren [< x :- _ , y :- _ ] ρ) ⟩ - ( M.split M.renᵛ v ρ - then[ x , y ] M.renᶜ c (ρ ⨾ (ThereVar ∘ ThereVar) :< x ↦ %% x :< y ↦ %% y) - ) + ≡⟨ cong (λ ◌ → M.split M.subᵛ v (ρ ⨾ M.var) then ◌) (subᶜ-cong c $ lift-ren [< x :- _ , y :- _ ] ρ) ⟩ + (M.split M.renᵛ v ρ then[ x , y ] M.renᶜ c (lift′ [< x :- _ , y :- _ ] ρ)) ∎ ren-inl : @@ -383,12 +380,12 @@ record IsAlgebra (M : RawAlgebra) : Set where ren-inr v ρ = sub-inr v (ρ ⨾ M.var) ren-case : - (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) → + (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) → (ρ : Γ ↝ Δ) → M.renᶜ (M.case v of c or d) ρ ≡ ( M.case M.renᵛ v ρ - of[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x) - or[ y ] M.renᶜ d (ρ ⨾ ThereVar :< y ↦ %% y)) + of[ x ] M.renᶜ c (lift′ [< x :- A ] ρ) + or[ y ] M.renᶜ d (lift′ [< y :- A′ ] ρ)) ren-case {x = x} {y = y} v c d ρ = begin M.renᶜ (M.case v of c or d) ρ @@ -396,12 +393,12 @@ record IsAlgebra (M : RawAlgebra) : Set where ( M.case M.subᵛ v (ρ ⨾ M.var) of M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var)) or M.subᶜ d (M.lift [< y :- _ ] (ρ ⨾ M.var))) - ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → M.case M.subᵛ v (ρ ⨾ M.var) of M.subᶜ c ◌ᵃ or M.subᶜ d ◌ᵇ) - (lift-ren [< x :- _ ] ρ) - (lift-ren [< y :- _ ] ρ) ⟩ + ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → M.case M.subᵛ v (ρ ⨾ M.var) of ◌ᵃ or ◌ᵇ) + (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) + (subᶜ-cong d $ lift-ren [< y :- _ ] ρ) ⟩ ( M.case M.subᵛ v (ρ ⨾ M.var) - of[ x ] M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x) - or[ y ] M.renᶜ d (ρ ⨾ ThereVar :< y ↦ %% y)) + of[ x ] M.renᶜ c (lift′ [< x :- _ ] ρ) + or[ y ] M.renᶜ d (lift′ [< y :- _ ] ρ)) ∎ ren-ret : @@ -410,15 +407,15 @@ record IsAlgebra (M : RawAlgebra) : Set where ren-ret v ρ = sub-ret v (ρ ⨾ M.var) ren-bind : - (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → - M.renᶜ (M.bind c to d) ρ ≡ (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (ρ ⨾ ThereVar :< x ↦ %% x)) + (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → + M.renᶜ (M.bind c to d) ρ ≡ (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (lift′ [< x :- A ] ρ)) ren-bind {x = x} c d ρ = begin M.renᶜ (M.bind c to d) ρ ≡⟨ sub-bind c d (ρ ⨾ M.var) ⟩ (M.bind M.renᶜ c ρ to M.subᶜ d (M.lift [< x :- _ ] (ρ ⨾ M.var))) - ≡⟨ cong (λ ◌ → M.bind M.renᶜ c ρ to M.subᶜ d ◌) (lift-ren [< x :- _ ] ρ) ⟩ - (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (ρ ⨾ ThereVar :< x ↦ %% x)) + ≡⟨ cong (λ ◌ → M.bind M.renᶜ c ρ to ◌) (subᶜ-cong d $ lift-ren [< x :- _ ] ρ) ⟩ + (M.bind M.renᶜ c ρ to[ x ] M.renᶜ d (lift′ [< x :- _ ] ρ)) ∎ ren-bundle : @@ -437,15 +434,15 @@ record IsAlgebra (M : RawAlgebra) : Set where ren-snd c ρ = sub-snd c (ρ ⨾ M.var) ren-pop : - (c : δᶜ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → - M.renᶜ (M.pop c) ρ ≡ M.pop[ x ] (M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)) + (c : δᵗ [< x :- A ] M.Comp B Γ) (ρ : Γ ↝ Δ) → + M.renᶜ (M.pop c) ρ ≡ M.pop[ x ] (M.renᶜ c (lift′ [< x :- A ] ρ)) ren-pop {x = x} c ρ = begin M.renᶜ (M.pop c) ρ ≡⟨ sub-pop c (ρ ⨾ M.var) ⟩ M.pop (M.subᶜ c (M.lift [< x :- _ ] (ρ ⨾ M.var))) - ≡⟨ cong (M.pop ∘ M.subᶜ c) (lift-ren [< x :- _ ] ρ) ⟩ - M.pop[ x ] (M.renᶜ c (ρ ⨾ ThereVar :< x ↦ %% x)) + ≡⟨ cong M.pop (subᶜ-cong c $ lift-ren [< x :- _ ] ρ) ⟩ + M.pop[ x ] (M.renᶜ c (lift′ [< x :- _ ] ρ)) ∎ ren-push : @@ -462,19 +459,19 @@ record IsModel (M : RawAlgebra) : Set where field have-beta : - (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) → (M.have v be c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) force-beta : (c : M.Comp B Γ) → M.force (M.thunk c) ≡ c thunk-eta : (v : M.Val (U B) Γ) → M.thunk (M.force v) ≡ v point-beta : (c : M.Comp B Γ) → (M.drop M.point then c) ≡ c drop-eta : - (v : M.Val 𝟙 Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val 𝟙 Γ) (c : δᵗ _ M.Comp B Γ) → (M.drop v then M.subᶜ c (id ⨾ M.var :< x ↦ M.point)) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) pair-beta : - (v : M.Val A Γ) (w : M.Val A′ Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val A Γ) (w : M.Val A′ Γ) (c : δᵗ _ M.Comp B Γ) → (M.split M.⟨ v , w ⟩ then c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v :< y ↦ w) pair-eta : - (v : M.Val (A × A′) Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val (A × A′) Γ) (c : δᵗ _ M.Comp B Γ) → (M.split v then M.subᶜ c ( weakl [< y :- A , z :- A′ ] ⨾ M.var @@ -483,40 +480,40 @@ record IsModel (M : RawAlgebra) : Set where ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) inl-beta : - (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) → + (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) → (M.case (M.inl v) of c or d) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) inr-beta : - (v : M.Val A′ Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ _ M.Comp B Γ) → + (v : M.Val A′ Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ _ M.Comp B Γ) → (M.case (M.inr v) of c or d) ≡ M.subᶜ d (id ⨾ M.var :< y ↦ v) case-eta : - (v : M.Val (A + A′) Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val (A + A′) Γ) (c : δᵗ _ M.Comp B Γ) → ( M.case v of M.subᶜ c (weakl [< y :- A ] ⨾ M.var :< x ↦ M.inl (M.var $ %% y)) or M.subᶜ c (weakl [< z :- A′ ] ⨾ M.var :< x ↦ M.inr (M.var $ %% z))) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) ret-beta : - (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) → (M.bind M.ret v to c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) bind-bind-comm : - (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (F A′) Γ) (e : δᶜ [< y :- A′ ] M.Comp B Γ) → + (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (F A′) Γ) (e : δᵗ [< y :- A′ ] M.Comp B Γ) → (M.bind (M.bind c to d) to e) ≡ (M.bind c to M.bind d to M.subᶜ e (weakl [< x :- _ , y :- _ ] ⨾ M.var :< y ↦ M.var (%% y))) bind-fst-comm : - (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (B × B′) Γ) → + (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (B × B′) Γ) → (M.bind c to M.fst d) ≡ M.fst (M.bind c to d) bind-snd-comm : - (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp (B × B′) Γ) → + (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp (B × B′) Γ) → (M.bind c to M.snd d) ≡ M.snd (M.bind c to d) bind-push-comm : - (v : M.Val A Γ) (c : M.Comp (F A′) Γ) (d : δᶜ [< x :- A′ ] M.Comp (A ⟶ B) Γ) → + (v : M.Val A Γ) (c : M.Comp (F A′) Γ) (d : δᵗ [< x :- A′ ] M.Comp (A ⟶ B) Γ) → (M.push v then M.bind c to d) ≡ (M.bind c to M.push M.subᵛ v (weakl _ ⨾ M.var) then d) fst-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.fst M.⟪ c , d ⟫ ≡ c snd-beta : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → M.snd M.⟪ c , d ⟫ ≡ d bundle-eta : (c : M.Comp (B × B′) Γ) → M.⟪ M.fst c , M.snd c ⟫ ≡ c push-beta : - (v : M.Val A Γ) (c : δᶜ _ M.Comp B Γ) → + (v : M.Val A Γ) (c : δᵗ _ M.Comp B Γ) → (M.push v then M.pop c) ≡ M.subᶜ c (id ⨾ M.var :< x ↦ v) push-eta : (c : M.Comp (A ⟶ B) Γ) → @@ -524,33 +521,33 @@ record IsModel (M : RawAlgebra) : Set where record IsAlgebraArrow (M N : RawAlgebra) - (fᵛ : M .Val ⇾ᵛ N .Val) (fᶜ : M .Comp ⇾ᶜ N .Comp) : Set + (fᵛ : M .Val ⇾ᵗ N .Val) (fᶜ : M .Comp ⇾ᵗ N .Comp) : Set where private module M = RawAlgebra M module N = RawAlgebra N field isMonoidArrow : IsMonoidArrow M.monoid N.monoid fᵛ fᶜ - ⟨have⟩ : (v : M.Val A Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.have v be c) ≡ (N.have fᵛ v be fᶜ c) + ⟨have⟩ : (v : M.Val A Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.have v be c) ≡ (N.have fᵛ v be fᶜ c) ⟨thunk⟩ : (c : M.Comp B Γ) → fᵛ (M.thunk c) ≡ N.thunk (fᶜ c) ⟨force⟩ : (v : M.Val (U B) Γ) → fᶜ (M.force v) ≡ N.force (fᵛ v) ⟨point⟩ : fᵛ M.point ≡ N.point {Γ = Γ} ⟨drop⟩ : (v : M.Val 𝟙 Γ) (c : M.Comp B Γ) → fᶜ (M.drop v then c) ≡ (N.drop fᵛ v then fᶜ c) ⟨pair⟩ : (v : M.Val A Γ) (w : M.Val A′ Γ) → fᵛ M.⟨ v , w ⟩ ≡ N.⟨ fᵛ v , fᵛ w ⟩ ⟨split⟩ : - (v : M.Val (A × A′) Γ) (c : δᶜ [< x :- A , y :- A′ ] M.Comp B Γ) → + (v : M.Val (A × A′) Γ) (c : δᵗ [< x :- A , y :- A′ ] M.Comp B Γ) → fᶜ (M.split v then c) ≡ (N.split fᵛ v then fᶜ c) ⟨inl⟩ : (v : M.Val A Γ) → fᵛ {A + A′} (M.inl v) ≡ N.inl (fᵛ v) ⟨inr⟩ : (v : M.Val A′ Γ) → fᵛ {A + A′} (M.inr v) ≡ N.inr (fᵛ v) ⟨case⟩ : - (v : M.Val (A + A′) Γ) (c : δᶜ [< x :- A ] M.Comp B Γ) (d : δᶜ [< y :- A′ ] M.Comp B Γ) → + (v : M.Val (A + A′) Γ) (c : δᵗ [< x :- A ] M.Comp B Γ) (d : δᵗ [< y :- A′ ] M.Comp B Γ) → fᶜ (M.case v of c or d) ≡ (N.case fᵛ v of fᶜ c or fᶜ d) ⟨ret⟩ : (v : M.Val A Γ) → fᶜ (M.ret v) ≡ N.ret (fᵛ v) - ⟨bind⟩ : (c : M.Comp (F A) Γ) (d : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.bind c to d) ≡ (N.bind fᶜ c to fᶜ d) + ⟨bind⟩ : (c : M.Comp (F A) Γ) (d : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.bind c to d) ≡ (N.bind fᶜ c to fᶜ d) ⟨bundle⟩ : (c : M.Comp B Γ) (d : M.Comp B′ Γ) → fᶜ M.⟪ c , d ⟫ ≡ N.⟪ fᶜ c , fᶜ d ⟫ ⟨fst⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.fst c) ≡ N.fst (fᶜ c) ⟨snd⟩ : (c : M.Comp (B × B′) Γ) → fᶜ (M.snd c) ≡ N.snd (fᶜ c) - ⟨pop⟩ : (c : δᶜ [< x :- A ] M.Comp B Γ) → fᶜ (M.pop c) ≡ N.pop (fᶜ c) + ⟨pop⟩ : (c : δᵗ [< x :- A ] M.Comp B Γ) → fᶜ (M.pop c) ≡ N.pop (fᶜ c) ⟨push⟩ : (v : M.Val A Γ) (c : M.Comp (A ⟶ B) Γ) → fᶜ (M.push v then c) ≡ (N.push fᵛ v then fᶜ c) record IsCompExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawCompExtension A Θ Ψ T) : Set where @@ -572,8 +569,8 @@ record IsValExtension {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawValExtension A Θ X .subᵛ (dyn vs cs) σ ≡ dyn (map (λ ◌ → X .subᵛ ◌ σ) vs) (map (λ ◌ → X .subᶜ ◌ σ) cs) record IsCompExtArrow {A Θ Ψ T} (M N : RawCompExtension A Θ Ψ T) - (fᵛ : RawCompExtension.X M .Val ⇾ᵛ RawCompExtension.X N .Val) - (fᶜ : RawCompExtension.X M .Comp ⇾ᶜ RawCompExtension.X N .Comp) : Set + (fᵛ : RawCompExtension.X M .Val ⇾ᵗ RawCompExtension.X N .Val) + (fᶜ : RawCompExtension.X M .Comp ⇾ᵗ RawCompExtension.X N .Comp) : Set where private module M = RawCompExtension M @@ -587,8 +584,8 @@ record IsCompExtArrow {A Θ Ψ T} (M N : RawCompExtension A Θ Ψ T) fᶜ (M.dyn vs cs) ≡ N.dyn (map fᵛ vs) (map fᶜ cs) record IsValExtArrow {A Θ Ψ T} (M N : RawValExtension A Θ Ψ T) - (fᵛ : RawValExtension.X M .Val ⇾ᵛ RawValExtension.X N .Val) - (fᶜ : RawValExtension.X M .Comp ⇾ᶜ RawValExtension.X N .Comp) : Set + (fᵛ : RawValExtension.X M .Val ⇾ᵗ RawValExtension.X N .Val) + (fᶜ : RawValExtension.X M .Comp ⇾ᵗ RawValExtension.X N .Comp) : Set where private module M = RawValExtension M @@ -611,15 +608,15 @@ record IsFreeCompExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeCompExtension A IsCompExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext) eval-uniqueᵛ : (ext : RawCompExtension A Θ Ψ T) → - (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) → - (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) → + (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) → + (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) → IsCompExtArrow M.extension ext fᵛ fᶜ → (v : M.extension .X .Val A′ Γ) → fᵛ v ≡ M.evalᵛ ext v eval-uniqueᶜ : (ext : RawCompExtension A Θ Ψ T) → - (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) → - (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) → + (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) → + (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) → IsCompExtArrow M.extension ext fᵛ fᶜ → (c : M.extension .X .Comp B Γ) → fᶜ c ≡ M.evalᶜ ext c @@ -634,15 +631,15 @@ record IsFreeValExt {A Θ Ψ T} (Aᴹ : IsModel A) (M : RawFreeValExtension A Θ IsValExtArrow M.extension ext (M.evalᵛ ext) (M.evalᶜ ext) eval-uniqueᵛ : (ext : RawValExtension A Θ Ψ T) → - (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) → - (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) → + (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) → + (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) → IsValExtArrow M.extension ext fᵛ fᶜ → (v : M.extension .X .Val A′ Γ) → fᵛ v ≡ M.evalᵛ ext v eval-uniqueᶜ : (ext : RawValExtension A Θ Ψ T) → - (fᵛ : M.extension .X .Val ⇾ᵛ ext .X .Val) → - (fᶜ : M.extension .X .Comp ⇾ᶜ ext .X .Comp) → + (fᵛ : M.extension .X .Val ⇾ᵗ ext .X .Val) → + (fᶜ : M.extension .X .Comp ⇾ᵗ ext .X .Comp) → IsValExtArrow M.extension ext fᵛ fᶜ → (c : M.extension .X .Comp B Γ) → fᶜ c ≡ M.evalᶜ ext c |