diff options
Diffstat (limited to 'Data/System/Values.agda')
| -rw-r--r-- | Data/System/Values.agda | 445 |
1 files changed, 408 insertions, 37 deletions
diff --git a/Data/System/Values.agda b/Data/System/Values.agda index 545a835..d1cd6c9 100644 --- a/Data/System/Values.agda +++ b/Data/System/Values.agda @@ -5,53 +5,98 @@ open import Level using (0ℓ) module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where -import Algebra.Properties.CommutativeMonoid.Sum as Sum -import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise -import Relation.Binary.PropositionalEquality as ≡ +open import Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) -open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt) -open import Data.Nat using (ℕ; _+_; suc) -open import Data.Product using (_,_) +import Algebra.Properties.CommutativeMonoid.Sum A as Sum +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise +import Object.Monoid.Commutative Setoids-×.symmetric as Obj +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Data.Bool using (Bool; if_then_else_) +open import Data.Bool.Properties using (if-cong) +open import Data.Monoid using (module FromMonoid) +open import Data.CMonoid using (fromCMonoid) +open import Data.Fin using (Fin; splitAt; _↑ˡ_; _↑ʳ_; punchIn; punchOut) +open import Data.Fin using (_≟_) +open import Data.Fin.Permutation using (Permutation; Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; id; flip; inverseˡ; inverseʳ; punchIn-permute; insert; remove) +open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) +open import Data.Fin.Properties using (punchIn-punchOut) +open import Data.Nat using (ℕ; _+_) +open import Data.Product using (_,_; Σ-syntax) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Setoid using (∣_∣) +open import Data.Subset.Functional using (Subset; ⁅_⁆; ⁅⁆∘ρ) open import Data.Sum using (inj₁; inj₂) open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate) open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_) open import Level using (0ℓ) open import Relation.Binary using (Rel; Setoid; IsEquivalence) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Relation.Nullary.Decidable using (yes; no) -open CommutativeMonoid A renaming (Carrier to Value) +open Bool +open CommutativeMonoid A renaming (Carrier to Value; setoid to Valueₛ) +open Fin open Func -open Sum A using (sum) - -open Pointwise setoid using (≋-setoid; ≋-isEquivalence) +open Pointwise Valueₛ using (≋-setoid; ≋-isEquivalence) +open ℕ opaque - Values : ℕ → Setoid 0ℓ 0ℓ Values = ≋-setoid +_when_ : Value → Bool → Value +x when b = if b then x else ε + +-- when preserves setoid equivalence +when-cong + : {x y : Value} + → x ≈ y + → (b : Bool) + → x when b ≈ y when b +when-cong _ false = refl +when-cong x≈y true = x≈y + module _ {n : ℕ} where opaque unfolding Values - merge : ∣ Values n ∣ → Value - merge = sum - _⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣ xs ⊕ ys = zipWith _∙_ xs ys <ε> : ∣ Values n ∣ <ε> = replicate n ε + mask : Subset n → ∣ Values n ∣ → ∣ Values n ∣ + mask S v i = v i when S i + + sum : ∣ Values n ∣ → Value + sum = Sum.sum + + merge : ∣ Values n ∣ → Subset n → Value + merge v S = sum (mask S v) + + -- mask preserves setoid equivalence + maskₛ : Subset n → Values n ⟶ₛ Values n + maskₛ S .to = mask S + maskₛ S .cong v≋w i = when-cong (v≋w i) (S i) + + -- sum preserves setoid equivalence + sumₛ : Values n ⟶ₛ Valueₛ + sumₛ .to = Sum.sum + sumₛ .cong = Sum.sum-cong-≋ + head : ∣ Values (suc n) ∣ → Value head xs = xs zero tail : ∣ Values (suc n) ∣ → ∣ Values n ∣ tail xs = xs ∘ suc + lookup : ∣ Values n ∣ → Fin n → Value + lookup v i = v i + module ≋ = Setoid (Values n) _≋_ : Rel ∣ Values n ∣ 0ℓ @@ -59,16 +104,45 @@ module _ {n : ℕ} where infix 4 _≋_ -opaque + opaque + + unfolding merge + + -- merge preserves setoid equivalence + merge-cong + : (S : Subset n) + → {xs ys : ∣ Values n ∣} + → xs ≋ ys + → merge xs S ≈ merge ys S + merge-cong S {xs} {ys} xs≋ys = cong sumₛ (cong (maskₛ S) xs≋ys) + + mask-cong₁ + : {S₁ S₂ : Subset n} + → S₁ ≗ S₂ + → (xs : ∣ Values n ∣) + → mask S₁ xs ≋ mask S₂ xs + mask-cong₁ S₁≋S₂ _ i = reflexive (if-cong (S₁≋S₂ i)) + + merge-cong₂ + : (xs : ∣ Values n ∣) + → {S₁ S₂ : Subset n} + → S₁ ≗ S₂ + → merge xs S₁ ≈ merge xs S₂ + merge-cong₂ xs S₁≋S₂ = cong sumₛ (mask-cong₁ S₁≋S₂ xs) + +module _ where - unfolding Values open Setoid - ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n)) - ≋-isEquiv = ≋-isEquivalence + + opaque + unfolding Values + ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n)) + ≋-isEquiv = ≋-isEquivalence module _ {n : ℕ} where opaque + unfolding _⊕_ ⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v @@ -86,25 +160,35 @@ module _ {n : ℕ} where ⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x ⊕-comm x y i = comm (x i) (y i) -open CommutativeMonoid -Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ -Valuesₘ n .Carrier = ∣ Values n ∣ -Valuesₘ n ._≈_ = _≋_ -Valuesₘ n ._∙_ = _⊕_ -Valuesₘ n .ε = <ε> -Valuesₘ n .isCommutativeMonoid = record - { isMonoid = record - { isSemigroup = record - { isMagma = record - { isEquivalence = ≋-isEquiv n - ; ∙-cong = ⊕-cong - } - ; assoc = ⊕-assoc - } - ; identity = ⊕-identityˡ , ⊕-identityʳ - } - ; comm = ⊕-comm - } +module Algebra where + + open CommutativeMonoid + + Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ + Valuesₘ n .Carrier = ∣ Values n ∣ + Valuesₘ n ._≈_ = _≋_ + Valuesₘ n ._∙_ = _⊕_ + Valuesₘ n .ε = <ε> + Valuesₘ n .isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≋-isEquiv n + ; ∙-cong = ⊕-cong + } + ; assoc = ⊕-assoc + } + ; identity = ⊕-identityˡ , ⊕-identityʳ + } + ; comm = ⊕-comm + } + +module Object where + + opaque + unfolding FromMonoid.μ + Valuesₘ : ℕ → Obj.CommutativeMonoid + Valuesₘ n = fromCMonoid (Algebra.Valuesₘ n) opaque @@ -144,3 +228,290 @@ module _ {n m : ℕ} where ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m) to ++ₛ (xs , ys) = xs ++ ys cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +opaque + + unfolding merge + + mask-⊕ + : {n : ℕ} + (xs ys : ∣ Values n ∣) + (S : Subset n) + → mask S (xs ⊕ ys) ≋ mask S xs ⊕ mask S ys + mask-⊕ xs ys S i with S i + ... | false = sym (identityˡ ε) + ... | true = refl + + sum-⊕ + : {n : ℕ} + → (xs ys : ∣ Values n ∣) + → sum (xs ⊕ ys) ≈ sum xs ∙ sum ys + sum-⊕ {zero} xs ys = sym (identityˡ ε) + sum-⊕ {suc n} xs ys = begin + (head xs ∙ head ys) ∙ sum (tail xs ⊕ tail ys) ≈⟨ ∙-congˡ (sum-⊕ (tail xs) (tail ys)) ⟩ + (head xs ∙ head ys) ∙ (sum (tail xs) ∙ sum (tail ys)) ≈⟨ assoc (head xs) (head ys) _ ⟩ + head xs ∙ (head ys ∙ (sum (tail xs) ∙ sum (tail ys))) ≈⟨ ∙-congˡ (assoc (head ys) (sum (tail xs)) _) ⟨ + head xs ∙ ((head ys ∙ sum (tail xs)) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (∙-congʳ (comm (head ys) (sum (tail xs)))) ⟩ + head xs ∙ ((sum (tail xs) ∙ head ys) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (assoc (sum (tail xs)) (head ys) _) ⟩ + head xs ∙ (sum (tail xs) ∙ (head ys ∙ sum (tail ys))) ≈⟨ assoc (head xs) (sum (tail xs)) _ ⟨ + (head xs ∙ sum (tail xs)) ∙ (head ys ∙ sum (tail ys)) ∎ + where + open ≈-Reasoning Valueₛ + + merge-⊕ + : {n : ℕ} + (xs ys : ∣ Values n ∣) + (S : Subset n) + → merge (xs ⊕ ys) S ≈ merge xs S ∙ merge ys S + merge-⊕ {n} xs ys S = begin + sum (mask S (xs ⊕ ys)) ≈⟨ cong sumₛ (mask-⊕ xs ys S) ⟩ + sum (mask S xs ⊕ mask S ys) ≈⟨ sum-⊕ (mask S xs) (mask S ys) ⟩ + sum (mask S xs) ∙ sum (mask S ys) ∎ + where + open ≈-Reasoning Valueₛ + + mask-<ε> : {n : ℕ} (S : Subset n) → mask {n} S <ε> ≋ <ε> + mask-<ε> S i with S i + ... | false = refl + ... | true = refl + + sum-<ε> : (n : ℕ) → sum {n} <ε> ≈ ε + sum-<ε> zero = refl + sum-<ε> (suc n) = trans (identityˡ (sum {n} <ε>)) (sum-<ε> n) + + merge-<ε> : {n : ℕ} (S : Subset n) → merge {n} <ε> S ≈ ε + merge-<ε> {n} S = begin + sum (mask S <ε>) ≈⟨ cong sumₛ (mask-<ε> S) ⟩ + sum {n} <ε> ≈⟨ sum-<ε> n ⟩ + ε ∎ + where + open ≈-Reasoning Valueₛ + + merge-⁅⁆ + : {n : ℕ} + (xs : ∣ Values n ∣) + (i : Fin n) + → merge xs ⁅ i ⁆ ≈ lookup xs i + merge-⁅⁆ {suc n} xs zero = trans (∙-congˡ (sum-<ε> n)) (identityʳ (head xs)) + merge-⁅⁆ {suc n} xs (suc i) = begin + ε ∙ merge (tail xs) ⁅ i ⁆ ≈⟨ identityˡ (sum (mask ⁅ i ⁆ (tail xs))) ⟩ + merge (tail xs) ⁅ i ⁆ ≈⟨ merge-⁅⁆ (tail xs) i ⟩ + tail xs i ∎ + where + open ≈-Reasoning Valueₛ + +opaque + + unfolding Values + + push : {A B : ℕ} → ∣ Values A ∣ → (Fin A → Fin B) → ∣ Values B ∣ + push v f = merge v ∘ preimage f ∘ ⁅_⁆ + + pull : {A B : ℕ} → ∣ Values B ∣ → (Fin A → Fin B) → ∣ Values A ∣ + pull v f = v ∘ f + +insert-f0-0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero) +insert-f0-0 {A} {B} f = ρ , ρf0≡0 + where + ρ : Permutation′ (suc B) + ρ = insert (f zero) zero id + ρf0≡0 : ρ ⟨$⟩ʳ f zero ≡ zero + ρf0≡0 with f zero ≟ f zero + ... | yes _ = ≡.refl + ... | no f0≢f0 with () ← f0≢f0 ≡.refl + +opaque + unfolding push + push-cong + : {A B : ℕ} + → (v : ∣ Values A ∣) + {f g : Fin A → Fin B} + → f ≗ g + → push v f ≋ push v g + push-cong v f≋g i = merge-cong₂ v (≡.cong ⁅ i ⁆ ∘ f≋g) + +opaque + unfolding Values + removeAt : {n : ℕ} → ∣ Values (suc n) ∣ → Fin (suc n) → ∣ Values n ∣ + removeAt v i = Vec.removeAt v i + +opaque + unfolding merge removeAt + merge-removeAt + : {A : ℕ} + (k : Fin (suc A)) + (v : ∣ Values (suc A) ∣) + (S : Subset (suc A)) + → merge v S ≈ lookup v k when S k ∙ merge (removeAt v k) (Vec.removeAt S k) + merge-removeAt {A} zero v S = refl + merge-removeAt {suc A} (suc k) v S = begin + v0? ∙ merge (tail v) (Vec.tail S) ≈⟨ ∙-congˡ (merge-removeAt k (tail v) (Vec.tail S)) ⟩ + v0? ∙ (vk? ∙ merge (tail v-) (Vec.tail S-)) ≈⟨ assoc v0? vk? _ ⟨ + (v0? ∙ vk?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ ∙-congʳ (comm v0? vk?) ⟩ + (vk? ∙ v0?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ assoc vk? v0? _ ⟩ + vk? ∙ (v0? ∙ merge (tail v-) (Vec.tail S-)) ≡⟨⟩ + vk? ∙ merge v- S- ∎ + where + open ≈-Reasoning Valueₛ + v0? vk? : Value + v0? = head v when Vec.head S + vk? = tail v k when Vec.tail S k + v- : Vector Value (suc A) + v- = removeAt v (suc k) + S- : Subset (suc A) + S- = Vec.removeAt S (suc k) + +opaque + unfolding merge pull removeAt + merge-preimage-ρ + : {A B : ℕ} + → (ρ : Permutation A B) + → (v : ∣ Values A ∣) + (S : Subset B) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≈ merge (pull v (ρ ⟨$⟩ˡ_)) S + merge-preimage-ρ {zero} {zero} ρ v S = refl + merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero + merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero + merge-preimage-ρ {suc A} {suc B} ρ v S = begin + merge v (preimage ρʳ S) ≈⟨ merge-removeAt (ρˡ zero) v (preimage ρʳ S) ⟩ + mask (preimage ρʳ S) v (ρˡ zero) ∙ merge v- [preimage-ρʳ-S]- ≈⟨ ∙-congʳ ≈vρˡ0? ⟩ + mask S (pull v ρˡ) zero ∙ merge v- [preimage-ρʳ-S]- ≈⟨ ∙-congˡ (merge-cong₂ v- preimage-) ⟩ + mask S (pull v ρˡ) zero ∙ merge v- (preimage ρʳ- S-) ≈⟨ ∙-congˡ (merge-preimage-ρ ρ- v- S-) ⟩ + mask S (pull v ρˡ) zero ∙ merge (pull v- ρˡ-) S- ≈⟨ ∙-congˡ (merge-cong S- (reflexive ∘ pull-v-ρˡ-)) ⟩ + mask S (pull v ρˡ) zero ∙ merge (tail (pull v ρˡ)) S- ≡⟨⟩ + merge (pull v ρˡ) S ∎ + where + ρˡ : Fin (suc B) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation A B + ρ- = remove (ρˡ zero) ρ + ρˡ- : Fin B → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : ∣ Values A ∣ + v- = removeAt v (ρˡ zero) + S- : Subset B + S- = S ∘ suc + [preimage-ρʳ-S]- : Subset A + [preimage-ρʳ-S]- = Vec.removeAt (preimage ρʳ S) (ρˡ zero) + vρˡ0? : Value + vρˡ0? = head (pull v ρˡ) when S zero + ≈vρˡ0? : mask (S ∘ ρʳ ∘ ρˡ) (pull v ρˡ) zero ≈ mask S (pull v ρˡ) zero + ≈vρˡ0? = mask-cong₁ (λ i → ≡.cong S (inverseʳ ρ {i})) (pull v ρˡ) zero + module _ where + open ≡-Reasoning + preimage- : [preimage-ρʳ-S]- ≗ preimage ρʳ- S- + preimage- x = begin + [preimage-ρʳ-S]- x ≡⟨⟩ + Vec.removeAt (preimage ρʳ S) (ρˡ zero) x ≡⟨⟩ + S (ρʳ (punchIn (ρˡ zero) x)) ≡⟨ ≡.cong S (punchIn-permute ρ (ρˡ zero) x) ⟩ + S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x)) ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ + S (punchIn zero (ρʳ- x)) ≡⟨⟩ + S (suc (ρʳ- x)) ≡⟨⟩ + preimage ρʳ- S- x ∎ + pull-v-ρˡ- : pull v- ρˡ- ≗ tail (pull v ρˡ) + pull-v-ρˡ- i = begin + v- (ρˡ- i) ≡⟨⟩ + v (punchIn (ρˡ zero) (punchOut {A} {ρˡ zero} _)) ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩ + v (ρˡ (punchIn (ρʳ (ρˡ zero)) i)) ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h i))) (inverseʳ ρ) ⟩ + v (ρˡ (punchIn zero i)) ≡⟨⟩ + v (ρˡ (suc i)) ≡⟨⟩ + tail (v ∘ ρˡ) i ∎ + open ≈-Reasoning Valueₛ + +opaque + + unfolding push merge mask + + mutual + + merge-preimage + : {A B : ℕ} + (f : Fin A → Fin B) + → (v : ∣ Values A ∣) + (S : Subset B) + → merge v (preimage f S) ≈ merge (push v f) S + merge-preimage {zero} {zero} f v S = refl + merge-preimage {zero} {suc B} f v S = sym (trans (cong sumₛ (mask-<ε> S)) (sum-<ε> (suc B))) + merge-preimage {suc A} {zero} f v S with () ← f zero + merge-preimage {suc A} {suc B} f v S with insert-f0-0 f + ... | ρ , ρf0≡0 = begin + merge v (preimage f S) ≈⟨ merge-cong₂ v (preimage-cong₁ (λ x → inverseˡ ρ {f x}) S) ⟨ + merge v (preimage (ρˡ ∘ ρʳ ∘ f) S) ≡⟨⟩ + merge v (preimage (ρʳ ∘ f) (preimage ρˡ S)) ≈⟨ merge-preimage-f0≡0 (ρʳ ∘ f) ρf0≡0 v (preimage ρˡ S) ⟩ + merge (push v (ρʳ ∘ f)) (preimage ρˡ S) ≈⟨ merge-preimage-ρ (flip ρ) (push v (ρʳ ∘ f)) S ⟩ + merge (pull (push v (ρʳ ∘ f)) ρʳ) S ≈⟨ merge-cong S (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) ⟩ + merge (push v (ρˡ ∘ ρʳ ∘ f)) S ≈⟨ merge-cong S (push-cong v (λ x → inverseˡ ρ {f x})) ⟩ + merge (push v f) S ∎ + where + open ≈-Reasoning Valueₛ + ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρˡ = ρ ⟨$⟩ˡ_ + + merge-preimage-f0≡0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → f zero ≡ zero + → (v : ∣ Values (suc A) ∣) + (S : Subset (suc B)) + → merge v (preimage f S) ≈ merge (push v f) S + merge-preimage-f0≡0 {A} {B} f f0≡0 v S + using S0 , S- ← S zero , S ∘ suc + using v0 , v- ← head v , tail v + using f0 , f- ← f zero , f ∘ suc = begin + merge v f⁻¹[S] ≡⟨⟩ + v0? ∙ merge v- f⁻¹[S]- ≈⟨ ∙-congˡ (merge-preimage f- v- S) ⟩ + v0? ∙ merge f[v-] S ≡⟨⟩ + v0? ∙ (f[v-]0? ∙ merge f[v-]- S-) ≈⟨ assoc v0? f[v-]0? (merge f[v-]- S-) ⟨ + v0? ∙ f[v-]0? ∙ merge f[v-]- S- ≈⟨ ∙-congʳ v0?∙f[v-]0?≈f[v]0? ⟩ + f[v]0? ∙ merge f[v-]- S- ≈⟨ ∙-congˡ (merge-cong S- ≋f[v]-) ⟩ + f[v]0? ∙ merge f[v]- S- ≡⟨⟩ + merge f[v] S ∎ + where + open ≈-Reasoning Valueₛ + f⁻¹[S] : Subset (suc A) + f⁻¹[S] = preimage f S + f⁻¹[S]- : Subset A + f⁻¹[S]- = f⁻¹[S] ∘ suc + f⁻¹[S]0 : Bool + f⁻¹[S]0 = f⁻¹[S] zero + f[v] : ∣ Values (suc B) ∣ + f[v] = push v f + f[v]- : Vector Value B + f[v]- = tail f[v] + f[v]0 : Value + f[v]0 = head f[v] + f[v-] : ∣ Values (suc B) ∣ + f[v-] = push v- f- + f[v-]- : Vector Value B + f[v-]- = tail f[v-] + f[v-]0 : Value + f[v-]0 = head f[v-] + v0? f[v-]0? v0?+[f[v-]0?] f[v]0? : Value + v0? = v0 when f⁻¹[S]0 + f[v-]0? = f[v-]0 when S0 + v0?+[f[v-]0?] = if S0 then v0? ∙ f[v-]0 else v0? + f[v]0? = f[v]0 when S0 + v0?∙f[v-]0?≈f[v]0? : v0? ∙ f[v-]0? ≈ f[v]0? + v0?∙f[v-]0?≈f[v]0? rewrite f0≡0 with S0 + ... | true = refl + ... | false = identityˡ ε + ≋f[v]- : f[v-]- ≋ f[v]- + ≋f[v]- x rewrite f0≡0 = sym (identityˡ (push v- f- (suc x))) + +opaque + unfolding push + merge-push + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → (v : ∣ Values A ∣) + → push v (g ∘ f) ≋ push (push v f) g + merge-push f g v i = merge-preimage f v (preimage g ⁅ i ⁆) |