From 25feb8c72e5e4a76fbd4ab381105de6c19d6ab50 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 19 Feb 2025 15:47:36 +0000 Subject: Update to stdlib 2.1.1 and other changes. I don't fully know what has changed because the changes are so old. Doesn't yet compile due to not finishing proofs in `CBPV.Frex.Comp`. --- src/CBPV/Structure.agda | 279 ++++++++++++++++++++++++------------------------ 1 file changed, 138 insertions(+), 141 deletions(-) (limited to 'src/CBPV/Structure.agda') 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 -- cgit v1.2.3