From 7071bd597991db76d3b0d923b83f1d0c3f116bee Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 15 Feb 2024 21:26:39 +0100
Subject: [PATCH] EqIndexedSet

---
 src/Construct/Artifact.agda                   | 12 +--
 src/Construct/Choices.agda                    | 19 ++---
 src/Data/EqIndexedSet.agda                    |  4 +
 src/Framework/Compiler.agda                   | 16 ++--
 src/Framework/Proof/Transitive.lagda.md       |  8 +-
 .../Properties/Completeness.lagda.md          |  6 +-
 src/Framework/Properties/Finity.agda          |  3 +-
 src/Framework/Properties/Soundness.lagda.md   |  6 +-
 src/Framework/Relation/Expression.lagda.md    |  3 +-
 .../Relation/Expressiveness.lagda.md          |  1 -
 .../{Variant.agda => VariantMap.agda}         | 14 +---
 src/Framework/Variants.agda                   |  8 +-
 src/Lang/CCC.lagda.md                         |  8 +-
 src/Lang/VariantList.lagda.md                 | 74 ++++++++-----------
 .../Construct/2Choice-to-NChoice-VL.agda      |  6 +-
 .../Lang/VariantList-to-CCC.lagda.md          | 21 +++---
 16 files changed, 90 insertions(+), 119 deletions(-)
 create mode 100644 src/Data/EqIndexedSet.agda
 rename src/Framework/{Variant.agda => VariantMap.agda} (71%)

diff --git a/src/Construct/Artifact.agda b/src/Construct/Artifact.agda
index 92d210dc..3d6d0c44 100644
--- a/src/Construct/Artifact.agda
+++ b/src/Construct/Artifact.agda
@@ -7,7 +7,6 @@ open import Level using (_⊔_)
 open import Function using (id; flip; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage
 open import Framework.Construct
@@ -23,9 +22,9 @@ Syntax E A = Artifact A (E A)
 Construct : PlainConstruct
 Construct = Plain-⟪ Syntax , (λ Γ e c → map-children (flip (Semantics Γ) c) e) ⟫
 
+open import Data.EqIndexedSet as ISet
 map-children-preserves : ∀ {V : 𝕍} {Γ₁ Γ₂ : VariabilityLanguage V} {A}
-  → let open IVSet V A using (_≅_; _≅[_][_]_) in
-  ∀ (mkArtifact : Syntax ∈ₛ V)
+  → (mkArtifact : Syntax ∈ₛ V)
   → (t : LanguageCompiler Γ₁ Γ₂)
   → (a : Syntax (Expression Γ₁) A)
   → PlainConstruct-Semantics Construct mkArtifact Γ₁ a
@@ -37,9 +36,10 @@ map-children-preserves {V} {Γ₁} {Γ₂} {A} mkArtifact t (a -< cs >-) =
     ≅[]⟨ t-⊆ , t-⊇ ⟩
       (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₂ c) (map (compile t) cs) >-))
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where
+      -- module I = IVSet V A
+          -- open I using (_≅[_][_]_; _⊆[_]_)
+          open ISet.≅[]-Reasoning
           open Eq.≡-Reasoning
 
           ⟦_⟧₁ = Semantics Γ₁
diff --git a/src/Construct/Choices.agda b/src/Construct/Choices.agda
index 3b0f5c24..1055d131 100644
--- a/src/Construct/Choices.agda
+++ b/src/Construct/Choices.agda
@@ -9,6 +9,8 @@ open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 
+open import Data.EqIndexedSet as ISet
+
 open import Util.AuxProofs using (if-cong)
 
 module Choice-Fix where
@@ -160,7 +162,6 @@ module Choiceₙ where
   show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-list⁺ show-a es))) <+> "⟩"
 
 -- Show how choices can be used as constructors in variability languages.
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage as VL hiding (Config; Semantics)
 open import Framework.Relation.Function using (to-is-Embedding)
@@ -184,8 +185,8 @@ module VLChoice₂ where
   Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V
   Construct V F = Variational-⟪ Syntax F , Config F , Semantics V F ⟫
 
-  map-compile-preserves : ∀ {F V A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+  map-compile-preserves : ∀ {F V A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible (Construct V F) Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (chc : Syntax F (Expression Γ₁) A)
@@ -210,9 +211,7 @@ module VLChoice₂ where
     ≅[]⟨⟩
       Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc)
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where open ISet.≅[]-Reasoning
 
           ⟦_⟧₁ = VL.Semantics Γ₁
           ⟦_⟧₂ = VL.Semantics Γ₂
@@ -271,8 +270,8 @@ module VLChoiceₙ where
   -- This proof is oblivious of at least
   --   - the implementation of map, we only need the preservation theorem
   --   - the Standard-Semantics, we only need the preservation theorem of t, and that the config-compiler is stable.
-  map-compile-preserves : ∀ {F V A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+  map-compile-preserves : ∀ {F V A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible (Construct V F) Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (chc : Syntax F (Expression Γ₁) A)
@@ -297,9 +296,7 @@ module VLChoiceₙ where
     ≅[]⟨⟩
       Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc)
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where open ISet.≅[]-Reasoning
 
           ⟦_⟧₁ = VL.Semantics Γ₁
           ⟦_⟧₂ = VL.Semantics Γ₂
diff --git a/src/Data/EqIndexedSet.agda b/src/Data/EqIndexedSet.agda
new file mode 100644
index 00000000..9ea8768d
--- /dev/null
+++ b/src/Data/EqIndexedSet.agda
@@ -0,0 +1,4 @@
+module Data.EqIndexedSet {A : Set} where
+
+import Relation.Binary.PropositionalEquality as Eq
+open import Data.IndexedSet (Eq.setoid A) as ISet public
diff --git a/src/Framework/Compiler.agda b/src/Framework/Compiler.agda
index d043eebd..35ea7353 100644
--- a/src/Framework/Compiler.agda
+++ b/src/Framework/Compiler.agda
@@ -1,6 +1,5 @@
 module Framework.Compiler where
 
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage
 open import Framework.Construct
@@ -10,6 +9,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≗_)
 open import Data.Product using (_×_)
 open import Function using (id; _∘_)
 
+open import Data.EqIndexedSet using (_≅_; _≅[_][_]_; ≅[]-trans)
+
 {-|
 A translated configuration is extensionally equal.
 Fixme: Give me a proper name not this ugly one.
@@ -24,8 +25,8 @@ record LanguageCompiler {V} (Γ₁ Γ₂ : VariabilityLanguage V) : Set₁ where
   field
     compile         : ∀ {A} → L₁ A → L₂ A
     config-compiler : Config Γ₁ ⇔ Config Γ₂
-    preserves : ∀ {A} → let open IVSet V A using (_≅[_][_]_) in
-                ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂
+    preserves : ∀ {A} (e : L₁ A)
+      → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂
                 -- TODO: It might nice to have syntax
                 --   ≅[ config-compiler ]
                 -- to abbreviate
@@ -46,8 +47,7 @@ record ConstructCompiler {V} (VC₁ VC₂ : VariabilityConstruct V) (Γ : Variab
 
     stable : to-is-Embedding config-compiler
     preserves : ∀ {A} (c : C₁ (Expression Γ) A)
-      → let open IVSet V A using (_≅_) in
-        Kem₁ Γ extract c ≅ Kem₂ Γ (to config-compiler ∘ extract) (compile c)
+      → Kem₁ Γ extract c ≅ Kem₂ Γ (to config-compiler ∘ extract) (compile c)
 
 {-|
 Compiles languages below constructs.
@@ -64,8 +64,8 @@ record ConstructFunctor {V} (VC : VariabilityConstruct V) : Set₁ where
     -- Note: There also should be an extract₂ but it must be
     -- equivalent to extract₁ ∘ fnoc t.
     -- extract₂ : Config Γ₂ → construct-config
-    preserves : ∀ {A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+    preserves : ∀ {A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible VC Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (c : VSyntax VC (Expression Γ₁) A)
@@ -128,8 +128,6 @@ _⊕ˡ_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record
         fnoc' = fnoc L₁→L₂ ∘ fnoc L₂→L₃
 
         module _ {A : 𝔸} where
-          open IVSet V A using (_≅[_][_]_; ≅[]-trans)
-
           -- this pattern is very similar of ⊆[]-trans
           p : ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' ][ fnoc' ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃
           p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e))
diff --git a/src/Framework/Proof/Transitive.lagda.md b/src/Framework/Proof/Transitive.lagda.md
index bff095f3..ce9e7ecf 100644
--- a/src/Framework/Proof/Transitive.lagda.md
+++ b/src/Framework/Proof/Transitive.lagda.md
@@ -9,7 +9,7 @@ open import Framework.VariabilityLanguage using (VariabilityLanguage)
 open import Framework.Properties.Completeness V
 open import Framework.Properties.Soundness V
 open import Framework.Relation.Expressiveness V
-open import Framework.Variant V
+open import Data.EqIndexedSet
 ```
 
 ## Conclusions
@@ -34,8 +34,6 @@ completeness-by-expressiveness : ∀ {L₁ L₂ : VariabilityLanguage V}
 completeness-by-expressiveness encode-in-L₂ L₂-to-L₁ {A} vs with encode-in-L₂ vs
 ... | e₂ , m≅e₂ with L₂-to-L₁ e₂
 ...   | e₁ , e₂≅e₁ = e₁ , ≅-trans m≅e₂ e₂≅e₁
-  where
-    open IVSet A using (≅-sym; ≅-trans)
 ```
 
 If a language `L₁` is sound and at least as expressive as another language `L₂`, then also `L₂` is sound.
@@ -50,8 +48,6 @@ soundness-by-expressiveness : ∀ {L₁ L₂ : VariabilityLanguage V}
 soundness-by-expressiveness L₁-sound L₂-to-L₁ {A} e₂ with L₂-to-L₁ e₂
 ... | e₁ , e₂≅e₁ with L₁-sound e₁
 ...   | n , m , m≅e₁ = n , m , ≅-trans m≅e₁ (≅-sym e₂≅e₁)
-  where
-    open IVSet A using (≅-trans; ≅-sym)
 ```
 
 Conversely, we can conclude that any complete language is at least as expressive as any other variability language.
@@ -70,8 +66,6 @@ expressiveness-by-completeness-and-soundness : ∀ {Lᶜ Lˢ : VariabilityLangua
 expressiveness-by-completeness-and-soundness comp sound {A} eˢ with sound eˢ
 ... | p , m , m≅⟦eˢ⟧ with comp m
 ...   | eᶜ , m≅⟦eᶜ⟧ = eᶜ , ≅-trans (≅-sym m≅⟦eˢ⟧) m≅⟦eᶜ⟧
-  where
-    open IVSet A using (≅-sym; ≅-trans)
 ```
 
 If a language `L₊` is complete and another language `L₋` is incomplete then `L₋` less expressive than `L₊`.
diff --git a/src/Framework/Properties/Completeness.lagda.md b/src/Framework/Properties/Completeness.lagda.md
index b459583e..70a671fc 100644
--- a/src/Framework/Properties/Completeness.lagda.md
+++ b/src/Framework/Properties/Completeness.lagda.md
@@ -13,7 +13,8 @@ module Framework.Properties.Completeness (V : 𝕍) where
 open import Data.Product using (Σ-syntax)
 open import Relation.Nullary.Negation using (¬_)
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
+open import Framework.VariantMap V
+open import Data.EqIndexedSet
 ```
 
 ## Definitions
@@ -28,8 +29,7 @@ via Fin (suc n) here for convenience.
 -}
 Complete : VariabilityLanguage V → Set₁
 Complete ⟪ E , _ , ⟦_⟧ ⟫ =
-  ∀ {A} → let open IVSet A using (_≅_) in
-  ∀ {n} (m : VMap A n)
+  ∀ {A} {n} (m : VMap A n)
     ----------------------
   → Σ[ e ∈ E A ] m ≅ ⟦ e ⟧
 ```
diff --git a/src/Framework/Properties/Finity.agda b/src/Framework/Properties/Finity.agda
index 577360a3..db4b7cb8 100644
--- a/src/Framework/Properties/Finity.agda
+++ b/src/Framework/Properties/Finity.agda
@@ -11,7 +11,7 @@ open import Framework.VariabilityLanguage
 open import Framework.Relation.Index V using (_∋_⊢_≣ⁱ_; ≣ⁱ-IsEquivalence; ≣ⁱ-congruent; ≣ⁱ-setoid)
 open import Framework.Properties.Soundness V
 open import Framework.Relation.Expression V
-open import Framework.Variant V
+open import Data.EqIndexedSet
 open import Util.Enumerable
 
 HasEnumerableNonEmptySemantics : VariabilityLanguage V → Set₁
@@ -35,4 +35,3 @@ soundness-from-enumerability {L} L-has-finite-semantics {A} e =
       where ⟦_⟧ = Semantics L
             fin = L-has-finite-semantics e
             enumerate-configuration = enumerate fin
-            open IVSet A using (IndexedSet; _≅_; ≅-trans; ≅-sym; re-index)
diff --git a/src/Framework/Properties/Soundness.lagda.md b/src/Framework/Properties/Soundness.lagda.md
index 03105d53..f4837e23 100644
--- a/src/Framework/Properties/Soundness.lagda.md
+++ b/src/Framework/Properties/Soundness.lagda.md
@@ -13,7 +13,8 @@ module Framework.Properties.Soundness (V : 𝕍) where
 open import Data.Product using (∃-syntax; Σ-syntax)
 open import Relation.Nullary.Negation  using (¬_)
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
+open import Framework.VariantMap V
+open import Data.EqIndexedSet
 ```
 
 ## Definitions
@@ -21,8 +22,7 @@ open import Framework.Variant V
 ```agda
 Sound : VariabilityLanguage V → Set₁
 Sound ⟪ E , _ , ⟦_⟧ ⟫ =
-  ∀ {A} → let open IVSet A using (_≅_) in
-  ∀ (e : E A)
+  ∀ {A} (e : E A)
     --------------------------------
   → ∃[ n ] Σ[ m ∈ VMap A n ] m ≅ ⟦ e ⟧
 
diff --git a/src/Framework/Relation/Expression.lagda.md b/src/Framework/Relation/Expression.lagda.md
index a821ab16..9443f958 100644
--- a/src/Framework/Relation/Expression.lagda.md
+++ b/src/Framework/Relation/Expression.lagda.md
@@ -9,9 +9,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Function using (_∘_; Injective)
 
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
 
-open IVSet A using
+open import Data.EqIndexedSet using
   ( _⊆_; _≅_; _≐_
   ; ≐→≅
   ; ⊆-refl; ⊆-antisym; ⊆-trans
diff --git a/src/Framework/Relation/Expressiveness.lagda.md b/src/Framework/Relation/Expressiveness.lagda.md
index d28f8f15..b023d8a3 100644
--- a/src/Framework/Relation/Expressiveness.lagda.md
+++ b/src/Framework/Relation/Expressiveness.lagda.md
@@ -9,7 +9,6 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Function using (_∘_; Injective)
 
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
 open import Framework.Relation.Expression V
 open import Framework.Relation.Function using (_⇒ₚ_)
 ```
diff --git a/src/Framework/Variant.agda b/src/Framework/VariantMap.agda
similarity index 71%
rename from src/Framework/Variant.agda
rename to src/Framework/VariantMap.agda
index 25fcfa2e..f3cffaf5 100644
--- a/src/Framework/Variant.agda
+++ b/src/Framework/VariantMap.agda
@@ -1,5 +1,5 @@
 open import Framework.Definitions using (𝕍; 𝔸)
-module Framework.Variant (V : 𝕍) (A : 𝔸) where
+module Framework.VariantMap (V : 𝕍) (A : 𝔸) where
 
 open import Data.Fin using (Fin)
 open import Data.List using (List)
@@ -9,15 +9,7 @@ open import Level using (0ℓ)
 open import Relation.Binary using (Setoid)
 import Relation.Binary.PropositionalEquality as Eq
 
-VariantSetoid : Setoid 0ℓ 0ℓ
-VariantSetoid = Eq.setoid (V A)
-
-import Data.IndexedSet
-module IVSet = Data.IndexedSet VariantSetoid
-
-VMapWithIndex : Set → Set
-VMapWithIndex I = IndexedSet I
-  where open IVSet using (IndexedSet)
+open import Data.EqIndexedSet {V A}
 
 {-|
 Variant maps constitute the semantic domain of variability languages.
@@ -25,7 +17,7 @@ While we defined variant maps to be indexed sets with an arbitrary finite and no
 via Fin (suc n) here for convenience.
 -}
 VMap : ℕ → Set
-VMap n = VMapWithIndex (Fin (suc n))
+VMap n = IndexedSet (Fin (suc n))
 
 -- Utility functions for manipulating variant maps.
 remove-first : ∀ {n} → VMap (suc n) → VMap n
diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda
index 84530f12..0aadb72c 100644
--- a/src/Framework/Variants.agda
+++ b/src/Framework/Variants.agda
@@ -13,6 +13,8 @@ open import Framework.Definitions using (𝕍; 𝔸)
 open import Framework.VariabilityLanguage
 open import Construct.Artifact as At using (_-<_>-; map-children; map-children-preserves) renaming (Syntax to Artifact; Construct to ArtifactC)
 
+open import Data.EqIndexedSet
+
 data GrulerVariant : 𝕍 where
   asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
@@ -62,8 +64,7 @@ VariantEncoder V Γ = LanguageCompiler (Variant-is-VL V) Γ
 
 
 module _ (V : 𝕍) (A : 𝔸) {Γ : VariabilityLanguage V} (encoder : VariantEncoder V Γ) where
-  open import Framework.Variant V A
-  open import Data.IndexedSet VariantSetoid
+  open import Data.EqIndexedSet
 
   private
     ⟦_⟧ = Semantics Γ
@@ -119,9 +120,6 @@ rose-encoder Γ has c = record
         → Artifact (Rose ∞) A
       ⟦_⟧ₚ = pcong ArtifactC Γ
 
-      open import Framework.Variant (Rose ∞) A using (VariantSetoid)
-      open import Data.IndexedSet VariantSetoid
-
       h : ∀ (v : Rose ∞ A) (j : Config Γ) → ⟦ t v ⟧ j ≡ v
       h (rose (a -< cs >-)) j =
         begin
diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md
index cb270edf..ee85079b 100644
--- a/src/Lang/CCC.lagda.md
+++ b/src/Lang/CCC.lagda.md
@@ -19,6 +19,7 @@ module Lang.CCC (Dimension : 𝔽) where
 ## Imports
 ```agda
 -- -- Imports from Standard Library
+open import Data.EqIndexedSet
 open import Data.List
   using (List; []; _∷_; foldl; map)
 open import Data.List.NonEmpty
@@ -26,7 +27,7 @@ open import Data.List.NonEmpty
   renaming (map to map⁺)
 open import Data.Product
   using (_,_; proj₁; proj₂; ∃-syntax; Σ-syntax)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
@@ -87,7 +88,6 @@ module Sem (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where
 Some transformation rules
 ```agda
 module Properties (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where
-  open import Framework.Variant V
   open import Framework.Relation.Expression V
   open Sem V mkArtifact
 
@@ -187,8 +187,8 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
   --     map (flip ⟦_⟧-i c) (map describe-variant (e ∷ es))
   --   ∎)
 
-  sizeof : ∀ {i A} → CCC i A → Size
-  sizeof {i} _ = i
+  -- sizeof : ∀ {i A} → CCC i A → Size
+  -- sizeof {i} _ = i
 ```
 
 
diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md
index 0884a668..17735a78 100644
--- a/src/Lang/VariantList.lagda.md
+++ b/src/Lang/VariantList.lagda.md
@@ -19,17 +19,20 @@ module Lang.VariantList (V : 𝕍) where
 ```agda
 open import Data.Fin using (Fin; zero; suc; toℕ)
 open import Data.List using ([]; _∷_)
-open import Data.List.NonEmpty using (List⁺; _∷_; toList)
+open import Data.List.NonEmpty using (List⁺; _∷_; toList; length)
 open import Data.Nat using (ℕ; zero; suc)
 open import Data.Product using (∃-syntax; _,_; proj₁; proj₂)
-open import Function using (_∘_)
+open import Function using (_∘_; Surjective)
 open import Size using (Size; ∞)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-import Data.IndexedSet
-import Framework.Variant
 open import Framework.VariabilityLanguage
+open import Framework.Properties.Completeness V using (Complete)
+open import Framework.Properties.Soundness V using (Sound)
+open import Framework.Properties.Finity V using (soundness-from-enumerability)
+open import Framework.Relation.Index V using (_∋_⊢_≣ⁱ_)
+open import Data.EqIndexedSet as ISet
 open import Util.List using (find-or-last)
 ```
 
@@ -60,7 +63,7 @@ VariantListL = ⟪ VariantList , Configuration , ⟦_⟧ ⟫
 open import Util.AuxProofs using (clampAt)
 
 private
-  open Framework.Variant V
+  open import Framework.VariantMap V
   variable
     n : ℕ
     A : 𝔸
@@ -91,8 +94,8 @@ determinism : ∀ {e₁ e₂ : VariantList A} {V : VMap A n}
   → n ⊢ V ⟶ e₂
     -----------------
   → e₁ ≡ e₂
-determinism E-zero E-zero = Eq.refl
-determinism (E-suc l) (E-suc r) rewrite determinism l r = Eq.refl
+determinism E-zero E-zero = refl
+determinism (E-suc l) (E-suc r) rewrite determinism l r = refl
 
 -- smart constructor for totality proofs
 -- makes the implicit result expression e explicit
@@ -122,39 +125,32 @@ vl-conf i = toℕ i
 vl-fnoc : Configuration → Fin (suc n)
 vl-fnoc {n} c = clampAt n c
 
--- proof of preservation
+preserves-∈ : ∀ {V}
+  → n ⊢ V ⟶ e
+    -----------------
+  → V ⊆[ vl-conf ] ⟦ e ⟧
+preserves-∈ E-zero    zero = refl
 
-module _ {A : 𝔸} where
-  open IVSet A using (_≅_; _⊆[_]_; ≅[]→≅)
-
-  preserves-∈ : ∀ {V}
-    → n ⊢ V ⟶ e
-      -----------------
-    → V ⊆[ vl-conf ] ⟦ e ⟧
-  preserves-∈ E-zero    zero = refl
-
-  preserves-∈ (E-suc _) zero = refl
-  preserves-∈ (E-suc ⟶e) (suc i) = preserves-∈ ⟶e i
-
-  preserves-∋ : ∀ {V}
-    → n ⊢ V ⟶ e
-      -----------------
-    → ⟦ e ⟧ ⊆[ vl-fnoc ] V
-  preserves-∋ E-zero      zero   = refl
-  preserves-∋ E-zero     (suc _) = refl
-  preserves-∋ (E-suc  _)  zero   = refl
-  preserves-∋ (E-suc ⟶e) (suc c) = preserves-∋ ⟶e c
-
-  preserves : ∀ {V}
-    → n ⊢ V ⟶ e
-      ----------
-    → V ≅ ⟦ e ⟧
-  preserves encoding = ≅[]→≅ (preserves-∈ encoding , preserves-∋ encoding)
+preserves-∈ (E-suc _) zero = refl
+preserves-∈ (E-suc ⟶e) (suc i) = preserves-∈ ⟶e i
 
-open import Framework.Properties.Completeness V using (Complete)
+preserves-∋ : ∀ {V}
+  → n ⊢ V ⟶ e
+    -----------------
+  → ⟦ e ⟧ ⊆[ vl-fnoc ] V
+preserves-∋ E-zero      zero   = refl
+preserves-∋ E-zero     (suc _) = refl
+preserves-∋ (E-suc  _)  zero   = refl
+preserves-∋ (E-suc ⟶e) (suc c) = preserves-∋ ⟶e c
+
+preserves : ∀ {V}
+  → n ⊢ V ⟶ e
+    ----------
+  → V ≅ ⟦ e ⟧
+preserves encoding = ≅[]→≅ (preserves-∈ encoding , preserves-∋ encoding)
 
 VariantList-is-Complete : Complete VariantListL
-VariantList-is-Complete {A} vs =
+VariantList-is-Complete vs =
   let e , derivation = total vs
   in  e , preserves derivation
 ```
@@ -162,12 +158,6 @@ VariantList-is-Complete {A} vs =
 ### Soundness
 
 ```agda
-open import Framework.Properties.Soundness V using (Sound)
-open import Framework.Properties.Finity V using (soundness-from-enumerability)
-open import Framework.Relation.Index V using (_∋_⊢_≣ⁱ_)
-open Data.List.NonEmpty using (length)
-open Function using (Surjective)
-
 module _ {A : 𝔸} where
   #' : VariantList A → ℕ
   #' = length
diff --git a/src/Translation/Construct/2Choice-to-NChoice-VL.agda b/src/Translation/Construct/2Choice-to-NChoice-VL.agda
index a6329dca..13c05156 100644
--- a/src/Translation/Construct/2Choice-to-NChoice-VL.agda
+++ b/src/Translation/Construct/2Choice-to-NChoice-VL.agda
@@ -12,7 +12,6 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≗_; refl)
 
 import Data.IndexedSet
 
-open import Framework.Variant
 open import Framework.VariabilityLanguage
 open import Framework.Construct
 open import Framework.Compiler using (LanguageCompiler)
@@ -90,9 +89,8 @@ module Translate {Q : 𝔽} {V : 𝕍} {A : 𝔸}
     where
     open 2→N-T₂.Preservation confi fnoci using (convert-preserves)
 
-    module VSet = IVSet V A
-    open VSet using (_≅[_][_]_)
-    open VSet.≅[]-Reasoning
+    open import Data.EqIndexedSet as ISet
+    open ISet.≅[]-Reasoning
 
     extract₂ : Compatible (Chc.VLChoiceₙ.Construct V Q) Γ₂
     extract₂ = confi ∘ extract₁ ∘ fnoc -- proof by diagram chasing
diff --git a/src/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Translation/Lang/VariantList-to-CCC.lagda.md
index 5189f267..daa524e2 100644
--- a/src/Translation/Lang/VariantList-to-CCC.lagda.md
+++ b/src/Translation/Lang/VariantList-to-CCC.lagda.md
@@ -12,6 +12,7 @@
 open import Framework.Definitions
 open import Framework.Construct
 open import Construct.Artifact as At using () renaming (Syntax to Artifact)
+open import Data.EqIndexedSet
 
 module Translation.Lang.VariantList-to-CCC
   (Dimension : 𝔽)
@@ -33,7 +34,7 @@ open import Data.Product using (_,_; proj₁)
 open import Function using (id; flip; _∘_; _$_)
 open import Size
 
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 open Eq.≡-Reasoning
 
 open import Framework.VariabilityLanguage
@@ -45,7 +46,6 @@ open import Lang.CCC Dimension as CCC-Module
   renaming (Configuration to Cᶜ)
 open CCC-Module.Sem V mkArtifact
 
-import Framework.Variant
 open import Framework.Variants
 
 open import Util.List using (find-or-last; map-find-or-last; map⁺-id)
@@ -73,9 +73,7 @@ module Translate
 
 ```agda
   module Preservation (A : 𝔸) where
-    open Framework.Variant V A
     open import Framework.Properties.Completeness V using (Complete)
-    open IVSet using (_≅_; irrelevant-index; _⊆[_]_; _≅[_][_]_; ≅[]→≅)
 
     ⟦_⟧ᵥ = Semantics (Variant-is-VL V)
     open import Data.Unit using (tt)
@@ -134,16 +132,16 @@ module Translate
       let ⟦⟧c = flip ⟦_⟧ c
           tail = w ∷ zs
           tail-in-ccc = map⁺ compile tail
-      in Eq.sym $
+      in sym $
       begin
         find-or-last i tail
-      ≡⟨ Eq.cong (find-or-last i) (Eq.sym (map⁺-id tail)) ⟩
+      ≡⟨ Eq.cong (find-or-last i) (sym (map⁺-id tail)) ⟩
         find-or-last i (map⁺ id tail)
       ≡˘⟨ Eq.cong (find-or-last i) (map⁺-cong (encode-idemp V A embed c) tail) ⟩
         find-or-last i (map⁺ (⟦⟧c ∘ compile) tail)
       ≡⟨ Eq.cong (find-or-last i) (map⁺-∘ tail) ⟩
         find-or-last i (map⁺ ⟦⟧c tail-in-ccc)
-      ≡⟨ Eq.sym (map-find-or-last ⟦⟧c i tail-in-ccc) ⟩
+      ≡⟨ sym (map-find-or-last ⟦⟧c i tail-in-ccc) ⟩
         ⟦⟧c (find-or-last i tail-in-ccc)
       ≡⟨⟩
         ⟦_⟧ (find-or-last i tail-in-ccc) c
@@ -160,16 +158,21 @@ module Translate
         preserves-⊆ e , preserves-⊇ e
     }
 
-open Framework.Variant V
 open import Framework.Properties.Completeness V using (Complete)
 open import Framework.Relation.Expressiveness V using (_≽_)
 open import Framework.Proof.Transitive V using (completeness-by-expressiveness)
 
+comp : ∀ (mkArtifact : Artifact ∈ₛ V) → LanguageCompiler (Variant-is-VL V) CCCL
+comp mkArtifact = record
+  { compile = {!!}
+  ; config-compiler = {!!}
+  ; preserves = {!!}
+  }
+
 CCCL-is-at-least-as-expressive-as-VariantListL : CCCL ≽ VariantListL
 CCCL-is-at-least-as-expressive-as-VariantListL {A} e = translate e , ≅[]→≅ (LanguageCompiler.preserves VariantList→CCC e)
   where
     open Translate {!!}
-    open IVSet A using (≅[]→≅)
 
 CCCL-is-complete : Complete CCCL
 CCCL-is-complete = completeness-by-expressiveness VariantList-is-Complete CCCL-is-at-least-as-expressive-as-VariantListL