diff --git a/src/Construct/Artifact.agda b/src/Construct/Artifact.agda
index 88c46701..456e050a 100644
--- a/src/Construct/Artifact.agda
+++ b/src/Construct/Artifact.agda
@@ -2,7 +2,7 @@ module Construct.Artifact where
 
 open import Data.List using (List; map)
 open import Data.List.Properties using (map-cong; map-∘)
-open import Data.Product using (proj₁; proj₂; _,_)
+open import Data.Product using (_,_)
 open import Level using (_⊔_)
 open import Function using (id; flip; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
@@ -17,7 +17,7 @@ import Data.IndexedSet
 open import Construct.Plain.Artifact public
 
 Syntax : ℂ
-Syntax E A = Artifact A (E A)
+Syntax E A = Artifact (atoms A) (E A)
 
 Construct : PlainConstruct
 Construct = Plain-⟪ Syntax , (λ Γ e c → map-children (flip (Semantics Γ) c) e) ⟫
diff --git a/src/Construct/GrulerArtifacts.agda b/src/Construct/GrulerArtifacts.agda
index 8a9df63b..278bc26c 100644
--- a/src/Construct/GrulerArtifacts.agda
+++ b/src/Construct/GrulerArtifacts.agda
@@ -23,15 +23,15 @@ record ParallelComposition {ℓ} (A : Set ℓ) : Set ℓ where
 
 module VLLeaf where
   Syntax : ℂ
-  Syntax _ A = Leaf A
+  Syntax _ A = Leaf (atoms A)
 
   make-leaf :
     ∀ {E : 𝔼} → Syntax ∈ₛ E
-    → {A : 𝔸} → A
+    → {A : 𝔸} → atoms A
     → E A
   make-leaf mkLeaf a = cons mkLeaf (leaf a)
 
-  elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf A → V A
+  elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf (atoms A) → V A
   elim-leaf leaf∈V l = cons leaf∈V l
 
   Construct : PlainConstruct
diff --git a/src/Construct/NestedChoice.agda b/src/Construct/NestedChoice.agda
index 0fdf2e6d..912ece3d 100644
--- a/src/Construct/NestedChoice.agda
+++ b/src/Construct/NestedChoice.agda
@@ -9,7 +9,7 @@ open import Size using (Size; ↑_)
 
 open import Construct.Choices
 
-data NestedChoice : Size → 𝔼 where
+data NestedChoice : Size → Set → Set where
   value  : ∀ {i A} → A → NestedChoice i A
   choice : ∀ {i A} → 2Choice.Syntax F (NestedChoice i A) → NestedChoice (↑ i) A
 
diff --git a/src/Framework/Definitions.agda b/src/Framework/Definitions.agda
index 4522c239..91129869 100644
--- a/src/Framework/Definitions.agda
+++ b/src/Framework/Definitions.agda
@@ -1,10 +1,11 @@
 module Framework.Definitions where
 
 open import Data.Maybe using (Maybe; just)
-open import Data.Product using (_×_; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
+open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
 open import Data.Unit using (⊤; tt) public
 open import Function using (id; _∘_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl)
+open import Relation.Binary using (DecidableEquality)
 open import Relation.Nullary.Negation using (¬_)
 
 -- open import Level using (suc; _⊔_)
@@ -16,7 +17,10 @@ We have no assumptions on that data so its just a type.
 -- 𝔸 : ∀ {ℓ} → Set (suc ℓ)
 -- 𝔸 {ℓ} = Set ℓ
 𝔸 : Set₁
-𝔸 = Set
+𝔸 = Σ Set DecidableEquality
+
+atoms : 𝔸 → Set
+atoms = proj₁
 
 {-
 Variant Language.
diff --git a/src/Framework/Relation/Index.lagda.md b/src/Framework/Relation/Index.lagda.md
index 192f67dc..f58436a0 100644
--- a/src/Framework/Relation/Index.lagda.md
+++ b/src/Framework/Relation/Index.lagda.md
@@ -1,5 +1,5 @@
 ```agda
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; 𝔸)
 module Framework.Relation.Index (V : 𝕍) where
 
 open import Level using (0ℓ)
@@ -15,7 +15,7 @@ Two indices are equivalent for an expression when they produce the same output f
 ```agda
 𝕃 = VariabilityLanguage V
 
-module _ {A : Set} where
+module _ {A : 𝔸} where
   _∋_⊢_≣ⁱ_ :
     ∀ (L : 𝕃)
     → Expression L A
diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda
index f3454793..b00d158b 100644
--- a/src/Framework/Variants.agda
+++ b/src/Framework/Variants.agda
@@ -9,20 +9,20 @@ open import Data.List using ([]; _∷_; map)
 open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
-open import Framework.Definitions using (𝕍; 𝔸)
+open import Framework.Definitions using (𝕍; 𝔸; atoms)
 open import Framework.VariabilityLanguage
 open import Construct.Artifact as At using (_-<_>-; map-children) renaming (Syntax to Artifact; Construct to ArtifactC)
 
 open import Data.EqIndexedSet
 
 data GrulerVariant : 𝕍 where
-  asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
+  asset : ∀ {A : 𝔸} (a : atoms A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
 
 data Rose : Size → 𝕍 where
   rose : ∀ {i} {A : 𝔸} → Artifact (Rose i) A → Rose (↑ i) A
 
-rose-leaf : ∀ {A : 𝔸} → A → Rose ∞ A
+rose-leaf : ∀ {A : 𝔸} → atoms A → Rose ∞ A
 rose-leaf {A} a = rose (At.leaf a)
 
 -- Variants are also variability languages
@@ -46,7 +46,7 @@ RoseVL : VariabilityLanguage (Rose ∞)
 RoseVL = Variant-is-VL (Rose ∞)
 
 open import Data.String using (String; _++_; intersperse)
-show-rose : ∀ {i} {A} → (A → String) → Rose i A → String
+show-rose : ∀ {i} {A} → (atoms A → String) → Rose i A → String
 show-rose show-a (rose (a -< [] >-)) = show-a a
 show-rose show-a (rose (a -< es@(_ ∷ _) >-)) = show-a a ++ "-<" ++ (intersperse ", " (map (show-rose show-a) es)) ++ ">-"
 
diff --git a/src/Lang/2CC.lagda.md b/src/Lang/2CC.lagda.md
index 20f289a6..40cf1eae 100644
--- a/src/Lang/2CC.lagda.md
+++ b/src/Lang/2CC.lagda.md
@@ -21,6 +21,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List
   using (List; []; _∷_; lookup)
   renaming (map to mapl)
+open import Data.Product using (_,_)
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
 
@@ -91,7 +92,7 @@ Some transformation rules:
     open Sem V mkArtifact
 
     module _ {A : 𝔸} where
-      ast-factoring : ∀ {i} {D : Dimension} {a : A} {n : ℕ}
+      ast-factoring : ∀ {i} {D : Dimension} {a : atoms A} {n : ℕ}
         → (xs ys : Vec (2CC Dimension i A) n)
           -------------------------------------------------------------------------------------
         → 2CCL Dimension ⊢
@@ -189,7 +190,7 @@ Some transformation rules:
   open Data.List using (concatMap) renaming (_++_ to _++l_)
 
   -- get all dimensions used in a binary CC expression
-  dims : ∀ {i : Size} {A : Set} → 2CC Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → 2CC Dimension i A → List Dimension
   dims (_ -< es >-) = concatMap dims es
   dims (D ⟨ l , r ⟩) = D ∷ (dims l ++l dims r)
 ```
@@ -197,17 +198,17 @@ Some transformation rules:
 ## Show
 
 ```agda
-  open import Data.String using (String; _++_; intersperse)
+  open import Data.String as String using (String; _++_; intersperse)
   module Pretty (show-D : Dimension → String) where
     open import Show.Lines
 
-    show : ∀ {i} → 2CC Dimension i String → String
+    show : ∀ {i} → 2CC Dimension i (String , String._≟_) → String
     show (a -< [] >-) = a
     show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (intersperse ", " (mapl show es)) ++ ">-"
     show (D ⟨ l , r ⟩) = show-D D ++ "⟨" ++ (show l) ++ ", " ++ (show r) ++ "⟩"
 
 
-    pretty : ∀ {i : Size} → 2CC Dimension i String → Lines
+    pretty : ∀ {i : Size} → 2CC Dimension i (String , String._≟_) → Lines
     pretty (a -< [] >-) = > a
     pretty (a -< es@(_ ∷ _) >-) = do
       > a ++ "-<"
diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md
index 83641777..4e554a81 100644
--- a/src/Lang/CCC.lagda.md
+++ b/src/Lang/CCC.lagda.md
@@ -187,7 +187,7 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
   -- get all dimensions used in a CCC Dimension expression
   open Data.List using (concatMap)
 
-  dims : ∀ {i : Size} {A : Set} → CCC Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → CCC Dimension i A → List Dimension
   dims (_ -< es >-) = concatMap dims es
   dims (D ⟨ es ⟩) = D ∷ concatMap dims (toList es)
 ```
@@ -195,10 +195,10 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
 ## Show
 
 ```agda
-  open import Data.String using (String; _++_)
+  open import Data.String as String using (String; _++_)
 
-  show : ∀ {i} → (Dimension → String) → CCC Dimension i String → String
+  show : ∀ {i} → (Dimension → String) → CCC Dimension i (String , String._≟_) → String
   show _ (a -< [] >-) = a
   show show-D (a -< es@(_ ∷ _) >- ) = a ++ "-<" ++ (foldl _++_ "" (map (show show-D) es)) ++ ">-"
-  show show-D (D ⟨ es ⟩) = show-D D ++ "⟨" ++ (Data.String.intersperse ", " (toList (map⁺ (show show-D) es))) ++ "⟩"
+  show show-D (D ⟨ es ⟩) = show-D D ++ "⟨" ++ (String.intersperse ", " (toList (map⁺ (show show-D) es))) ++ "⟩"
 ```
diff --git a/src/Lang/Gruler.agda b/src/Lang/Gruler.agda
index f84424ec..0989297e 100644
--- a/src/Lang/Gruler.agda
+++ b/src/Lang/Gruler.agda
@@ -23,7 +23,7 @@ private
   pc-semantics = PlainConstruct-Semantics VLParallelComposition.Construct VLParallelComposition.ParallelComposition∈ₛGrulerVariant
 
 data Gruler : Size → 𝔼 where
-  GAsset  : ∀ {i A} → Leaf A                           → Gruler i A
+  GAsset  : ∀ {i A} → Leaf (atoms A)                   → Gruler i A
   GPComp  : ∀ {i A} → ParallelComposition (Gruler i A) → Gruler (↑ i) A
   GChoice : ∀ {i A} → VL2Choice.Syntax F (Gruler i) A  → Gruler (↑ i) A
 
@@ -42,7 +42,7 @@ gruler-has-leaf {i} = record
   ; snoc = snoc'
   ; id-l = λ _ → refl
   }
-  where snoc' : ∀ {A} → Gruler i A → Maybe (Leaf A)
+  where snoc' : ∀ {A} → Gruler i A → Maybe (Leaf (atoms A))
         snoc' (GAsset A)  = just A
         snoc' _ = nothing
 
diff --git a/src/Lang/NCC.lagda.md b/src/Lang/NCC.lagda.md
index d82303e7..0f999eba 100644
--- a/src/Lang/NCC.lagda.md
+++ b/src/Lang/NCC.lagda.md
@@ -26,6 +26,7 @@ open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List
   using (List; []; _∷_; lookup)
   renaming (map to mapl)
+open import Data.Product using (_,_)
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
 
@@ -74,7 +75,7 @@ module _ {n : ℕ≥ 2} {Dimension : 𝔽} where
   import Data.Vec as Vec
 
   -- get all dimensions used in a binary CC expression
-  dims : ∀ {i : Size} {A : Set} → NCC n Dimension i A → List Dimension
+  dims : ∀ {i : Size} {A : 𝔸} → NCC n Dimension i A → List Dimension
   dims (_ -< es >-) = concatMap dims es
   dims (D ⟨ cs ⟩) = D ∷ concatMap dims (Vec.toList cs)
 ```
@@ -82,17 +83,17 @@ module _ {n : ℕ≥ 2} {Dimension : 𝔽} where
 ## Show
 
 ```agda
-  open import Data.String using (String; _++_; intersperse)
+  open import Data.String as String using (String; _++_; intersperse)
   module Pretty (show-D : Dimension → String) where
     open import Show.Lines
 
-    show : ∀ {i} → NCC n Dimension i String → String
+    show : ∀ {i} → NCC n Dimension i (String , String._≟_) → String
     show (a -< [] >-) = a
     show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (intersperse ", " (mapl show es)) ++ ">-"
     show (D ⟨ cs ⟩) = show-D D ++ "⟨" ++ (intersperse ", " (mapl show (Vec.toList cs))) ++ "⟩"
 
 
-    pretty : ∀ {i : Size} → NCC n Dimension i String → Lines
+    pretty : ∀ {i : Size} → NCC n Dimension i (String , String._≟_) → Lines
     pretty (a -< [] >-) = > a
     pretty (a -< es@(_ ∷ _) >-) = do
       > a ++ "-<"
diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md
index 578cd2e4..358e9a8c 100644
--- a/src/Lang/OC.lagda.md
+++ b/src/Lang/OC.lagda.md
@@ -19,7 +19,7 @@ module Lang.OC where
 ```agda
 open import Data.Bool using (Bool; true; false; if_then_else_)
 open import Data.List using (List; []; _∷_)
-open import Data.String using (String)
+open import Data.String as String using (String)
 open import Size using (Size; ∞; ↑_)
 open import Function using (_∘_)
 
@@ -46,7 +46,7 @@ data OC (Option : 𝔽) : Size → 𝔼 where
   Maybe reusing Artifact hides something from the Agda
   compiler that it needs for termination checking.
   -}
-  _-<_>- : ∀ {i A} → A → List (OC Option i A) → OC Option (↑ i) A
+  _-<_>- : ∀ {i A} → atoms A → List (OC Option i A) → OC Option (↑ i) A
   _❲_❳ : ∀ {i : Size} {A : 𝔸} →
     Option → OC Option i A → OC Option (↑ i) A
 infixl 6 _❲_❳
@@ -144,7 +144,7 @@ And now for the semantics of well-formed option calculus which just reuses the s
 
 ```agda
 open import Data.Fin using (zero; suc)
-open import Data.Nat using (ℕ; zero; suc)
+open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Product   using (_,_; ∃-syntax; ∄-syntax)
 open import Util.Existence using (_,_)
 open import Data.List.Relation.Unary.All using (_∷_; [])
@@ -163,12 +163,12 @@ As our counter example, we use the set `{0, 1}` as our variants:
   -- TODO: Can this be generalized to other types of variants as well?
   module IncompleteOnRose where
     open import Framework.Variants using (Rose; Artifact∈ₛRose)
-    open import Framework.VariantMap (Rose ∞) ℕ
+    open import Framework.VariantMap (Rose ∞) (ℕ , ℕ._≟_)
     open import Framework.Properties.Completeness (Rose ∞) using (Incomplete)
     open Sem (Rose ∞) Artifact∈ₛRose
 
-    variant-0 = rose-leaf 0
-    variant-1 = rose-leaf 1
+    variant-0 = rose-leaf {A = (ℕ , ℕ._≟_)} 0
+    variant-1 = rose-leaf {A = (ℕ , ℕ._≟_)} 1
     -- variant-0 = cons mkArtifact (At.leaf 0)
     -- variant-1 = cons mkArtifact (At.leaf 1)
 
@@ -183,7 +183,7 @@ So we show that given an expression `e`, a proof that `e` can be configured to `
 ```agda
     does-not-describe-variants-0-and-1 :
       ∀ {i : Size}
-      → (e : WFOC Option i ℕ)
+      → (e : WFOC Option i (ℕ , ℕ._≟_))
       → ∃[ c ] (variant-0 ≡ ⟦ e ⟧ c)
       → ∄[ c ] (variant-1 ≡ ⟦ e ⟧ c)
     -- If e has 0 as root, it may be configured to 0 but never to 1.
@@ -208,14 +208,14 @@ Another way is to enrich the annotation language, for example using propositiona
 ## Utility
 
 ```agda
-  oc-leaf : ∀ {i : Size} {A : 𝔸} → A → OC Option (↑ i) A
+  oc-leaf : ∀ {i : Size} {A : 𝔸} → atoms A → OC Option (↑ i) A
   oc-leaf a = a -< [] >-
 
   -- alternative name that does not require writing tortoise shell braces
   opt : ∀ {i : Size} {A : 𝔸} → Option → OC Option i A → OC Option (↑ i) A
   opt O = _❲_❳ O
 
-  singleton : ∀ {i : Size} {A : 𝔸} → A → OC Option i A → OC Option (↑ i) A
+  singleton : ∀ {i : Size} {A : 𝔸} → atoms A → OC Option i A → OC Option (↑ i) A
   singleton a e = a -< e ∷ [] >-
 
   open import Util.Named
@@ -233,15 +233,15 @@ Another way is to enrich the annotation language, for example using propositiona
 ## Show
 
 ```agda
-open Data.String using (_++_; intersperse)
+open String using (_++_; intersperse)
 open import Function using (_∘_)
 
 module Show (Option : 𝔽) (print-opt : Option → String) where
-  show-oc : ∀ {i : Size} → OC Option i String → String
+  show-oc : ∀ {i : Size} → OC Option i (String , String._≟_) → String
   show-oc (s -< [] >-) = s
   show-oc (s -< es@(_ ∷ _) >-) = s ++ "-<" ++ (intersperse ", " (map show-oc es)) ++ ">-"
   show-oc (O ❲ e ❳) = print-opt O ++ "❲" ++ show-oc e ++ "❳"
 
-  show-wfoc : ∀ {i : Size} → WFOC Option i String → String
+  show-wfoc : ∀ {i : Size} → WFOC Option i (String , String._≟_) → String
   show-wfoc = show-oc ∘ forgetWF
 ```
diff --git a/src/Test/Examples/CCC.agda b/src/Test/Examples/CCC.agda
index d77b4b3b..5e68323c 100644
--- a/src/Test/Examples/CCC.agda
+++ b/src/Test/Examples/CCC.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --sized-types #-}
 module Test.Examples.CCC where
 
-open import Data.String using (String)
+open import Data.String as String using (String)
 open import Data.List using (List; _∷_; [])
 open import Data.List.NonEmpty
   using (List⁺; _∷_; toList)
@@ -11,6 +11,7 @@ open import Data.Product
 open import Size
   using (Size; ∞; ↑_)
 
+open import Framework.Definitions using (𝔸; atoms)
 open import Construct.Plain.Artifact using (leaf; leaves⁺)
 
 open import Lang.All
@@ -18,19 +19,19 @@ open CCC -- use strings as dimensions
 open import Test.Example
 
 CCCExample : Set
-CCCExample = Example (CCC String ∞ String)
+CCCExample = Example (CCC String ∞ (String , String._≟_))
 
 -- some smart constructors
-ccA : ∀ {i : Size} {A : Set} → List⁺ (CCC String i A) → CCC String (↑ i) A
+ccA : ∀ {i : Size} {A : 𝔸} → List⁺ (CCC String i A) → CCC String (↑ i) A
 ccA es = "A" ⟨ es ⟩
 
-cc-leaves : ∀ {i : Size} {A : Set} → String → List⁺ A → CCC String (↑ ↑ i) A
+cc-leaves : ∀ {i : Size} {A : 𝔸} → String → List⁺ (atoms A) → CCC String (↑ ↑ i) A
 cc-leaves D es = D ⟨ map⁺ atom (leaves⁺ es) ⟩
 
-ccA-leaves : ∀ {i : Size} {A : Set} → List⁺ A → CCC String (↑ ↑ i) A
+ccA-leaves : ∀ {i : Size} {A : 𝔸} → List⁺ (atoms A) → CCC String (↑ ↑ i) A
 ccA-leaves = cc-leaves "A"
 
-cc-leaf : ∀ {i : Size} {A : Set} → A → CCC String (↑ i) A
+cc-leaf : ∀ {i : Size} {A : 𝔸} → (atoms A) → CCC String (↑ i) A
 cc-leaf a = atom (leaf a)
 
 -- examples
diff --git a/src/Test/Examples/OC.agda b/src/Test/Examples/OC.agda
index 56d1d4dd..1adf171a 100644
--- a/src/Test/Examples/OC.agda
+++ b/src/Test/Examples/OC.agda
@@ -3,7 +3,8 @@
 module Test.Examples.OC where
 
 open import Data.List using (List; []; _∷_; [_])
-open import Data.String using (String)
+open import Data.String as String using (String)
+open import Data.Product using (_,_)
 open import Size using (Size; ↑_; ∞)
 
 -- open import Framework.Annotation.Name using (Option)
@@ -14,7 +15,7 @@ open OC
 open import Test.Example
 
 OCExample : Set
-OCExample = Example (WFOC String ∞ String)
+OCExample = Example (WFOC String ∞ (String , String._≟_))
 
 optex-unary : OCExample
 optex-unary = "unary" ≔ (Root "r" [ opt "O" (oc-leaf "lol") ])
diff --git a/src/Test/Examples/Variants.agda b/src/Test/Examples/Variants.agda
index d5907cd8..34b848fa 100644
--- a/src/Test/Examples/Variants.agda
+++ b/src/Test/Examples/Variants.agda
@@ -3,24 +3,24 @@
 module Test.Examples.Variants where
 
 open import Data.Fin using (zero; suc)
-open import Data.Nat using (ℕ)
+open import Data.Nat as ℕ using (ℕ)
 open import Data.Product using (∃-syntax; _,_)
 open import Data.List using (List; []; _∷_)
-open import Data.String using (String)
+open import Data.String as String using (String)
 open import Size using (∞)
 open import Framework.Variants using (Rose; rose-leaf)
 open import Framework.VariantMap (Rose ∞) using (VMap)
 
 open import Test.Example
 
-𝕍-123 : Example (VMap ℕ 2)
+𝕍-123 : Example (VMap (ℕ , ℕ._≟_) 2)
 𝕍-123 = "123" ≔ set
-  where set : VMap ℕ 2
+  where set : VMap (ℕ , ℕ._≟_) 2
         set zero = rose-leaf 1
         set (suc zero) = rose-leaf 2
         set (suc (suc zero)) = rose-leaf 3
 
-𝕍-lr : Example (VMap String 1)
+𝕍-lr : Example (VMap (String , String._≟_) 1)
 getName 𝕍-lr = "lr"
 get 𝕍-lr zero = rose-leaf "left"
 get 𝕍-lr (suc zero) = rose-leaf "right"
diff --git a/src/Test/Experiments/OC-to-2CC.agda b/src/Test/Experiments/OC-to-2CC.agda
index e13ad6d2..781089cb 100644
--- a/src/Test/Experiments/OC-to-2CC.agda
+++ b/src/Test/Experiments/OC-to-2CC.agda
@@ -5,8 +5,8 @@ module Test.Experiments.OC-to-2CC where
 open import Data.Bool using (Bool; true; false)
 open import Data.List using (_∷_; [])
 open import Data.Nat using (_+_)
-open import Data.Product using (proj₁; proj₂)
-open import Data.String using (String; _++_; unlines; _==_)
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.String as String using (String; _++_; unlines; _==_)
 
 open import Size using (Size; ∞)
 open import Function using (id)
@@ -65,7 +65,7 @@ OC→2CC-Test-conffnoc-allno = refl ∷ refl ∷ refl ∷ refl ∷ []
 
 -- Translate an option calculus expression.
 -- Then configure it with an all-yes and an all-no config and print the resulting variants.
-exp-oc-to-bcc : Experiment (WFOC Feature ∞ String)
+exp-oc-to-bcc : Experiment (WFOC Feature ∞ (String , String._≟_))
 getName exp-oc-to-bcc = "Translate OC to 2CC"
 get     exp-oc-to-bcc ex@(name ≔ oc) = do
   let --trans-result   = translate oc
diff --git a/src/Translation/Construct/Choice-to-2Choice.agda b/src/Translation/Construct/Choice-to-2Choice.agda
index d0800f80..3e63e509 100644
--- a/src/Translation/Construct/Choice-to-2Choice.agda
+++ b/src/Translation/Construct/Choice-to-2Choice.agda
@@ -17,11 +17,9 @@ open import Size using (Size; ↑_; ∞)
 open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≢_)
 import Relation.Binary.PropositionalEquality as Eq
 
-import Data.IndexedSet
+import Data.EqIndexedSet
 open import Util.List using (find-or-last)
 
-open import Relation.Binary using (Setoid; IsEquivalence)
-
 open import Util.AuxProofs using (true≢false; n≡ᵇn; n<m→m≡ᵇn)
 open import Framework.Annotation.IndexedName using (IndexedName; _∙_; show-IndexedName)
 open import Construct.Choices
@@ -105,31 +103,28 @@ record FnocContract (D : Q) (fnoc : 2Config → NConfig) : Set where
       → fnoc c D ≢ i
 open FnocContract
 
-module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
-  open Setoid S
-  module ≈-Eq = IsEquivalence isEquivalence
-
-  show-nested-choice : ∀ {i} → (Q → String) → (Carrier → String) → NestedChoice i Carrier → String
+module Translate (A : Set) where
+  show-nested-choice : ∀ {i} → (Q → String) → (A → String) → NestedChoice i A → String
   show-nested-choice show-q = NestedChoice.show-nested-choice (show-IndexedName show-q)
 
-  ⟦_⟧ : ∀ {i : Size} → NestedChoice i Carrier → 2Config → Carrier
+  ⟦_⟧ : ∀ {i : Size} → NestedChoice i A → 2Config → A
   ⟦ chc ⟧ c = ⟦ chc ⟧ₒ (evalConfig c)
 
-  convert' : Q → Carrier → List Carrier → ℕ → NestedChoice ∞ Carrier
+  convert' : Q → A → List A → ℕ → NestedChoice ∞ A
   convert' D l []       n = value l
   convert' D l (r ∷ rs) n = choice ((D ∙ n) ⟨ value l , convert' D r rs (suc n) ⟩)
 
-  convert : Choice.Syntax Q Carrier → NestedChoice ∞ Carrier
+  convert : Choice.Syntax Q A → NestedChoice ∞ A
   convert (D ⟨ c ∷ cs ⟩) = convert' D c cs zero
 
   module Preservation
       (conf : NConfig → 2Config)
       (fnoc : 2Config → NConfig)
       where
-    open Data.IndexedSet S using (_⊆[_]_; _≅[_][_]_; _≅_)
+    open Data.EqIndexedSet using (_⊆[_]_; _≅[_][_]_; _≅_)
 
     preserves-conf :
-      ∀ (chc : Choice.Syntax Q Carrier)
+      ∀ (chc : Choice.Syntax Q A)
       → ConfContract (Choice.Syntax.dim chc) conf
         -----------------------------------
       → Choice.⟦ chc ⟧ ⊆[ conf ] ⟦ convert chc ⟧
@@ -149,17 +144,17 @@ module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
         Hence, we introduce `n` which decreases each iteration such that we have
         `n + m ≡ c D`.
         -}
-        induction : (l : Carrier) → (rs : List Carrier)
+        induction : (l : A) → (rs : List A)
                   → (n m : ℕ)
                   → n + m ≡ c D
-                  → find-or-last n (l ∷ rs) ≈ ⟦ convert' D l rs m ⟧ (conf c)
+                  → find-or-last n (l ∷ rs) ≡ ⟦ convert' D l rs m ⟧ (conf c)
         -- Only one alternative left
-        induction l [] n m n+m≡cD = ≈-Eq.refl
+        induction l [] n m n+m≡cD = refl
         -- Select the current alternative (numbered `m`) because
         -- `c D = 0 + m = m`
         induction l (r ∷ rs) zero m m≡cD
           rewrite select-n confContract c (Eq.sym m≡cD)
-          = ≈-Eq.refl
+          = refl
         -- Ignore the current alternative (numbered `m`) and select one of the
         -- later alternatives (numbered `> m`) because `c D = suc n + m` and
         -- thus `c D > m`
@@ -169,7 +164,7 @@ module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
           = induction r rs n (suc m) n+m≡cD
 
     preserves-fnoc :
-      ∀ (chc : Choice.Syntax Q Carrier)
+      ∀ (chc : Choice.Syntax Q A)
       → FnocContract (Choice.Syntax.dim chc) fnoc
         -----------------------------------
       → ⟦ convert chc ⟧ ⊆[ fnoc ] Choice.⟦ chc ⟧
@@ -186,13 +181,13 @@ module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
         to  fulfill FnocContract we also need to remember (in `ps`) that all
         alternatives with an index `< n` where not selected.
         -}
-        induction : (l : Carrier) → (rs : List Carrier)
+        induction : (l : A) → (rs : List A)
                   → (n m : ℕ)
                   → fnoc c D ≡ n + m
                   → (∀ (j : ℕ) → j < n → evalConfig c (D ∙ j) ≡ false)
-                  → ⟦ convert' D l rs n ⟧ c ≈ find-or-last m (l ∷ rs)
+                  → ⟦ convert' D l rs n ⟧ c ≡ find-or-last m (l ∷ rs)
         -- Only one alternative left
-        induction l [] n m p ps = ≈-Eq.refl
+        induction l [] n m p ps = refl
         induction l (r ∷ rs) n m p ps with evalConfig c (D ∙ n) in selected
         -- Select the current alternative because it is the first one where
         -- `config-without-proof c (D ∙ n)` is true
@@ -200,7 +195,7 @@ module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
           rewrite correct fnocContract c n selected ps
           rewrite Nat.+-comm n m
           rewrite Eq.sym (Nat.+-cancelʳ-≡ n zero m p)
-          = ≈-Eq.refl
+          = refl
         -- Impossible case: `config-without-proof c (D ∙ n)` is `false` hence
         -- `incorrect` guarantees `fnoc c D ≢ n` but we have
         -- `fnoc c D ≡ n + 0 = n`
@@ -219,7 +214,7 @@ module Translate {ℓ₂} (S : Setoid Level.zero ℓ₂) where
             ... | yes refl = selected
 
     convert-preserves :
-      ∀ (chc : Choice.Syntax Q Carrier)
+      ∀ (chc : Choice.Syntax Q A)
       → ConfContract (Choice.Syntax.dim chc) conf
       → FnocContract (Choice.Syntax.dim chc) fnoc
         ------------------------------------------
diff --git a/src/Translation/Construct/NestedChoice-to-2Choice.agda b/src/Translation/Construct/NestedChoice-to-2Choice.agda
index cce58c37..5ae4433b 100644
--- a/src/Translation/Construct/NestedChoice-to-2Choice.agda
+++ b/src/Translation/Construct/NestedChoice-to-2Choice.agda
@@ -41,7 +41,7 @@ module Embed
 
   extr = extract constr
 
-  open Choice-to-2Choice.Translate {F} (Eq.setoid (Expression Γ A))
+  open Choice-to-2Choice.Translate {F} (Expression Γ A)
   open Data.IndexedSet (Eq.setoid (V A)) using (_≅_; ≗→≅)
 
   embed : ∀ {i} → NestedChoice i (Expression Γ A) → Expression Γ A
diff --git a/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda b/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda
index de2233ab..f1c6d1a3 100644
--- a/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda
+++ b/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda
@@ -30,7 +30,7 @@ open import Data.String using (String; _<+>_)
 exp : Experiment (Choice.Syntax String ℕ)
 getName exp = "Check N → 2 Choice trans"
 get exp (name ≔ e) = do
- let open Trans (Eq.setoid ℕ) using (convert; show-nested-choice)
+ let open Trans ℕ using (convert; show-nested-choice)
  >         name <+> "=" <+> Choice.show id show-ℕ e
  > phantom name <+> "⇝" <+> show-nested-choice id show-ℕ (convert e)
 
diff --git a/src/Translation/Lang/2ADT-to-2CC.agda b/src/Translation/Lang/2ADT-to-2CC.agda
index 92819f59..b551dfeb 100644
--- a/src/Translation/Lang/2ADT-to-2CC.agda
+++ b/src/Translation/Lang/2ADT-to-2CC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2ADT-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2ADT-to-2CC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Bool as Bool using (if_then_else_)
@@ -12,7 +13,6 @@ open import Data.Product using (proj₂)
 open import Data.List as List using (List; []; _∷_; _ʳ++_)
 import Data.List.Properties as List
 open import Framework.Compiler using (LanguageCompiler)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Framework.Variants using (VariantEncoder)
@@ -27,7 +27,7 @@ open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL)
 open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
diff --git a/src/Translation/Lang/2ADT-to-NADT.agda b/src/Translation/Lang/2ADT-to-NADT.agda
index 9007437f..7bcbcdd6 100644
--- a/src/Translation/Lang/2ADT-to-NADT.agda
+++ b/src/Translation/Lang/2ADT-to-NADT.agda
@@ -5,7 +5,7 @@ open import Framework.Definitions
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2ADT-to-NADT (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2ADT-to-NADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (if_then_else_; true; false)
 import Data.Bool.Properties as Bool
@@ -42,7 +42,7 @@ open NADT using (NADT; NADTL; NADTAsset; NADTChoice)
 import Translation.Construct.2Choice-to-Choice as 2Choice-to-Choice
 open 2Choice-to-Choice.Translate using (convert)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
diff --git a/src/Translation/Lang/2ADT/Rename.agda b/src/Translation/Lang/2ADT/Rename.agda
index 1d7dd6ea..98e9ee79 100644
--- a/src/Translation/Lang/2ADT/Rename.agda
+++ b/src/Translation/Lang/2ADT/Rename.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; atoms)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
@@ -29,7 +29,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 2ADT-map-config : ∀ {D₁ D₂ : 𝔽}
diff --git a/src/Translation/Lang/2CC-to-2ADT.agda b/src/Translation/Lang/2CC-to-2ADT.agda
index 90b706fe..bf6d8054 100644
--- a/src/Translation/Lang/2CC-to-2ADT.agda
+++ b/src/Translation/Lang/2CC-to-2ADT.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2CC-to-2ADT (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2CC-to-2ADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Bool as Bool using (if_then_else_)
@@ -11,7 +12,6 @@ import Data.Bool.Properties as Bool
 open import Data.List as List using (List; []; _∷_; _ʳ++_)
 import Data.List.Properties as List
 open import Framework.Compiler using (LanguageCompiler)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Function using (id)
@@ -25,11 +25,11 @@ open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL)
 open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
-push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → A → List (2ADT Variant D A) → 2ADT Variant D A
+push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → atoms A → List (2ADT Variant D A) → 2ADT Variant D A
 push-down-artifact {A = A} a cs = go cs []
   module push-down-artifact-Implementation where
   go : ∀ {i : Size} {D : 𝔽} → List (2ADT Variant D A) → List (Variant A) → 2ADT Variant D A
@@ -44,7 +44,7 @@ translate (a 2CC.-< cs >-) = push-down-artifact a (List.map translate cs)
 translate (d 2CC.⟨ l , r ⟩) = d ⟨ translate l , translate r ⟩
 
 ⟦push-down-artifact⟧ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
-  → (a : A)
+  → (a : atoms A)
   → (cs : List (2ADT Variant D A))
   → (config : 2ADT.Configuration D)
   → 2ADT.⟦ push-down-artifact a cs ⟧ config ≡ artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) cs)
diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Translation/Lang/2CC-to-NCC.agda
index 4a4a090f..039454f7 100644
--- a/src/Translation/Lang/2CC-to-NCC.agda
+++ b/src/Translation/Lang/2CC-to-NCC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2CC-to-NCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2CC-to-NCC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (true; false; if_then_else_)
 open import Data.Bool.Properties as Bool
@@ -16,7 +17,6 @@ open import Data.Product using () renaming (_,_ to _and_)
 open import Data.Vec as Vec using (Vec; []; _∷_)
 import Data.Vec.Properties as Vec
 open import Framework.Compiler using (LanguageCompiler; _⊕_)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
@@ -32,12 +32,12 @@ open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩)
 
 open import Translation.Lang.NCC.Grow Variant Artifact∈ₛVariant using (growFrom2Compiler)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
 module 2Ary where
-  translate : ∀ {i : Size} {D : 𝔽} {A : 𝔽}
+  translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
     → 2CC D i A
     → NCC (sucs zero) D i A
   translate (a -< cs >-) = a -< List.map translate cs >-
@@ -53,7 +53,7 @@ module 2Ary where
   ... | zero = true
   ... | suc zero = false
 
-  preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔽}
+  preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
     → (expr : 2CC D i A)
     → NCC.⟦ translate expr ⟧ ⊆[ fnoc ] 2CC.⟦ expr ⟧
   preserves-⊆ (a -< cs >-) config =
diff --git a/src/Translation/Lang/2CC/Rename.agda b/src/Translation/Lang/2CC/Rename.agda
index 8ef84316..8785c85d 100644
--- a/src/Translation/Lang/2CC/Rename.agda
+++ b/src/Translation/Lang/2CC/Rename.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; atoms)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
@@ -29,7 +29,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 2CC-map-config : ∀ {D₁ D₂ : 𝔽}
diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Translation/Lang/CCC-to-NCC.agda
index fcbd6d48..ee48e1e7 100644
--- a/src/Translation/Lang/CCC-to-NCC.agda
+++ b/src/Translation/Lang/CCC-to-NCC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.CCC-to-NCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.CCC-to-NCC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Fin as Fin using (Fin)
@@ -15,7 +16,6 @@ open import Data.Product using (_×_; _,_)
 open import Data.Vec as Vec using (Vec; []; _∷_)
 import Data.Vec.Properties as Vec
 open import Framework.Compiler using (LanguageCompiler)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Function using (_∘_; id)
@@ -39,7 +39,7 @@ open import Translation.Lang.NCC.Rename Variant Artifact∈ₛVariant using (NCC
 module NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse = LanguageCompiler (NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse)
 module NCC→NCC {i} {D} n m = LanguageCompiler (NCC→NCC {i} {D} n m)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 module Exact where
@@ -68,7 +68,7 @@ module Exact where
   mutual
     -- A proof that an expression's longest alternative list is at maximum `n`.
     data NumberOfAlternatives≤ {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → CCC D i A → Set where
-      maxArtifact : {i : Size} → {a : A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤ n {↑ i} (a -< cs >-)
+      maxArtifact : {i : Size} → {a : atoms A} → {cs : List (CCC D i A)} → NumberOfAlternatives≤-List n {i} cs → NumberOfAlternatives≤ n {↑ i} (a -< cs >-)
       maxChoice : {i : Size} → {d : D} → {cs : List⁺ (CCC D i A)} → List⁺.length cs ≤ ℕ≥.toℕ n → NumberOfAlternatives≤-List⁺ n {i} cs → NumberOfAlternatives≤ n {↑ i} (d ⟨ cs ⟩)
 
     data NumberOfAlternatives≤-List {D : 𝔽} {A : 𝔸} (n : ℕ≥ 2) : {i : Size} → List (CCC D i A) → Set where
diff --git a/src/Translation/Lang/NADT-to-CCC.agda b/src/Translation/Lang/NADT-to-CCC.agda
index 1ed38e4c..e8106a0b 100644
--- a/src/Translation/Lang/NADT-to-CCC.agda
+++ b/src/Translation/Lang/NADT-to-CCC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_)
+open import Framework.Definitions
 open import Construct.Artifact using () renaming (Syntax to Artifact)
 
-module Translation.Lang.NADT-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.NADT-to-CCC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Construct.Choices
 open import Construct.GrulerArtifacts using (leaf)
@@ -11,7 +12,6 @@ import Data.EqIndexedSet as IndexedSet
 import Data.List.NonEmpty as List⁺
 open import Data.Product using (proj₂)
 open import Framework.Compiler using (LanguageCompiler)
-open import Framework.Definitions
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Framework.Variants using (VariantEncoder)
diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Translation/Lang/NCC-to-2CC.agda
index 9ddb824b..a50ec8fe 100644
--- a/src/Translation/Lang/NCC-to-2CC.agda
+++ b/src/Translation/Lang/NCC-to-2CC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.NCC-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.NCC-to-2CC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (true; false; if_then_else_)
 open import Data.Bool.Properties as Bool
@@ -16,7 +17,6 @@ open import Data.Product using (_×_) renaming (_,_ to _and_)
 open import Data.Vec as Vec using (Vec; []; _∷_)
 import Data.Vec.Properties as Vec
 open import Framework.Compiler using (LanguageCompiler; _⊕_)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
@@ -32,7 +32,7 @@ open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
 open import Framework.Annotation.IndexedDimension
 open import Translation.Lang.NCC.NCC-to-NCC Variant Artifact∈ₛVariant using (NCC→NCC)
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
@@ -85,7 +85,7 @@ module 2Ary where
       NCC.⟦ d ⟨ l ∷ r ∷ [] ⟩ ⟧ (fnoc config)
     ∎
     where
-    lemma : ∀ {A : 𝔸} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (fnoc config d)
+    lemma : ∀ {A : Set} {a b : A} → (if config d then a else b) ≡ Vec.lookup (a ∷ b ∷ []) (fnoc config d)
     lemma with config d
     ... | true = refl
     ... | false = refl
@@ -124,7 +124,7 @@ module 2Ary where
       2CC.⟦ translate (d ⟨ l ∷ r ∷ [] ⟩) ⟧ (conf config)
     ∎
     where
-    lemma : {A : 𝔸} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if conf config d then a else b)
+    lemma : {A : Set} → {a b : A} → Vec.lookup (a ∷ b ∷ []) (config d) ≡ (if conf config d then a else b)
     lemma with config d
     ... | zero = refl
     ... | suc zero = refl
diff --git a/src/Translation/Lang/NCC-to-CCC.agda b/src/Translation/Lang/NCC-to-CCC.agda
index 4dc8674d..b1a19c32 100644
--- a/src/Translation/Lang/NCC-to-CCC.agda
+++ b/src/Translation/Lang/NCC-to-CCC.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_; cons)
+open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.NCC-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.NCC-to-CCC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Fin as Fin using (Fin)
@@ -14,7 +15,6 @@ open import Data.Product using (_,_)
 open import Data.Vec as Vec using (Vec; []; _∷_)
 import Data.Vec.Properties as Vec
 open import Framework.Compiler using (LanguageCompiler)
-open import Framework.Definitions using (𝔸; 𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Framework.Relation.Function using (from; to)
 open import Relation.Binary.PropositionalEquality as Eq using (refl)
@@ -29,7 +29,7 @@ open import Lang.All.Generic Variant Artifact∈ₛVariant
 open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩)
 open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
-artifact : ∀ {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
diff --git a/src/Translation/Lang/NCC/Grow.agda b/src/Translation/Lang/NCC/Grow.agda
index aac6dd89..e2e768c2 100644
--- a/src/Translation/Lang/NCC/Grow.agda
+++ b/src/Translation/Lang/NCC/Grow.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; atoms)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
@@ -39,7 +39,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
-artifact : {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 -- Increasing the arity is straightforward. We have to duplicate one element (we choose the last one to be consistent with the saturation semantic of `CCC`, see `find-or-last`) until the arity difference is zero.
diff --git a/src/Translation/Lang/NCC/Rename.agda b/src/Translation/Lang/NCC/Rename.agda
index 8846250a..d831d835 100644
--- a/src/Translation/Lang/NCC/Rename.agda
+++ b/src/Translation/Lang/NCC/Rename.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; atoms)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
@@ -38,7 +38,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
-artifact : {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 NCC-map-config : ∀ {D₁ D₂ : Set}
diff --git a/src/Translation/Lang/NCC/ShrinkTo2.agda b/src/Translation/Lang/NCC/ShrinkTo2.agda
index a4bb1360..a23b0bac 100644
--- a/src/Translation/Lang/NCC/ShrinkTo2.agda
+++ b/src/Translation/Lang/NCC/ShrinkTo2.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; atoms)
 open import Framework.Construct using (_∈ₛ_; cons)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
@@ -44,7 +44,7 @@ open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
 
-artifact : {A : 𝔸} → A → List (Variant A) → Variant A
+artifact : {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 -- To simplify the implementation and the proof, we constrain the translation to result in 2-ary `NCC` expressions.
diff --git a/src/Translation/Lang/OC-to-2CC.lagda.md b/src/Translation/Lang/OC-to-2CC.lagda.md
index e02a0f04..50658804 100644
--- a/src/Translation/Lang/OC-to-2CC.lagda.md
+++ b/src/Translation/Lang/OC-to-2CC.lagda.md
@@ -39,7 +39,7 @@ open 2CC renaming (_-<_>- to Artifact₂; ⟦_⟧ to ⟦_⟧₂)
 
 open import Data.EqIndexedSet
 
-Artifactᵥ : ∀ {A} → A → List (Rose ∞ A) → Rose ∞ A
+Artifactᵥ : ∀ {A} → atoms A → List (Rose ∞ A) → Rose ∞ A
 Artifactᵥ a cs = rose (a At.-< cs >-)
 
 open import Util.AuxProofs using (id≗toList∘fromList)
@@ -84,7 +84,7 @@ record Zip (work : ℕ) (i : Size) (A : 𝔸) : Set where
   -- However, in Agda, using ⦇ and ⦈ is forbidden.
   constructor _-<_≪_>- --\T
   field
-    parent    : A
+    parent    : atoms A
     siblingsL : List (2CC F ∞ A)
     siblingsR : Vec (OC F i A) work
 open Zip public
@@ -119,7 +119,7 @@ data _⊢_⟶ₒ_ where
   T-done :
     ∀ {i  : Size}
       {A  : 𝔸}
-      {a  : A}
+      {a  : atoms A}
       {ls : List (2CC F ∞ A)}
       --------------------------------------
     → i ⊢ a -< ls ≪ [] >- ⟶ₒ Artifact₂ a ls
@@ -133,7 +133,7 @@ data _⊢_⟶ₒ_ where
     ∀ {i   : Size  }
       {n   : ℕ    }
       {A   : 𝔸}
-      {a b : A     }
+      {a b : atoms A}
       {ls  : List (2CC F ∞    A)  }
       {es  : List (OC F    i  A)  }
       {rs  : Vec  (OC F (↑ i) A) n}
@@ -155,7 +155,7 @@ data _⊢_⟶ₒ_ where
     ∀ {i   : Size  }
       {n   : ℕ     }
       {A   : 𝔸     }
-      {a   : A     }
+      {a   : atoms A}
       {O   : Option}
       {e   : OC F i A}
       {ls  : List (2CC F    ∞  A)  }
@@ -177,7 +177,7 @@ data _⟶_ where
   T-root :
     ∀ {i  : Size}
       {A  : 𝔸}
-      {a  : A}
+      {a  : atoms A}
       {es : List (OC F i A)}
       {e  : 2CC F ∞ A}
     → i ⊢ a -< [] ≪ (fromList es) >- ⟶ₒ e
@@ -297,7 +297,7 @@ Agda fails to see that "preserves" directly unpacks this constructor again and c
 Since Agda fails here, we have to avoid the re- and unpacking below T-root and thus introduce this auxiliary function.
 -}
 preserves-without-T-root :
-  ∀ {i} {A} {b : A} {es : List (OC F i A)} {e : 2CC F ∞ A}
+  ∀ {i} {A} {b : atoms A} {es : List (OC F i A)} {e : 2CC F ∞ A}
   → (c : OC.Configuration F)
   → (⟶e : i ⊢ b -< [] ≪ fromList es >- ⟶ₒ e)
     ------------------------------------------
@@ -323,7 +323,7 @@ The concrete formulas are a bit convoluted here because they are partially norma
 -}
 preservesₒ-artifact :
   ∀ {i} {A} {c}
-    {b   : A}
+    {b   : atoms A}
     {ls  : List (2CC F ∞ A)}
     {es  : List (OC F i A)}
     {e   : 2CC F ∞ A}
@@ -365,7 +365,7 @@ So we show Agda that ⟦_⟧ₒ never does so.
 This theorem has no real meaning and is rather a technical necessity.
 -}
 preservesₒ-option-size :
-  ∀ {n} {i} {A} {c} {a : A} {ls : List (2CC F ∞ A)} {rs : Vec (OC F (↑ i) A) n}
+  ∀ {n} {i} {A} {c} {a : atoms A} {ls : List (2CC F ∞ A)} {rs : Vec (OC F (↑ i) A) n}
   → (e : OC F i A)
     -----------------------------------------------------------------------------------------------------
   →   Artifactᵥ a (map (flip ⟦_⟧₂ c) ls ++ catMaybes (⟦_⟧ₒ {i  } e c ∷ map (flip ⟦_⟧ₒ c) (toList rs)))
diff --git a/src/Translation/Lang/Transitive/2CC-to-CCC.agda b/src/Translation/Lang/Transitive/2CC-to-CCC.agda
index 729bd437..dd82afc2 100644
--- a/src/Translation/Lang/Transitive/2CC-to-CCC.agda
+++ b/src/Translation/Lang/Transitive/2CC-to-CCC.agda
@@ -1,13 +1,13 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_)
+open import Framework.Definitions using (𝔽; 𝕍)
 open import Construct.Artifact using () renaming (Syntax to Artifact)
 
-module Translation.Lang.Transitive.2CC-to-CCC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.Transitive.2CC-to-CCC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Nat using (zero)
 open import Framework.Compiler using (LanguageCompiler; _⊕_)
-open import Framework.Definitions using (𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Size using (Size)
 open import Util.Nat.AtLeast using (sucs)
diff --git a/src/Translation/Lang/Transitive/CCC-to-2CC.agda b/src/Translation/Lang/Transitive/CCC-to-2CC.agda
index 549e8d86..be053153 100644
--- a/src/Translation/Lang/Transitive/CCC-to-2CC.agda
+++ b/src/Translation/Lang/Transitive/CCC-to-2CC.agda
@@ -1,14 +1,14 @@
 {-# OPTIONS --sized-types #-}
 
 open import Framework.Construct using (_∈ₛ_)
+open import Framework.Definitions using (𝔽; 𝕍)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact)
 
-module Translation.Lang.Transitive.CCC-to-2CC (Variant : Set → Set) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.Transitive.CCC-to-2CC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Nat using (ℕ; zero)
 open import Data.Product using (_×_)
 open import Framework.Compiler using (LanguageCompiler; _⊕_)
-open import Framework.Definitions using (𝔽)
 open import Framework.Relation.Expressiveness Variant using (expressiveness-from-compiler; _≽_)
 open import Size using (Size)
 open import Util.Nat.AtLeast using (sucs)
diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md
index 1c1e985d..313216ee 100644
--- a/src/Translation/LanguageMap.lagda.md
+++ b/src/Translation/LanguageMap.lagda.md
@@ -143,6 +143,8 @@ make the changes in the feature model explicit. For theoretical results however,
 it is easier to assume that the set of annotations `F` is infinite, which is
 equivalent to the restriction used here (except if `F` is empty).
 
+A witness of these preconditions can be faund in `Util.String`.
+
 ```agda
 module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f⁻¹∘f≗id : f⁻¹ ∘ f ≗ id) where
   private