Add Push and Pull functors

3 files changed, 542 insertions, 0 deletions

diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda
new file mode 100644
index 0000000..d8180b4
--- /dev/null
+++ b/Data/Circuit/Merge.agda
@@ -0,0 +1,338 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Merge where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut)
+open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut)
+open import Data.Bool.Properties using (if-float)
+open import Data.Bool using (Bool; if_then_else_)
+open import Data.Circuit.Value using (Value; join; join-comm; join-assoc)
+open import Data.Subset.Functional
+  using
+      ( Subset
+      ; ⁅_⁆ ; ⊥ ; ⁅⁆∘ρ
+      ; foldl ; foldl-cong₁ ; foldl-cong₂
+      ; foldl-[] ; foldl-suc
+      ; foldl-⊥ ; foldl-⁅⁆
+      ; foldl-fusion
+      )
+open import Data.Vector as V using (Vector; head; tail; removeAt)
+open import Data.Fin.Permutation
+  using
+    ( Permutation′
+    ; _⟨$⟩ˡ_ ; _⟨$⟩ʳ_
+    ; inverseˡ ; inverseʳ
+    ; id
+    ; flip
+    ; insert ; remove
+    ; punchIn-permute
+    )
+open import Data.Product using (Σ-syntax; _,_)
+open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂)
+open import Function.Base using (∣_⟩-_; _∘_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+open Value using (U)
+open ℕ
+open Fin
+open Bool
+
+_when_ : Value → Bool → Value
+x when b = if b then x else U
+
+opaque
+  merge-with : {A : ℕ} → Value → Vector Value A → Subset A → Value
+  merge-with e v = foldl (∣ join ⟩- v) e
+
+  merge-with-cong : {A : ℕ} {v₁ v₂ : Vector Value A} (e : Value) → v₁ ≗ v₂ → merge-with e v₁ ≗ merge-with e v₂
+  merge-with-cong e v₁≗v₂ = foldl-cong₁ (λ x → ≡.cong (join x) ∘ v₁≗v₂) e
+
+  merge-with-cong₂ : {A : ℕ} (e : Value) (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge-with e v S₁ ≡ merge-with e v S₂
+  merge-with-cong₂ e v = foldl-cong₂ (∣ join ⟩- v) e
+
+  merge-with-⊥ : {A : ℕ} (e : Value) (v : Vector Value A) → merge-with e v ⊥ ≡ e
+  merge-with-⊥ e v = foldl-⊥ (∣ join ⟩- v) e
+
+  merge-with-[] : (e : Value) (v : Vector Value 0) (S : Subset 0) → merge-with e v S ≡ e
+  merge-with-[] e v = foldl-[] (∣ join ⟩- v) e
+
+  merge-with-suc
+      : {A : ℕ} (e : Value) (v : Vector Value (suc A)) (S : Subset (suc A))
+      → merge-with e v S
+      ≡ merge-with (if head S then join e (head v) else e) (tail v) (tail S)
+  merge-with-suc e v = foldl-suc (∣ join ⟩- v) e
+
+  merge-with-join
+      : {A : ℕ}
+        (x y : Value)
+        (v : Vector Value A)
+      → merge-with (join x y) v ≗ join x ∘ merge-with y v
+  merge-with-join {A} x y v S = ≡.sym (foldl-fusion (join x) fuse y S)
+    where
+      fuse : (acc : Value) (k : Fin A) → join x (join acc (v k)) ≡ join (join x acc) (v k)
+      fuse acc k = ≡.sym (join-assoc x acc (v k))
+
+  merge-with-⁅⁆ : {A : ℕ} (e : Value) (v : Vector Value A) (x : Fin A) → merge-with e v ⁅ x ⁆ ≡ join e (v x)
+  merge-with-⁅⁆ e v = foldl-⁅⁆ (∣ join ⟩- v) e
+
+merge-with-U : {A : ℕ} (e : Value) (S : Subset A) → merge-with e (λ _ → U) S ≡ e
+merge-with-U {zero} e S = merge-with-[] e (λ _ → U) S
+merge-with-U {suc A} e S = begin
+    merge-with e (λ _ → U) S                ≡⟨ merge-with-suc e (λ _ → U) S ⟩
+    merge-with
+        (if head S then join e U else e)
+        (tail (λ _ → U)) (tail S)           ≡⟨ ≡.cong (λ h → merge-with (if head S then h else e) _ _) (join-comm e U) ⟩
+    merge-with
+        (if head S then e else e)
+        (tail (λ _ → U)) (tail S)           ≡⟨ ≡.cong (λ h → merge-with h (λ _ → U) (tail S)) (either-way (head S)) ⟨
+    merge-with e (tail (λ _ → U)) (tail S)  ≡⟨⟩
+    merge-with e (λ _ → U) (tail S)         ≡⟨ merge-with-U e (tail S) ⟩
+    e                                       ∎
+  where
+    open ≡.≡-Reasoning
+    either-way : (b : Bool) → e ≡ (if b then e else e)
+    either-way b = if-float (λ _ → e) b {e} {e}
+
+merge : {A : ℕ} → Vector Value A → Subset A → Value
+merge v = merge-with U v
+
+merge-cong₁ : {A : ℕ} {v₁ v₂ : Vector Value A} → v₁ ≗ v₂ → merge v₁ ≗ merge v₂
+merge-cong₁ = merge-with-cong U
+
+merge-cong₂ : {A : ℕ} (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge v S₁ ≡ merge v S₂
+merge-cong₂ = merge-with-cong₂ U
+
+merge-⊥ : {A : ℕ} (v : Vector Value A) → merge-with U v ⊥ ≡ U
+merge-⊥ = merge-with-⊥ U
+
+merge-[] : (v : Vector Value 0) (S : Subset 0) → merge v S ≡ U
+merge-[] = merge-with-[] U
+
+merge-[]₂ : {v₁ v₂ : Vector Value 0} {S₁ S₂ : Subset 0} → merge v₁ S₁ ≡ merge v₂ S₂
+merge-[]₂ {v₁} {v₂} {S₁} {S₂} = ≡.trans (merge-[] v₁ S₁) (≡.sym (merge-[] v₂ S₂))
+
+merge-⁅⁆ : {A : ℕ} (v : Vector Value A) (x : Fin A) → merge v ⁅ x ⁆ ≡ v x
+merge-⁅⁆ = merge-with-⁅⁆ U
+
+join-merge : {A : ℕ} (e : Value) (v : Vector Value A) (S : Subset A) → join e (merge v S) ≡ merge-with e v S
+join-merge e v S = ≡.sym (≡.trans (≡.cong (λ h → merge-with h v S) (join-comm U e)) (merge-with-join e U v S))
+
+merge-suc
+    : {A : ℕ} (v : Vector Value (suc A)) (S : Subset (suc A))
+    → merge v S
+    ≡ merge-with (head v when head S) (tail v) (tail S)
+merge-suc = merge-with-suc U
+
+insert-f0-0
+    : {A B : ℕ}
+      (f : Fin (suc A) → Fin (suc B))
+    → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero)
+insert-f0-0 f = insert (f zero) zero id , help
+  where
+    open import Data.Fin using (_≟_)
+    open import Relation.Nullary.Decidable using (yes; no)
+    help : insert (f zero) zero id ⟨$⟩ʳ f zero ≡ zero
+    help with f zero ≟ f zero
+    ... | yes _ = ≡.refl
+    ... | no f0≢f0 with () ← f0≢f0 ≡.refl
+
+merge-removeAt
+    : {A : ℕ}
+      (k : Fin (suc A))
+      (v : Vector Value (suc A))
+      (S : Subset (suc A))
+    → merge v S ≡ join (v k when S k) (merge (removeAt v k) (removeAt S k))
+merge-removeAt {A} zero v S = begin
+    merge-with U v S                                            ≡⟨ merge-suc v S ⟩
+    merge-with (head v when head S) (tail v) (tail S)           ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨
+    join (head v when head S) (merge-with U (tail v) (tail S))  ∎
+  where
+    open ≡.≡-Reasoning
+merge-removeAt {suc A} (suc k) v S = begin
+    merge-with U v S                                  ≡⟨ merge-suc v S ⟩
+    merge-with v0? (tail v) (tail S)                  ≡⟨ join-merge _ (tail v) (tail S) ⟨
+    join v0? (merge (tail v) (tail S))                ≡⟨ ≡.cong (join v0?) (merge-removeAt k (tail v) (tail S)) ⟩
+    join v0? (join vk? (merge (tail v-) (tail S-)))   ≡⟨ join-assoc (head v when head S) _ _ ⟨
+    join (join v0? vk?) (merge (tail v-) (tail S-))   ≡⟨ ≡.cong (λ h → join h (merge (tail v-) (tail S-))) (join-comm (head v- when head S-) _) ⟩
+    join (join vk? v0?) (merge (tail v-) (tail S-))   ≡⟨ join-assoc (tail v k when tail S k) _ _ ⟩
+    join vk? (join v0? (merge (tail v-) (tail S-)))   ≡⟨ ≡.cong (join vk?) (join-merge _ (tail v-) (tail S-)) ⟩
+    join vk? (merge-with v0? (tail v-) (tail S-))     ≡⟨ ≡.cong (join vk?) (merge-suc v- S-) ⟨
+    join vk? (merge v- S-)                            ∎
+  where
+    v0? vk? : Value
+    v0? = head v when head S
+    vk? = tail v k when tail S k
+    v- : Vector Value (suc A)
+    v- = removeAt v (suc k)
+    S- : Subset (suc A)
+    S- = removeAt S (suc k)
+    open ≡.≡-Reasoning
+
+import Function.Structures as FunctionStructures
+open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse)
+open IsInverse using () renaming (inverseˡ to invˡ; inverseʳ to invʳ)
+
+merge-preimage-ρ
+    : {A : ℕ}
+    → (ρ : Permutation′ A)
+    → (v : Vector Value A)
+      (S : Subset A)
+    → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S
+merge-preimage-ρ {zero} ρ v S = merge-[]₂
+merge-preimage-ρ {suc A} ρ v S = begin
+    merge v (preimage ρʳ S)                   ≡⟨ merge-removeAt (head ρˡ) v (preimage ρʳ S) ⟩
+    join
+        (head (v ∘ ρˡ) when S (ρʳ (ρˡ zero)))
+        (merge v- [preimageρʳS]-)             ≡⟨ ≡.cong (λ h → join h (merge v- [preimageρʳS]-)) ≡vρˡ0? ⟩
+    join vρˡ0? (merge v- [preimageρʳS]-)      ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₂ v- preimage-) ⟩
+    join vρˡ0? (merge v- (preimage ρʳ- S-))   ≡⟨ ≡.cong (join vρˡ0?) (merge-preimage-ρ ρ- v- S-) ⟩
+    join vρˡ0? (merge (v- ∘ ρˡ-) S-)          ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₁ v∘ρˡ- S-) ⟩
+    join vρˡ0? (merge (tail (v ∘ ρˡ)) S-)     ≡⟨ join-merge vρˡ0? (tail (v ∘ ρˡ)) S- ⟩
+    merge-with vρˡ0? (tail (v ∘ ρˡ)) S-       ≡⟨ merge-suc (v ∘ ρˡ) S ⟨
+    merge (v ∘ ρˡ) S                          ∎
+  where
+    ρˡ ρʳ : Fin (suc A) → Fin (suc A)
+    ρˡ = ρ ⟨$⟩ˡ_
+    ρʳ = ρ ⟨$⟩ʳ_
+    ρ- : Permutation′ A
+    ρ- = remove (head ρˡ) ρ
+    ρˡ- ρʳ- : Fin A → Fin A
+    ρˡ- = ρ- ⟨$⟩ˡ_
+    ρʳ- = ρ- ⟨$⟩ʳ_
+    v- : Vector Value A
+    v- = removeAt v (head ρˡ)
+    [preimageρʳS]- : Subset A
+    [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ)
+    S- : Subset A
+    S- = tail S
+    vρˡ0? : Value
+    vρˡ0? = head (v ∘ ρˡ) when head S
+    open ≡.≡-Reasoning
+    ≡vρˡ0?  : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S
+    ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ)
+    v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ)
+    v∘ρˡ- x = begin
+        v- (ρˡ- x)                                        ≡⟨⟩
+        v (punchIn (head ρˡ) (punchOut {A} {head ρˡ} _))  ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩
+        v (ρˡ (punchIn (ρʳ (ρˡ zero)) x))                 ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h x))) (inverseʳ ρ) ⟩
+        v (ρˡ (punchIn zero x))                           ≡⟨⟩
+        v (ρˡ (suc x))                                    ≡⟨⟩
+        tail (v ∘ ρˡ) x                                   ∎
+    preimage- : [preimageρʳS]- ≗ preimage ρʳ- S-
+    preimage- x = begin
+        [preimageρʳS]- x                      ≡⟨⟩
+        removeAt (preimage ρʳ S) (head ρˡ) x  ≡⟨⟩
+        S (ρʳ (punchIn (head ρˡ) x))          ≡⟨ ≡.cong S (punchIn-permute ρ (head ρˡ) x) ⟩ 
+        S (punchIn (ρʳ (head ρˡ)) (ρʳ- x))    ≡⟨⟩
+        S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x))    ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ 
+        S (punchIn zero (ρʳ- x))              ≡⟨⟩ 
+        S (suc (ρʳ- x))                       ≡⟨⟩
+        preimage ρʳ- S- x                     ∎
+
+push-with : {A B : ℕ} → (e : Value) → Vector Value A → (Fin A → Fin B) → Vector Value B
+push-with e v f = merge-with e v ∘ preimage f ∘ ⁅_⁆
+
+push : {A B : ℕ} → Vector Value A → (Fin A → Fin B) → Vector Value B
+push = push-with U
+
+mutual
+  merge-preimage
+      : {A B : ℕ}
+        (f : Fin A → Fin B)
+      → (v : Vector Value A)
+        (S : Subset B)
+      → merge v (preimage f S) ≡ merge (push v f) S
+  merge-preimage {zero} {zero} f v S = merge-[]₂
+  merge-preimage {zero} {suc B} f v S = begin
+      merge v (preimage f S)  ≡⟨ merge-[] v (preimage f S) ⟩
+      U                       ≡⟨ merge-with-U U S ⟨
+      merge (λ _ → U) S       ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩
+      merge (push v f) S      ∎
+    where
+      open ≡.≡-Reasoning
+  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 (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) (preimage ρˡ S) ≡⟨ merge-preimage-ρ (flip ρ) (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) S ⟩
+          merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆ ∘ ρʳ) S          ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) S ⟩
+          merge (merge v ∘ preimage (ρʳ ∘ f) ∘ preimage ρˡ ∘ ⁅_⁆) S ≡⟨⟩
+          merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S          ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩
+          merge (merge v ∘ preimage f ∘ ⁅_⁆) S                      ∎
+        where
+          open ≡.≡-Reasoning
+          ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B)
+          ρʳ = ρ ⟨$⟩ʳ_
+          ρˡ = ρ ⟨$⟩ˡ_
+
+  merge-preimage-f0≡0
+      : {A B : ℕ}
+        (f : Fin (ℕ.suc A) → Fin (ℕ.suc B))
+      → f Fin.zero ≡ Fin.zero
+      → (v : Vector Value (ℕ.suc A))
+        (S : Subset (ℕ.suc B))
+      → merge v (preimage f S) ≡ merge (merge v ∘ preimage f ∘ ⁅_⁆) S
+  merge-preimage-f0≡0 {A} {B} f f0≡0 v S
+    using S0 , S- ← head S , tail S
+    using v0 , v- ← head v , tail v
+    using _  , f- ← head f , tail f
+      = begin
+            merge v f⁻¹[S]                      ≡⟨ merge-suc v f⁻¹[S] ⟩
+            merge-with v0? v- f⁻¹[S]-           ≡⟨ join-merge v0? v- f⁻¹[S]- ⟨
+            join v0? (merge v- f⁻¹[S]-)         ≡⟨ ≡.cong (join v0?) (merge-preimage f- v- S) ⟩
+            join v0? (merge f[v-] S)            ≡⟨ join-merge v0? f[v-] S ⟩
+            merge-with v0? f[v-] S              ≡⟨ merge-with-suc v0? f[v-] S ⟩
+            merge-with v0?+[f[v-]0?] f[v-]- S-  ≡⟨ ≡.cong (λ h → merge-with h f[v-]- S-) ≡f[v]0 ⟩
+            merge-with f[v]0? f[v-]- S-         ≡⟨ merge-with-cong f[v]0? ≡f[v]- S- ⟩
+            merge-with f[v]0? f[v]- S-          ≡⟨ merge-suc f[v] S ⟨
+            merge f[v] S                        ∎
+          where
+            f⁻¹[S] : Subset (suc A)
+            f⁻¹[S] = preimage f S
+            f⁻¹[S]- : Subset A
+            f⁻¹[S]- = tail f⁻¹[S]
+            f⁻¹[S]0 : Bool
+            f⁻¹[S]0 = head f⁻¹[S]
+            f[v] : Vector Value (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-] : Vector Value (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⁻¹⁅0⁆ : Subset (suc A)
+            f⁻¹⁅0⁆ = preimage f ⁅ zero ⁆
+            f⁻¹⁅0⁆- : Subset A
+            f⁻¹⁅0⁆- = tail f⁻¹⁅0⁆
+            v0? v0?+[f[v-]0?] f[v]0? : Value
+            v0? = v0 when f⁻¹[S]0
+            v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?)
+            f[v]0? = f[v]0 when S0
+            open ≡.≡-Reasoning
+            ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0?
+            ≡f[v]0 rewrite f0≡0 with S0
+            ... | true = begin
+                      join v0 (merge v- f⁻¹⁅0⁆-)  ≡⟨ join-merge v0 v- (tail (preimage f ⁅ zero ⁆)) ⟩
+                      merge-with v0 v- f⁻¹⁅0⁆-    ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ zero ⁆ h) v- f⁻¹⁅0⁆-) f0≡0 ⟨
+                      merge-with v0?′ v- f⁻¹⁅0⁆-  ≡⟨ merge-suc v (preimage f ⁅ zero ⁆) ⟨
+                      merge v f⁻¹⁅0⁆              ∎
+                    where
+                      v0?′ : Value
+                      v0?′ = v0 when head f⁻¹⁅0⁆
+            ... | false = ≡.refl
+            ≡f[v]- : f[v-]- ≗ f[v]-
+            ≡f[v]- x = begin
+                push v- f- (suc x)            ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ suc x ⁆ h) v- (preimage f- ⁅ suc x ⁆)) f0≡0 ⟨
+                push-with v0?′ v- f- (suc x)  ≡⟨ merge-suc v (preimage f ⁅ suc x ⁆) ⟨
+                push v f (suc x)              ∎
+              where
+                v0?′ : Value
+                v0?′ = v0 when head (preimage f ⁅ suc x ⁆)
diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda
new file mode 100644
index 0000000..f6e4373
--- /dev/null
+++ b/Data/Fin/Preimage.agda
@@ -0,0 +1,42 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Preimage where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin.Base using (Fin)
+open import Function.Base using (∣_⟩-_; _∘_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
+open import Data.Subset.Functional using (Subset; foldl; _∪_; ⊥; ⁅_⁆)
+
+private
+  variable A B C : ℕ
+
+preimage : (Fin A → Fin B) → Subset B → Subset A
+preimage f Y = Y ∘ f
+
+⋃ : Subset A → (Fin A → Subset B) → Subset B
+⋃ S f = foldl (∣ _∪_ ⟩- f) ⊥ S
+
+image : (Fin A → Fin B) → Subset A → Subset B
+image f X = ⋃ X (⁅_⁆ ∘ f)
+
+preimage-cong₁
+    : {f g : Fin A → Fin B}
+    → f ≗ g
+    → (S : Subset B)
+    → preimage f S ≗ preimage g S
+preimage-cong₁ f≗g S x = ≡.cong S (f≗g x)
+
+preimage-cong₂
+    : (f : Fin A → Fin B)
+      {S₁ S₂ : Subset B}
+    → S₁ ≗ S₂
+    → preimage f S₁ ≗ preimage f S₂
+preimage-cong₂ f S₁≗S₂ = S₁≗S₂ ∘ f
+
+preimage-∘
+    : (f : Fin A → Fin B)
+      (g : Fin B → Fin C)
+      (z : Fin C)
+    → preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆)
+preimage-∘ f g S x = ≡.refl
diff --git a/Data/Subset/Functional.agda b/Data/Subset/Functional.agda
new file mode 100644
index 0000000..33a6d8e
--- /dev/null
+++ b/Data/Subset/Functional.agda
@@ -0,0 +1,162 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Subset.Functional where
+
+open import Data.Bool.Base using (Bool; _∨_; _∧_; if_then_else_)
+open import Data.Bool.Properties using (if-float)
+open import Data.Fin.Base using (Fin)
+open import Data.Fin.Permutation using (Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; inverseˡ; inverseʳ)
+open import Data.Fin.Properties using (suc-injective; 0≢1+n)
+open import Data.Nat.Base using (ℕ)
+open import Function.Base using (∣_⟩-_; _∘_)
+open import Function.Definitions using (Injective)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; _≢_)
+open import Data.Vector as V using (Vector; head; tail)
+
+open Bool
+open Fin
+open ℕ
+
+Subset : ℕ → Set
+Subset = Vector Bool
+
+private
+  variable n A : ℕ
+  variable B C : Set
+
+⊥ : Subset n
+⊥ _ = false
+
+_∪_ : Subset n → Subset n → Subset n
+(A ∪ B) k = A k ∨ B k
+
+_∩_ : Subset n → Subset n → Subset n
+(A ∩ B) k = A k ∧ B k
+
+⁅_⁆ : Fin n → Subset n
+⁅_⁆ zero zero = true
+⁅_⁆ zero (suc _) = false
+⁅_⁆ (suc k) zero = false
+⁅_⁆ (suc k) (suc i) = ⁅ k ⁆ i
+
+⁅⁆-refl : (k : Fin n) → ⁅ k ⁆ k ≡ true
+⁅⁆-refl zero = ≡.refl
+⁅⁆-refl (suc k) = ⁅⁆-refl k
+
+⁅x⁆y≡true
+    : (x y : Fin n)
+    → .(⁅ x ⁆ y ≡ true)
+    → x ≡ y
+⁅x⁆y≡true zero zero prf = ≡.refl
+⁅x⁆y≡true (suc x) (suc y) prf = ≡.cong suc (⁅x⁆y≡true x y prf)
+
+⁅x⁆y≡false
+    : (x y : Fin n)
+    → .(⁅ x ⁆ y ≡ false)
+    → x ≢ y
+⁅x⁆y≡false zero (suc y) prf = 0≢1+n
+⁅x⁆y≡false (suc x) zero prf = 0≢1+n ∘ ≡.sym
+⁅x⁆y≡false (suc x) (suc y) prf = ⁅x⁆y≡false x y prf ∘ suc-injective
+
+f-⁅⁆
+    : {n m : ℕ}
+      (f : Fin n → Fin m)
+    → Injective _≡_ _≡_ f
+    → (x y : Fin n)
+    → ⁅ x ⁆ y ≡ ⁅ f x ⁆ (f y)
+f-⁅⁆ f f-inj zero zero = ≡.sym (⁅⁆-refl (f zero))
+f-⁅⁆ f f-inj zero (suc y) with ⁅ f zero ⁆ (f (suc y)) in eq
+... | true with () ← f-inj (⁅x⁆y≡true (f zero) (f (suc y)) eq)
+... | false = ≡.refl
+f-⁅⁆ f f-inj (suc x) zero with ⁅ f (suc x) ⁆ (f zero) in eq
+... | true with () ← f-inj (⁅x⁆y≡true (f (suc x)) (f zero) eq)
+... | false = ≡.refl
+f-⁅⁆ f f-inj (suc x) (suc y) = f-⁅⁆ (f ∘ suc) (suc-injective ∘ f-inj) x y
+
+⁅⁆∘ρ
+    : (ρ : Permutation′ (suc n))
+      (x : Fin (suc n))
+    → ⁅ ρ ⟨$⟩ʳ x ⁆ ≗ ⁅ x ⁆ ∘ (ρ ⟨$⟩ˡ_)
+⁅⁆∘ρ {n} ρ x y = begin
+    ⁅ ρ ⟨$⟩ʳ x ⁆ y                    ≡⟨ f-⁅⁆ (ρ ⟨$⟩ˡ_) ρˡ-inj (ρ ⟨$⟩ʳ x) y ⟩
+    ⁅ ρ ⟨$⟩ˡ (ρ ⟨$⟩ʳ x) ⁆ (ρ ⟨$⟩ˡ y)  ≡⟨ ≡.cong (λ h → ⁅ h ⁆ (ρ ⟨$⟩ˡ y)) (inverseˡ ρ) ⟩
+    ⁅ x ⁆ (ρ ⟨$⟩ˡ y)                  ∎
+  where
+    open ≡.≡-Reasoning
+    ρˡ-inj : {x y : Fin (suc n)} → ρ ⟨$⟩ˡ x ≡ ρ ⟨$⟩ˡ y → x ≡ y
+    ρˡ-inj {x} {y} ρˡx≡ρˡy = begin
+        x                 ≡⟨ inverseʳ ρ ⟨
+        ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ x) ≡⟨ ≡.cong (ρ ⟨$⟩ʳ_) ρˡx≡ρˡy ⟩
+        ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ y) ≡⟨ inverseʳ ρ ⟩
+        y                 ∎
+
+opaque
+  -- TODO dependent fold
+  foldl : (B → Fin A → B) → B → Subset A → B
+  foldl {B = B} f = V.foldl (λ _ → B) (λ { {k} acc b → if b then f acc k else acc })
+
+  foldl-cong₁
+      : {f g : B → Fin A → B}
+      → (∀ x y → f x y ≡ g x y)
+      → (e : B)
+      → (S : Subset A)
+      → foldl f e S ≡ foldl g e S
+  foldl-cong₁ {B = B} f≗g e S = V.foldl-cong (λ _ → B) (λ { {k} x y → ≡.cong (if y then_else x) (f≗g x k) }) e S
+
+  foldl-cong₂
+      : (f : B → Fin A → B)
+        (e : B)
+        {S₁ S₂ : Subset A}
+      → (S₁ ≗ S₂)
+      → foldl f e S₁ ≡ foldl f e S₂
+  foldl-cong₂ {B = B} f e S₁≗S₂ = V.foldl-cong-arg (λ _ → B) (λ {n} acc b → if b then f acc n else acc) e S₁≗S₂
+
+  foldl-suc
+      : (f : B → Fin (suc A) → B)
+      → (e : B)
+      → (S : Subset (suc A))
+      → foldl f e S ≡ foldl (∣ f ⟩- suc) (if head S then f e zero else e) (tail S)
+  foldl-suc f e S = ≡.refl
+
+  foldl-⊥
+      : {A : ℕ}
+        {B : Set}
+        (f : B → Fin A → B)
+        (e : B)
+      → foldl f e ⊥ ≡ e
+  foldl-⊥ {zero} _ _ = ≡.refl
+  foldl-⊥ {suc A} f e = foldl-⊥ (∣ f ⟩- suc) e
+
+  foldl-⁅⁆
+      : (f : B → Fin A → B)
+        (e : B)
+        (k : Fin A)
+      → foldl f e ⁅ k ⁆ ≡ f e k
+  foldl-⁅⁆ f e zero = foldl-⊥ f (f e zero)
+  foldl-⁅⁆ f e (suc k) = foldl-⁅⁆ (∣ f ⟩- suc) e k
+
+  foldl-fusion
+      : (h : C → B)
+        {f : C → Fin A → C}
+        {g : B → Fin A → B}
+      → (∀ x n → h (f x n) ≡ g (h x) n)
+      → (e : C)
+      → h ∘ foldl f e ≗ foldl g (h e)
+  foldl-fusion {C = C} {A = A} h {f} {g} fuse e = V.foldl-fusion h ≡.refl fuse′
+    where
+      open ≡.≡-Reasoning
+      fuse′
+          : {k : Fin A}
+            (acc : C)
+            (b : Bool)
+          → h (if b then f acc k else acc) ≡ (if b then g (h acc) k else h acc)
+      fuse′ {k} acc b = begin
+          h (if b then f acc k else acc)      ≡⟨ if-float h b ⟩
+          (if b then h (f acc k) else h acc)  ≡⟨ ≡.cong (if b then_else h acc) (fuse acc k) ⟩
+          (if b then g (h acc) k else h acc)  ∎
+
+Subset0≗⊥ : (S : Subset 0) → S ≗ ⊥
+Subset0≗⊥ S ()
+
+foldl-[] : (f : B → Fin 0 → B) (e : B) (S : Subset 0) → foldl f e S ≡ e
+foldl-[] f e S = ≡.trans (foldl-cong₂ f e (Subset0≗⊥ S)) (foldl-⊥ f e)