diff --git a/src/Lang/2ADT.agda b/src/Lang/ADT.agda
similarity index 67%
rename from src/Lang/2ADT.agda
rename to src/Lang/ADT.agda
index 3ec41c0c..5a391d64 100644
--- a/src/Lang/2ADT.agda
+++ b/src/Lang/ADT.agda
@@ -1,31 +1,31 @@
 open import Framework.Definitions
-module Lang.2ADT where
+module Lang.ADT where
 
 open import Data.Bool using (Bool; if_then_else_)
 open import Framework.VariabilityLanguage
 
-data 2ADT (V : 𝕍) (F : 𝔽) : 𝔼 where
-  leaf   : ∀ {A} → V A → 2ADT V F A
-  _⟨_,_⟩ : ∀ {A} → (D : F) → (l : 2ADT V F A) → (r : 2ADT V F A) → 2ADT V F A
+data ADT (V : 𝕍) (F : 𝔽) : 𝔼 where
+  leaf   : ∀ {A} → V A → ADT V F A
+  _⟨_,_⟩ : ∀ {A} → (D : F) → (l : ADT V F A) → (r : ADT V F A) → ADT V F A
 
 Configuration : (F : 𝔽) → Set
 Configuration F = F → Bool
 
-⟦_⟧ : {V : 𝕍} → {F : 𝔽} → 𝔼-Semantics V (Configuration F) (2ADT V F)
+⟦_⟧ : {V : 𝕍} → {F : 𝔽} → 𝔼-Semantics V (Configuration F) (ADT V F)
 ⟦ leaf v      ⟧ _ = v
 ⟦ D ⟨ l , r ⟩ ⟧ c = if c D
                     then ⟦ l ⟧ c
                     else ⟦ r ⟧ c
 
-2ADTL : (V : 𝕍) → (F : 𝔽) → VariabilityLanguage V
-2ADTL V F = ⟪ 2ADT V F , Configuration F , ⟦_⟧ ⟫
+ADTL : (V : 𝕍) → (F : 𝔽) → VariabilityLanguage V
+ADTL V F = ⟪ ADT V F , Configuration F , ⟦_⟧ ⟫
 
 
 open import Data.String as String using (String; _++_; intersperse)
 open import Data.Product using (_,_)
 open import Show.Lines
 
-pretty : {A : 𝔸} → {V : 𝕍} → {F : 𝔽} → (V A → String) → (F → String) → 2ADT V F A → Lines
+pretty : {A : 𝔸} → {V : 𝕍} → {F : 𝔽} → (V A → String) → (F → String) → ADT V F A → Lines
 pretty pretty-variant show-F (leaf v) = > pretty-variant v
 pretty pretty-variant show-F (D ⟨ l , r ⟩) = do
   > show-F D ++ "⟨"
diff --git a/src/Lang/2ADT/Path.agda b/src/Lang/ADT/Path.agda
similarity index 91%
rename from src/Lang/2ADT/Path.agda
rename to src/Lang/ADT/Path.agda
index 2d2f3d8f..d22aad6f 100644
--- a/src/Lang/2ADT/Path.agda
+++ b/src/Lang/ADT/Path.agda
@@ -1,6 +1,6 @@
 open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼)
 open import Relation.Binary using (DecidableEquality; Rel)
-module Lang.2ADT.Path
+module Lang.ADT.Path
   (F : 𝔽)
   (V : 𝕍)
   (_==_ : DecidableEquality F)
@@ -26,7 +26,7 @@ open Eq.≡-Reasoning
 
 open import Framework.VariabilityLanguage
 open import Util.Suffix using (_endswith_)
-open import Lang.2ADT using (2ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
+open import Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
 
 -- A selection of a feature matches it to a boolean value.
 record Selection : Set where
@@ -36,7 +36,7 @@ record Selection : Set where
     value : Bool
 open Selection public
 
--- A list of selection which denotes a path from the root of a 2ADT to a leaf node.
+-- A list of selection which denotes a path from the root of a ADT to a leaf node.
 Path : Set
 Path = List Selection
 
@@ -123,17 +123,17 @@ Note: The symmetry between the rules walk-left and walk-right causes many
       However, we cannot merge the rules into a single rule
       because we have to recurse on either the left or right alternative (not both).
 -}
-data _starts-at_ : ∀ {A} → (p : Path) → (e : 2ADT V F A) → Set where
+data _starts-at_ : ∀ {A} → (p : Path) → (e : ADT V F A) → Set where
   tleaf : ∀ {A} {v : V A}
       ------------------
     → [] starts-at (leaf v)
 
-  walk-left : ∀ {A} {D : F} {l r : 2ADT V F A} {pl : Path}
+  walk-left : ∀ {A} {D : F} {l r : ADT V F A} {pl : Path}
     → pl starts-at l
       -------------------------------------
     → ((D ↣ true) ∷ pl) starts-at (D ⟨ l , r ⟩)
 
-  walk-right : ∀ {A} {D : F} {l r : 2ADT V F A} {pr : Path}
+  walk-right : ∀ {A} {D : F} {l r : ADT V F A} {pr : Path}
     → pr starts-at r
       --------------------------------------
     → ((D ↣ false) ∷ pr) starts-at (D ⟨ l , r ⟩)
@@ -142,14 +142,14 @@ data _starts-at_ : ∀ {A} → (p : Path) → (e : 2ADT V F A) → Set where
 An expression does not contain a feature name
 if all paths do not contain that feature name.
 -}
-_∉'_ : ∀{A} → F → 2ADT V F A → Set
+_∉'_ : ∀{A} → F → ADT V F A → Set
 D ∉' e = ∀ (p : Path) → p starts-at e → D ∉ p
 
 {-
 A path serves as a configuration for an expression e
 if it starts at that expression and ends at a leaf.
 -}
-record PathConfig {A} (e : 2ADT V F A) : Set where
+record PathConfig {A} (e : ADT V F A) : Set where
   constructor _is-valid_
   field
     path : Path
@@ -157,12 +157,12 @@ record PathConfig {A} (e : 2ADT V F A) : Set where
 open PathConfig public
 
 {-
-Alternative semantics of 2ADTs by walking a path.
+Alternative semantics of ADTs by walking a path.
 This walk may be illegal by choosing different alternatives for the same choice within a path.
 For example in D ⟨ D ⟨ 1 , dead ⟩ , 2 ⟩ we can reach 'dead' via (D ↣ true ∷ D ↣ false ∷ []).
 However, walking like this is fine as long as the path is unique as we will later prove.
 -}
-walk : ∀ {A} → (e : 2ADT V F A) → PathConfig e → V A
+walk : ∀ {A} → (e : ADT V F A) → PathConfig e → V A
 walk (leaf v) ([] is-valid tleaf) = v
 walk (D ⟨ l , _ ⟩) ((.(D ↣ true ) ∷ pl) is-valid walk-left  t) = walk l (pl is-valid t)
 walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r (pr is-valid t)
@@ -171,7 +171,7 @@ walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r
 An expression a is a sub-expression of b
 iff all valid paths from a lead to paths from b.
 -}
-_subexprof_ : ∀ {A} → 2ADT V F A → 2ADT V F A → Set
+_subexprof_ : ∀ {A} → ADT V F A → ADT V F A → Set
 a subexprof b = ∀ (pa : Path) → pa starts-at a → ∃[ pb ] ((pb starts-at b) × (pb endswith pa))
 
 {-
diff --git a/src/Lang/All/Generic.agda b/src/Lang/All/Generic.agda
index 91e710db..c73c167f 100644
--- a/src/Lang/All/Generic.agda
+++ b/src/Lang/All/Generic.agda
@@ -24,8 +24,8 @@ module 2CC where
 module NADT where
   open import Lang.NADT renaming (NADTVL to NADTL) public
 
-module 2ADT where
-  open import Lang.2ADT public
+module ADT where
+  open import Lang.ADT public
 
 module OC where
   open import Lang.OC public
diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda
index 90fae295..1d686614 100644
--- a/src/Test/Experiments/RoundTrip.agda
+++ b/src/Test/Experiments/RoundTrip.agda
@@ -84,12 +84,12 @@ get     round-trip ex@(name ≔ ccc) = do
   overwrite-alignment-with Center
     (boxed (6 + width pretty-ccc) "" pretty-ccc)
 
-  ncc         ← translate ccc         "NCC"         CCC→NCC-Exact                                               (NCC.Pretty.pretty id)
-  ncc2        ← compile   ncc         "NCC"         (shrinkTo2Compiler ⌈ ccc ⌉)                                 (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  2cc         ← compile   ncc2        "2CC"         NCC-2→2CC                                                   (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  2adt        ← compile   2cc         "2ADT"        2CC→2ADT                                                    (2ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  variantList ← compile   2adt        "VariantList" (2ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id))
-  ccc'        ← compile   variantList "CCC"         (VariantList→CCC "default feature")                         (CCC.pretty id)
+  ncc         ← translate ccc         "NCC"         CCC→NCC-Exact                                              (NCC.Pretty.pretty id)
+  ncc2        ← compile   ncc         "NCC"         (shrinkTo2Compiler ⌈ ccc ⌉)                                (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  2cc         ← compile   ncc2        "2CC"         NCC-2→2CC                                                  (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  adt         ← compile   2cc         "ADT"         2CC→ADT                                                    (ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  variantList ← compile   adt         "VariantList" (ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id))
+  ccc'        ← compile   variantList "CCC"         (VariantList→CCC "default feature")                        (CCC.pretty id)
   linebreak
 
 
diff --git a/src/Translation/Lang/2CC-to-2ADT.agda b/src/Translation/Lang/2CC-to-ADT.agda
similarity index 53%
rename from src/Translation/Lang/2CC-to-2ADT.agda
rename to src/Translation/Lang/2CC-to-ADT.agda
index bf6d8054..132b7dd8 100644
--- a/src/Translation/Lang/2CC-to-2ADT.agda
+++ b/src/Translation/Lang/2CC-to-ADT.agda
@@ -4,7 +4,7 @@ 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 : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2CC-to-ADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Bool as Bool using (if_then_else_)
@@ -23,87 +23,87 @@ open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[])
 
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL)
-open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
+open ADT using (ADT; ADTL; leaf; _⟨_,_⟩)
 
 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 : 𝔸} → atoms A → List (2ADT Variant D A) → 2ADT Variant D A
+push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → atoms A → List (ADT Variant D A) → ADT 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
+  go : ∀ {i : Size} {D : 𝔽} → List (ADT Variant D A) → List (Variant A) → ADT Variant D A
   go [] vs = leaf (artifact a (List.reverse vs))
   go (leaf v ∷ cs) vs = go cs (v ∷ vs)
   go (d ⟨ c₁ , c₂ ⟩ ∷ cs) vs = d ⟨ go (c₁ ∷ cs) vs , go (c₂ ∷ cs) vs ⟩
 
 translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → 2CC D i A
-  → 2ADT Variant D A
+  → ADT Variant D A
 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 : 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)
+  → (cs : List (ADT Variant D A))
+  → (config : ADT.Configuration D)
+  → ADT.⟦ push-down-artifact a cs ⟧ config ≡ artifact a (List.map (λ e → ADT.⟦ e ⟧ config) cs)
 ⟦push-down-artifact⟧ {D = D} {A = A} a cs config = go' cs []
   where
   open push-down-artifact-Implementation
 
   go' : ∀ {i : Size}
-    → (cs' : List (2ADT Variant D A))
+    → (cs' : List (ADT Variant D A))
     → (vs : List (Variant A))
-    → 2ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+    → ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) cs')
   go' [] vs = Eq.sym (Eq.cong₂ artifact refl (Eq.trans (List.ʳ++-defn vs) (List.++-identityʳ (List.reverse vs))))
   go' (leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ artifact refl (List.ʳ++-++ List.[ v ] {ys = vs}))
   go' ((d ⟨ c₁ , c₂ ⟩) ∷ cs') vs =
-      2ADT.⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config
+      ADT.⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config
     ≡⟨⟩
       (if config d
-        then 2ADT.⟦ go a cs (c₁ ∷ cs') vs ⟧ config
-        else 2ADT.⟦ go a cs (c₂ ∷ cs') vs ⟧ config)
+        then ADT.⟦ go a cs (c₁ ∷ cs') vs ⟧ config
+        else ADT.⟦ go a cs (c₂ ∷ cs') vs ⟧ config)
     ≡⟨ Eq.cong₂ (if config d then_else_) (go' (c₁ ∷ cs') vs) (go' (c₂ ∷ cs') vs) ⟩
       (if config d
-        then artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₁ ∷ cs'))
-        else artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₂ ∷ cs')))
-    ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩
-      artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs'))
+        then artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₁ ∷ cs'))
+        else artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₂ ∷ cs')))
+    ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩
+      artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs'))
     ≡⟨⟩
-      artifact a (vs ʳ++ 2ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
-    ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → 2ADT.⟦ e ⟧ config) (config d)) refl)) ⟩
-      artifact a (vs ʳ++ (if config d then 2ADT.⟦ c₁ ⟧ config else 2ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+      artifact a (vs ʳ++ ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
+    ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → ADT.⟦ e ⟧ config) (config d)) refl)) ⟩
+      artifact a (vs ʳ++ (if config d then ADT.⟦ c₁ ⟧ config else ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
     ≡⟨⟩
-      artifact a (vs ʳ++ 2ADT.⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+      artifact a (vs ʳ++ ADT.⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
     ≡⟨⟩
-      artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (d ⟨ c₁ , c₂ ⟩ ∷ cs'))
+      artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (d ⟨ c₁ , c₂ ⟩ ∷ cs'))
     ∎
 
 preserves-≗ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → (expr : 2CC D i A)
-  → 2ADT.⟦ translate expr ⟧ ≗ 2CC.⟦ expr ⟧
+  → ADT.⟦ translate expr ⟧ ≗ 2CC.⟦ expr ⟧
 preserves-≗ {D = D} {A = A} (a 2CC.-< cs >-) config =
-    2ADT.⟦ translate (a 2CC.-< cs >-) ⟧ config
+    ADT.⟦ translate (a 2CC.-< cs >-) ⟧ config
   ≡⟨⟩
-    2ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config
+    ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config
   ≡⟨ ⟦push-down-artifact⟧ a (List.map translate cs) config ⟩
-    artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) (List.map translate cs))
+    artifact a (List.map (λ e → ADT.⟦ e ⟧ config) (List.map translate cs))
   ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩
-    artifact a (List.map (λ e → 2ADT.⟦ translate e ⟧ config) cs)
+    artifact a (List.map (λ e → ADT.⟦ translate e ⟧ config) cs)
   ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-≗ e config) cs) ⟩
     artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) cs)
   ≡⟨⟩
     2CC.⟦ a 2CC.-< cs >- ⟧ config
   ∎
 preserves-≗ (d 2CC.⟨ l , r ⟩) config =
-    2ADT.⟦ translate (d 2CC.⟨ l , r ⟩) ⟧ config
+    ADT.⟦ translate (d 2CC.⟨ l , r ⟩) ⟧ config
   ≡⟨⟩
-    2ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config
+    ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config
   ≡⟨⟩
-    (if config d then 2ADT.⟦ translate l ⟧ config else 2ADT.⟦ translate r ⟧ config)
-  ≡˘⟨ Bool.push-function-into-if (λ e → 2ADT.⟦ translate e ⟧ config) (config d) ⟩
-    2ADT.⟦ translate (if config d then l else r) ⟧ config
+    (if config d then ADT.⟦ translate l ⟧ config else ADT.⟦ translate r ⟧ config)
+  ≡˘⟨ Bool.push-function-into-if (λ e → ADT.⟦ translate e ⟧ config) (config d) ⟩
+    ADT.⟦ translate (if config d then l else r) ⟧ config
   ≡⟨ preserves-≗ (if config d then l else r) config ⟩
     2CC.⟦ if config d then l else r ⟧ config
   ≡⟨⟩
@@ -112,14 +112,14 @@ preserves-≗ (d 2CC.⟨ l , r ⟩) config =
 
 preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → (expr : 2CC D i A)
-  → 2ADT.⟦ translate expr ⟧ ≅[ id ][ id ] 2CC.⟦ expr ⟧
+  → ADT.⟦ translate expr ⟧ ≅[ id ][ id ] 2CC.⟦ expr ⟧
 preserves expr = ≗→≅[] (preserves-≗ expr)
 
-2CC→2ADT : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (2ADTL Variant D)
-2CC→2ADT .LanguageCompiler.compile = translate
-2CC→2ADT .LanguageCompiler.config-compiler expr .to = id
-2CC→2ADT .LanguageCompiler.config-compiler expr .from = id
-2CC→2ADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
+2CC→ADT : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (ADTL Variant D)
+2CC→ADT .LanguageCompiler.compile = translate
+2CC→ADT .LanguageCompiler.config-compiler expr .to = id
+2CC→ADT .LanguageCompiler.config-compiler expr .from = id
+2CC→ADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
 
-2ADT≽2CC : ∀ {D : 𝔽} → 2ADTL Variant D ≽ 2CCL D
-2ADT≽2CC = expressiveness-from-compiler 2CC→2ADT
+ADT≽2CC : ∀ {D : 𝔽} → ADTL Variant D ≽ 2CCL D
+ADT≽2CC = expressiveness-from-compiler 2CC→ADT
diff --git a/src/Translation/Lang/2ADT-to-2CC.agda b/src/Translation/Lang/ADT-to-2CC.agda
similarity index 61%
rename from src/Translation/Lang/2ADT-to-2CC.agda
rename to src/Translation/Lang/ADT-to-2CC.agda
index b551dfeb..60c68416 100644
--- a/src/Translation/Lang/2ADT-to-2CC.agda
+++ b/src/Translation/Lang/ADT-to-2CC.agda
@@ -4,7 +4,7 @@ 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 : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.ADT-to-2CC (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Bool as Bool using (if_then_else_)
@@ -25,27 +25,27 @@ open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[])
 
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL)
-open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
+open ADT using (ADT; ADTL; leaf; _⟨_,_⟩)
 
 artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
-translate : ∀ {F : 𝔽} {A : 𝔸} → VariantEncoder Variant (2CCL F) → 2ADT Variant F A → 2CC F ∞ A
-translate Variant→2CC (2ADT.leaf v) = LanguageCompiler.compile Variant→2CC v
-translate Variant→2CC (f 2ADT.⟨ l , r ⟩) = f 2CC.⟨ translate Variant→2CC l , translate Variant→2CC r ⟩
+translate : ∀ {F : 𝔽} {A : 𝔸} → VariantEncoder Variant (2CCL F) → ADT Variant F A → 2CC F ∞ A
+translate Variant→2CC (ADT.leaf v) = LanguageCompiler.compile Variant→2CC v
+translate Variant→2CC (f ADT.⟨ l , r ⟩) = f 2CC.⟨ translate Variant→2CC l , translate Variant→2CC r ⟩
 
-preserves-≗ : ∀ {F : 𝔽} {A : 𝔸} → (Variant→2CC : VariantEncoder Variant (2CCL F)) → (expr : 2ADT Variant F A) → 2CC.⟦ translate Variant→2CC expr ⟧ ≗ 2ADT.⟦ expr ⟧
-preserves-≗ {A = A} Variant→2CC (2ADT.leaf v) config =
+preserves-≗ : ∀ {F : 𝔽} {A : 𝔸} → (Variant→2CC : VariantEncoder Variant (2CCL F)) → (expr : ADT Variant F A) → 2CC.⟦ translate Variant→2CC expr ⟧ ≗ ADT.⟦ expr ⟧
+preserves-≗ {A = A} Variant→2CC (ADT.leaf v) config =
     2CC.⟦ translate Variant→2CC (leaf v) ⟧ config
   ≡⟨⟩
     2CC.⟦ LanguageCompiler.compile Variant→2CC v ⟧ config
   ≡⟨ proj₂ (LanguageCompiler.preserves Variant→2CC v) config ⟩
     v
   ≡⟨⟩
-    2ADT.⟦ leaf {Variant} v ⟧ config
+    ADT.⟦ leaf {Variant} v ⟧ config
   ∎
-preserves-≗ Variant→2CC (f 2ADT.⟨ l , r ⟩) config =
+preserves-≗ Variant→2CC (f ADT.⟨ l , r ⟩) config =
     2CC.⟦ translate Variant→2CC (f ⟨ l , r ⟩) ⟧ config
   ≡⟨⟩
     2CC.⟦ f 2CC.⟨ translate Variant→2CC l , translate Variant→2CC r ⟩ ⟧ config
@@ -54,19 +54,19 @@ preserves-≗ Variant→2CC (f 2ADT.⟨ l , r ⟩) config =
   ≡⟨ Bool.push-function-into-if (λ e → 2CC.⟦ e ⟧ config) (config f) ⟩
     (if config f then 2CC.⟦ translate Variant→2CC l ⟧ config else 2CC.⟦ translate Variant→2CC r ⟧ config)
   ≡⟨ Eq.cong₂ (if config f then_else_) (preserves-≗ Variant→2CC l config) (preserves-≗ Variant→2CC r config) ⟩
-    (if config f then 2ADT.⟦ l ⟧ config else 2ADT.⟦ r ⟧ config)
+    (if config f then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config)
   ≡⟨⟩
-    2ADT.⟦ f ⟨ l , r ⟩ ⟧ config
+    ADT.⟦ f ⟨ l , r ⟩ ⟧ config
   ∎
 
-preserves : ∀ {F : 𝔽} {A : 𝔸} → (Variant→2CC : VariantEncoder Variant (2CCL F)) → (expr : 2ADT Variant F A) → 2CC.⟦ translate Variant→2CC expr ⟧ ≅[ id ][ id ] 2ADT.⟦ expr ⟧
+preserves : ∀ {F : 𝔽} {A : 𝔸} → (Variant→2CC : VariantEncoder Variant (2CCL F)) → (expr : ADT Variant F A) → 2CC.⟦ translate Variant→2CC expr ⟧ ≅[ id ][ id ] ADT.⟦ expr ⟧
 preserves Variant→2CC expr = ≗→≅[] (preserves-≗ Variant→2CC expr)
 
-2ADT→2CC : ∀ {F : 𝔽} → VariantEncoder Variant (2CCL F) → LanguageCompiler (2ADTL Variant F) (2CCL F)
-2ADT→2CC Variant→2CC .LanguageCompiler.compile = translate Variant→2CC
-2ADT→2CC Variant→2CC .LanguageCompiler.config-compiler expr .to = id
-2ADT→2CC Variant→2CC .LanguageCompiler.config-compiler expr .from = id
-2ADT→2CC Variant→2CC .LanguageCompiler.preserves expr = ≅[]-sym (preserves Variant→2CC expr)
+ADT→2CC : ∀ {F : 𝔽} → VariantEncoder Variant (2CCL F) → LanguageCompiler (ADTL Variant F) (2CCL F)
+ADT→2CC Variant→2CC .LanguageCompiler.compile = translate Variant→2CC
+ADT→2CC Variant→2CC .LanguageCompiler.config-compiler expr .to = id
+ADT→2CC Variant→2CC .LanguageCompiler.config-compiler expr .from = id
+ADT→2CC Variant→2CC .LanguageCompiler.preserves expr = ≅[]-sym (preserves Variant→2CC expr)
 
-2CC≽2ADT : ∀ {F : 𝔽} → VariantEncoder Variant (2CCL F) → 2CCL F ≽ 2ADTL Variant F
-2CC≽2ADT Variant→2CC = expressiveness-from-compiler (2ADT→2CC Variant→2CC)
+2CC≽ADT : ∀ {F : 𝔽} → VariantEncoder Variant (2CCL F) → 2CCL F ≽ ADTL Variant F
+2CC≽ADT Variant→2CC = expressiveness-from-compiler (ADT→2CC Variant→2CC)
diff --git a/src/Translation/Lang/2ADT-to-NADT.agda b/src/Translation/Lang/ADT-to-NADT.agda
similarity index 66%
rename from src/Translation/Lang/2ADT-to-NADT.agda
rename to src/Translation/Lang/ADT-to-NADT.agda
index 7bcbcdd6..6c90aa55 100644
--- a/src/Translation/Lang/2ADT-to-NADT.agda
+++ b/src/Translation/Lang/ADT-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 : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.ADT-to-NADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (if_then_else_; true; false)
 import Data.Bool.Properties as Bool
@@ -35,7 +35,7 @@ open import Framework.Variants using (GrulerVariant)
 open import Construct.GrulerArtifacts using (leaf)
 
 open import Lang.All.Generic Variant Artifact∈ₛVariant
-open 2ADT using (2ADT; 2ADTL; _⟨_,_⟩)
+open ADT using (ADT; ADTL; _⟨_,_⟩)
 open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩)
 open NADT using (NADT; NADTL; NADTAsset; NADTChoice)
 
@@ -46,23 +46,23 @@ artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
-translate : ∀ {F : 𝔽} {A : 𝔸} → 2ADT Variant F A → NADT Variant F ∞ A
-translate (2ADT.leaf a) = NADTAsset (leaf a)
-translate {F = F} {A = A} (f 2ADT.⟨ l , r ⟩) = NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩)
+translate : ∀ {F : 𝔽} {A : 𝔸} → ADT Variant F A → NADT Variant F ∞ A
+translate (ADT.leaf a) = NADTAsset (leaf a)
+translate {F = F} {A = A} (f ADT.⟨ l , r ⟩) = NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩)
 
-conf : ∀ {F : 𝔽} → 2ADT.Configuration F → CCC.Configuration F
+conf : ∀ {F : 𝔽} → ADT.Configuration F → CCC.Configuration F
 conf config f with config f
 ... | true = 0
 ... | false = 1
 
-fnoc : ∀ {F : 𝔽} → CCC.Configuration F → 2ADT.Configuration F
+fnoc : ∀ {F : 𝔽} → CCC.Configuration F → ADT.Configuration F
 fnoc config f with config f
 ... | zero = true
 ... | suc _ = false
 
-preserves-⊆ : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT Variant F A) → NADT.⟦ translate expr ⟧ ⊆[ fnoc ] 2ADT.⟦ expr ⟧
-preserves-⊆ (2ADT.leaf v) config = refl
-preserves-⊆ (f 2ADT.⟨ l , r ⟩) config =
+preserves-⊆ : ∀ {F : 𝔽} {A : 𝔸} → (expr : ADT Variant F A) → NADT.⟦ translate expr ⟧ ⊆[ fnoc ] ADT.⟦ expr ⟧
+preserves-⊆ (ADT.leaf v) config = refl
+preserves-⊆ (f ADT.⟨ l , r ⟩) config =
     NADT.⟦ NADTChoice (f Choice.⟨ translate l ∷ translate r ∷ [] ⟩) ⟧ config
   ≡⟨⟩
     NADT.⟦ List.find-or-last (config f) (translate l ∷ translate r ∷ []) ⟧ config
@@ -71,9 +71,9 @@ preserves-⊆ (f 2ADT.⟨ l , r ⟩) config =
   ≡⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ config) (fnoc config f) ⟩
     (if fnoc config f then NADT.⟦ translate l ⟧ config else NADT.⟦ translate r ⟧ config)
   ≡⟨ Eq.cong₂ (if fnoc config f then_else_) (preserves-⊆ l config) (preserves-⊆ r config) ⟩
-    (if fnoc config f then 2ADT.⟦ l ⟧ (fnoc config) else 2ADT.⟦ r ⟧ (fnoc config))
+    (if fnoc config f then ADT.⟦ l ⟧ (fnoc config) else ADT.⟦ r ⟧ (fnoc config))
   ≡⟨⟩
-    2ADT.⟦ f ⟨ l , r ⟩ ⟧ (fnoc config)
+    ADT.⟦ f ⟨ l , r ⟩ ⟧ (fnoc config)
   ∎
   where
   lemma : List.find-or-last (config f) (translate l ∷ translate r ∷ []) ≡ (if fnoc config f then translate l else translate r)
@@ -81,12 +81,12 @@ preserves-⊆ (f 2ADT.⟨ l , r ⟩) config =
   ... | zero = refl
   ... | suc _ = refl
 
-preserves-⊇ : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT Variant F A) → 2ADT.⟦ expr ⟧ ⊆[ conf ] NADT.⟦ translate expr ⟧
-preserves-⊇ (2ADT.leaf v) config = refl
+preserves-⊇ : ∀ {F : 𝔽} {A : 𝔸} → (expr : ADT Variant F A) → ADT.⟦ expr ⟧ ⊆[ conf ] NADT.⟦ translate expr ⟧
+preserves-⊇ (ADT.leaf v) config = refl
 preserves-⊇ (f ⟨ l , r ⟩) config =
-    2ADT.⟦ f ⟨ l , r ⟩ ⟧ config
+    ADT.⟦ f ⟨ l , r ⟩ ⟧ config
   ≡⟨⟩
-    (if config f then 2ADT.⟦ l ⟧ config else 2ADT.⟦ r ⟧ config)
+    (if config f then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config)
   ≡⟨ Eq.cong₂ (if config f then_else_) (preserves-⊇ l config) (preserves-⊇ r config) ⟩
     (if config f then NADT.⟦ translate l ⟧ (conf config) else NADT.⟦ translate r ⟧ (conf config))
   ≡˘⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ (conf config)) (config f) ⟩
@@ -102,14 +102,14 @@ preserves-⊇ (f ⟨ l , r ⟩) config =
   ... | true = refl
   ... | false = refl
 
-preserves : ∀ {F : 𝔽} {A : 𝔸} → (expr : 2ADT Variant F A) → NADT.⟦ translate expr ⟧ ≅[ fnoc ][ conf ] 2ADT.⟦ expr ⟧
+preserves : ∀ {F : 𝔽} {A : 𝔸} → (expr : ADT Variant F A) → NADT.⟦ translate expr ⟧ ≅[ fnoc ][ conf ] ADT.⟦ expr ⟧
 preserves expr = preserves-⊆ expr and preserves-⊇ expr
 
-2ADT→NADT : ∀ {i : Size} {F : 𝔽} → LanguageCompiler (2ADTL Variant F) (NADTL Variant F)
-2ADT→NADT .LanguageCompiler.compile = translate
-2ADT→NADT .LanguageCompiler.config-compiler expr .to = conf
-2ADT→NADT .LanguageCompiler.config-compiler expr .from = fnoc
-2ADT→NADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
+ADT→NADT : ∀ {i : Size} {F : 𝔽} → LanguageCompiler (ADTL Variant F) (NADTL Variant F)
+ADT→NADT .LanguageCompiler.compile = translate
+ADT→NADT .LanguageCompiler.config-compiler expr .to = conf
+ADT→NADT .LanguageCompiler.config-compiler expr .from = fnoc
+ADT→NADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
 
-NADT≽2ADT : ∀ {F : 𝔽} → NADTL Variant F ≽ 2ADTL Variant F
-NADT≽2ADT = expressiveness-from-compiler 2ADT→NADT
+NADT≽ADT : ∀ {F : 𝔽} → NADTL Variant F ≽ ADTL Variant F
+NADT≽ADT = expressiveness-from-compiler ADT→NADT
diff --git a/src/Translation/Lang/2ADT-to-VariantList.agda b/src/Translation/Lang/ADT-to-VariantList.agda
similarity index 78%
rename from src/Translation/Lang/2ADT-to-VariantList.agda
rename to src/Translation/Lang/ADT-to-VariantList.agda
index 5f58c9e2..643aef12 100644
--- a/src/Translation/Lang/2ADT-to-VariantList.agda
+++ b/src/Translation/Lang/ADT-to-VariantList.agda
@@ -1,7 +1,7 @@
 open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼)
 open import Data.Bool using (Bool; true; false; not; if_then_else_)
 open import Relation.Binary using (DecidableEquality; Rel)
-module Translation.Lang.2ADT-to-VariantList
+module Translation.Lang.ADT-to-VariantList
   (F : 𝔽)
   (V : 𝕍)
   (_==_ : DecidableEquality F)
@@ -27,44 +27,44 @@ open import Framework.Compiler
 open import Framework.Relation.Expressiveness V using (_≽_; expressiveness-from-compiler)
 open import Framework.Properties.Soundness V using (Sound)
 open import Framework.Proof.Transitive V using (soundness-by-expressiveness)
-open import Lang.2ADT
-  using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
+open import Lang.ADT
+  using (ADT; ADTL; leaf; _⟨_,_⟩)
   renaming (⟦_⟧ to ⟦_⟧₂; Configuration to Conf₂)
 open import Lang.VariantList V
   using (VariantList; VariantListL; VariantList-is-Sound)
   renaming (⟦_⟧ to ⟦_⟧ₗ; Configuration to Confₗ)
 
-open import Lang.2ADT.Path F V _==_
-open import Translation.Lang.2ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ; Undead2ADT; Undead2ADTL)
-open import Translation.Lang.2ADT.WalkSemantics F V _==_ as Walk using ()
+open import Lang.ADT.Path F V _==_
+open import Translation.Lang.ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ; UndeadADT; UndeadADTL)
+open import Translation.Lang.ADT.WalkSemantics F V _==_ as Walk using ()
 
 open import Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸)
 open import Util.AuxProofs using (<-cong-+ˡ)
 
 {-
-This translates a 2ADT to a VariantList.
-This is correct only if the 2ADT is undead.
+This translates a ADT to a VariantList.
+This is correct only if the ADT is undead.
 Otherwise, also dead variants will be part of
 the resulting list.
 -}
-tr : ∀ {A : 𝔸} → 2ADT V F A → VariantList A
+tr : ∀ {A : 𝔸} → ADT V F A → VariantList A
 tr (leaf v) = v ∷ []
 tr (D ⟨ l , r ⟩) = tr l ⁺++⁺ tr r
 
-tr-undead : ∀ {A : 𝔸} → Undead2ADT A → VariantList A
+tr-undead : ∀ {A : 𝔸} → UndeadADT A → VariantList A
 tr-undead = tr ∘ node
 
-toVariantList : ∀ {A : 𝔸} → 2ADT V F A → VariantList A
+toVariantList : ∀ {A : 𝔸} → ADT V F A → VariantList A
 toVariantList = tr-undead ∘ kill-dead
 
--- Converts a path to in the input 2ADT to the index in the resulting list.
-conf : ∀ {A} → (e : 2ADT V F A) → PathConfig e → ℕ
+-- Converts a path to in the input ADT to the index in the resulting list.
+conf : ∀ {A} → (e : ADT V F A) → PathConfig e → ℕ
 conf .(leaf _) (.[] is-valid tleaf) = 0
 conf (D ⟨ l , _ ⟩) ((_ ∷ pl) is-valid walk-left  t) = conf l (pl is-valid t)
 conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right t) = length (tr l) + conf r (pr is-valid t)
 
--- Converts an index from the resulting list back to a path in the input 2ADT.
-fnoc : ∀ {A} → (e : 2ADT V F A) → ℕ → PathConfig e
+-- Converts an index from the resulting list back to a path in the input ADT.
+fnoc : ∀ {A} → (e : ADT V F A) → ℕ → PathConfig e
 fnoc (leaf v) _ = [] is-valid tleaf
 fnoc (D ⟨ l , r ⟩) i with length (tr l) ≤? i
 fnoc (D ⟨ l , r ⟩) i | no _ {-left-} with fnoc l i
@@ -74,7 +74,7 @@ fnoc (D ⟨ l , r ⟩) i | yes _  {-right-} with fnoc r (i ∸ (length (tr l)))
 
 -- The index of a path will never be out of bounds.
 conf-bounded : ∀ {A}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → (c : PathConfig e)
   → conf e c < length (tr e)
 conf-bounded (leaf v) (.[] is-valid tleaf) = s≤s z≤n
@@ -96,7 +96,7 @@ conf-bounded (D ⟨ l , r ⟩) ((.D ↣ false ∷ p) is-valid walk-right t) = go
     go rewrite ⁺++⁺-length (tr l) (tr r) = gox
 
 preservation-walk-to-list-conf : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → walk e ⊆[ conf e ] ⟦ tr e ⟧ₗ
 preservation-walk-to-list-conf .(leaf _) (.[] is-valid tleaf) = refl
 preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pl) is-valid walk-left t) =
@@ -121,7 +121,7 @@ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right
   ∎
 
 preservation-walk-to-list-fnoc : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → ⟦ tr e ⟧ₗ ⊆[ fnoc e ] walk e
 preservation-walk-to-list-fnoc (leaf v) i = refl
 preservation-walk-to-list-fnoc (D ⟨ l , r ⟩) i with length (tr l) ≤? i
@@ -152,23 +152,23 @@ preservation-walk-to-list-fnoc (D ⟨ l , r ⟩) i with length (tr l) ≤? i
 
 {-
 This proves that 'tr' preserves walk-semantics.
-This means that when we evaluate 2ADTs by just walking "randomly"
-down them, then simply converting a 2ADT to a variant list by
+This means that when we evaluate ADTs by just walking "randomly"
+down them, then simply converting a ADT to a variant list by
 gathering all variants in leafs from left to right preserves semantics.
 -}
 preservation-walk-to-list : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → walk e ≅[ conf e ][ fnoc e ] ⟦ tr e ⟧ₗ
 preservation-walk-to-list e = (preservation-walk-to-list-conf e , preservation-walk-to-list-fnoc e)
 
-conf-undead-to-list : ∀ {A} → Undead2ADT A → Conf₂ F → ℕ
+conf-undead-to-list : ∀ {A} → UndeadADT A → Conf₂ F → ℕ
 conf-undead-to-list e = conf (node e) ∘ Walk.fun-to-path (node e)
 
-fnoc-undead-to-list : ∀ {A} → Undead2ADT A → ℕ → Conf₂ F
+fnoc-undead-to-list : ∀ {A} → UndeadADT A → ℕ → Conf₂ F
 fnoc-undead-to-list e = Walk.path-to-fun (node e) ∘ fnoc (node e)
 
 preservation-undead-to-list : ∀ {A : 𝔸}
-  → (e : Undead2ADT A)
+  → (e : UndeadADT A)
   → ⟦ e ⟧ᵤ ≅[ conf-undead-to-list e ][ fnoc-undead-to-list e ] ⟦ tr-undead e ⟧ₗ
 preservation-undead-to-list e =
   ≅[]-begin
@@ -179,8 +179,8 @@ preservation-undead-to-list e =
     ⟦ tr-undead e ⟧ₗ
   ≅[]-∎
 
-Undead2ADT→VariantList : LanguageCompiler Undead2ADTL VariantListL
-Undead2ADT→VariantList = record
+UndeadADT→VariantList : LanguageCompiler UndeadADTL VariantListL
+UndeadADT→VariantList = record
   { compile = tr-undead
   ; config-compiler = λ e → record
     { to = conf-undead-to-list e
@@ -189,11 +189,11 @@ Undead2ADT→VariantList = record
   ; preserves = preservation-undead-to-list
   }
 
-2ADT→VariantList : LanguageCompiler (2ADTL V F) VariantListL
-2ADT→VariantList = DeadElim.kill-dead-compiler ⊕ Undead2ADT→VariantList
+ADT→VariantList : LanguageCompiler (ADTL V F) VariantListL
+ADT→VariantList = DeadElim.kill-dead-compiler ⊕ UndeadADT→VariantList
 
-VariantList≽2ADT : VariantListL ≽ 2ADTL V F
-VariantList≽2ADT = expressiveness-from-compiler 2ADT→VariantList
+VariantList≽ADT : VariantListL ≽ ADTL V F
+VariantList≽ADT = expressiveness-from-compiler ADT→VariantList
 
-2ADT-is-sound : Sound (2ADTL V F)
-2ADT-is-sound = soundness-by-expressiveness VariantList-is-Sound VariantList≽2ADT
+ADT-is-sound : Sound (ADTL V F)
+ADT-is-sound = soundness-by-expressiveness VariantList-is-Sound VariantList≽ADT
diff --git a/src/Translation/Lang/2ADT/DeadElim.agda b/src/Translation/Lang/ADT/DeadElim.agda
similarity index 89%
rename from src/Translation/Lang/2ADT/DeadElim.agda
rename to src/Translation/Lang/ADT/DeadElim.agda
index 7e23760f..5f4dbcf2 100644
--- a/src/Translation/Lang/2ADT/DeadElim.agda
+++ b/src/Translation/Lang/ADT/DeadElim.agda
@@ -1,6 +1,6 @@
 open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼)
 open import Relation.Binary using (DecidableEquality; Rel)
-module Translation.Lang.2ADT.DeadElim
+module Translation.Lang.ADT.DeadElim
   (F : 𝔽)
   (V : 𝕍)
   (_==_ : DecidableEquality F)
@@ -23,15 +23,15 @@ open Eq.≡-Reasoning
 open import Framework.VariabilityLanguage
 open import Framework.Compiler
 open import Data.EqIndexedSet using (_≅[_][_]_; ≐→≅[])
-open import Lang.2ADT
-open import Lang.2ADT.Path F V _==_
+open import Lang.ADT
+open import Lang.ADT.Path F V _==_
 
 {-
-A 2ADT is undead if it does not contain any dead branches.
+A ADT is undead if it does not contain any dead branches.
 This is the case if any path from the root to a leaf does not contain
 a feature name twice.
 -}
-Undead : ∀ {A} (e : 2ADT V F A) → Set
+Undead : ∀ {A} (e : ADT V F A) → Set
 Undead e = ∀ (p : Path) → p starts-at e → Unique p
 
 {-
@@ -45,7 +45,7 @@ undead-leaf .[] tleaf = []
 {-
 If a choice is undead, so is its left alternative.
 -}
-undead-left : ∀ {A} {D} {l r : 2ADT V F A}
+undead-left : ∀ {A} {D} {l r : ADT V F A}
   → Undead (D ⟨ l , r ⟩)
     --------------------
   → Undead l
@@ -55,7 +55,7 @@ undead-left {D = D} u-chc p t with u-chc (D ↣ true ∷ p) (walk-left t)
 {-
 If a choice is undead, so is its right alternative.
 -}
-undead-right : ∀ {A} {D} {l r : 2ADT V F A}
+undead-right : ∀ {A} {D} {l r : ADT V F A}
   → Undead (D ⟨ l , r ⟩)
     --------------------
   → Undead r
@@ -67,7 +67,7 @@ If two expressions l and r are undead and do
 not contain the feature name D,
 then the choice D ⟨ l , r ⟩ is undead, too.
 -}
-undead-choice : ∀ {A} {D} {l r : 2ADT V F A}
+undead-choice : ∀ {A} {D} {l r : ADT V F A}
   → Undead l
   → Undead r
     -- It might be handy to introduce a new predicate for containment of feature names in expressions D ∈ l later.
@@ -78,18 +78,18 @@ undead-choice : ∀ {A} {D} {l r : 2ADT V F A}
 undead-choice u-l u-r D∉l D∉r (.(_ ↣ true ) ∷ p) (walk-left  t) = ∉→All-different p (D∉l p t) ∷ (u-l p t)
 undead-choice u-l u-r D∉l D∉r (.(_ ↣ false) ∷ p) (walk-right t) = ∉→All-different p (D∉r p t) ∷ (u-r p t)
 
-record Undead2ADT (A : 𝔸) : Set where
+record UndeadADT (A : 𝔸) : Set where
   constructor _⊚_ -- \oo
   field
-    node   : 2ADT V F A
+    node   : ADT V F A
     undead : Undead node
-open Undead2ADT public
+open UndeadADT public
 
-⟦_⟧ᵤ : 𝔼-Semantics V (Configuration F) Undead2ADT
+⟦_⟧ᵤ : 𝔼-Semantics V (Configuration F) UndeadADT
 ⟦_⟧ᵤ = ⟦_⟧ ∘ node
 
-Undead2ADTL : VariabilityLanguage V
-Undead2ADTL = ⟪ Undead2ADT , Configuration F , ⟦_⟧ᵤ ⟫
+UndeadADTL : VariabilityLanguage V
+UndeadADTL = ⟪ UndeadADT , Configuration F , ⟦_⟧ᵤ ⟫
 
 {-
 Kills all dead branches within a given expression,
@@ -97,8 +97,8 @@ assuming that some features were already defined.
 -}
 kill-dead-below : ∀ {A}
   → (defined : Path)
-  → 2ADT V F A
-  → 2ADT V F A
+  → ADT V F A
+  → ADT V F A
 kill-dead-below _ (leaf v) = leaf v
 kill-dead-below defined (D ⟨ l , r ⟩) with D ∈? defined
 --- The current choice was already encountered above this choice.
@@ -123,7 +123,7 @@ kill-dead-eliminates-defined-features : ∀ {A}
   → (defined : Path)
   → (D : F)
   → D ∈ defined
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → D ∉' kill-dead-below defined e
 kill-dead-eliminates-defined-features _ _ _ (leaf _) .[] tleaf ()
 kill-dead-eliminates-defined-features defined _ _ (D' ⟨ _ , _ ⟩) _ _ _ with D' ∈? defined
@@ -150,7 +150,7 @@ is undead.
 -}
 kill-dead-correct : ∀ {A}
   → (defined : Path)
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → Undead (kill-dead-below defined e)
 kill-dead-correct _ (leaf v) = undead-leaf
 kill-dead-correct defined (D ⟨ _ , _ ⟩) with D ∈? defined
@@ -165,15 +165,15 @@ kill-dead-correct defined (D ⟨ l , r ⟩) | no  D∉defined =
   (kill-dead-eliminates-defined-features (D ↣ false ∷ defined) D (here (is-refl D false)) r)
 
 {-
-Dead branch elimination of 2ADTs.
+Dead branch elimination of ADTs.
 -}
 kill-dead : ∀ {A}
-  → 2ADT V F A
-  → Undead2ADT A
+  → ADT V F A
+  → UndeadADT A
 kill-dead e = kill-dead-below [] e ⊚ kill-dead-correct [] e
 
 kill-dead-preserves-below-partial-configs : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → (defined : Path)
   → (c : Configuration F)
   → defined ⊑ c
@@ -191,11 +191,11 @@ kill-dead-preserves-below-partial-configs (D ⟨ l , r ⟩) def c def⊑c | no D
 ... | false = kill-dead-preserves-below-partial-configs r ((D ↣ false) ∷ def) c (eq ∷ def⊑c)
 
 kill-dead-preserves : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → ⟦ e ⟧ ≅[ id ][ id ] ⟦ kill-dead e ⟧ᵤ
 kill-dead-preserves e = ≐→≅[] (λ c → kill-dead-preserves-below-partial-configs e [] c [])
 
-kill-dead-compiler : LanguageCompiler (2ADTL V F) Undead2ADTL
+kill-dead-compiler : LanguageCompiler (ADTL V F) UndeadADTL
 kill-dead-compiler = record
   { compile = kill-dead
   ; config-compiler = λ _ → record { to = id ; from = id }
diff --git a/src/Translation/Lang/2ADT/Rename.agda b/src/Translation/Lang/ADT/Rename.agda
similarity index 52%
rename from src/Translation/Lang/2ADT/Rename.agda
rename to src/Translation/Lang/ADT/Rename.agda
index 98e9ee79..c0ed63a7 100644
--- a/src/Translation/Lang/2ADT/Rename.agda
+++ b/src/Translation/Lang/ADT/Rename.agda
@@ -7,7 +7,7 @@ open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to
 {-
 This module renames dimensions in algebraic decision trees.
 -}
-module Translation.Lang.2ADT.Rename (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.ADT.Rename (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 open import Data.Bool using (if_then_else_)
 open import Data.Bool.Properties as Bool
@@ -27,84 +27,84 @@ open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎)
 open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
 
 open import Lang.All.Generic Variant Artifact∈ₛVariant
-open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
+open ADT using (ADT; ADTL; leaf; _⟨_,_⟩)
 
 artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
-2ADT-map-config : ∀ {D₁ D₂ : 𝔽}
+ADT-map-config : ∀ {D₁ D₂ : 𝔽}
   → (D₂ → D₁)
-  → 2ADT.Configuration D₁
-  → 2ADT.Configuration D₂
-2ADT-map-config f config = config ∘ f
+  → ADT.Configuration D₁
+  → ADT.Configuration D₂
+ADT-map-config f config = config ∘ f
 
 rename : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
   → (D₁ → D₂)
-  → 2ADT Variant D₁ A
-  → 2ADT Variant D₂ A
+  → ADT Variant D₁ A
+  → ADT Variant D₂ A
 rename f (leaf v) = leaf v
-rename f (d 2ADT.⟨ l , r ⟩) = f d ⟨ rename f l , rename f r ⟩
+rename f (d ADT.⟨ l , r ⟩) = f d ⟨ rename f l , rename f r ⟩
 
 preserves-⊆ : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
-  → (expr : 2ADT Variant D₁ A)
-  → 2ADT.⟦ rename f expr ⟧ ⊆[ 2ADT-map-config f ] 2ADT.⟦ expr ⟧
+  → (expr : ADT Variant D₁ A)
+  → ADT.⟦ rename f expr ⟧ ⊆[ ADT-map-config f ] ADT.⟦ expr ⟧
 preserves-⊆ f f⁻¹ (leaf v) config = refl
 preserves-⊆ f f⁻¹ (d ⟨ l , r ⟩) config =
-    2ADT.⟦ rename f (d ⟨ l , r ⟩) ⟧ config
+    ADT.⟦ rename f (d ⟨ l , r ⟩) ⟧ config
   ≡⟨⟩
-    2ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config
+    ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config
   ≡⟨⟩
-    (if config (f d) then 2ADT.⟦ rename f l ⟧ config else 2ADT.⟦ rename f r ⟧ config)
+    (if config (f d) then ADT.⟦ rename f l ⟧ config else ADT.⟦ rename f r ⟧ config)
   ≡⟨ Eq.cong₂ (if config (f d) then_else_) (preserves-⊆ f f⁻¹ l config) (preserves-⊆ f f⁻¹ r config) ⟩
-    (if config (f d) then 2ADT.⟦ l ⟧ (config ∘ f) else 2ADT.⟦ r ⟧ (config ∘ f))
+    (if config (f d) then ADT.⟦ l ⟧ (config ∘ f) else ADT.⟦ r ⟧ (config ∘ f))
   ≡⟨⟩
-    2ADT.⟦ d ⟨ l , r ⟩ ⟧ (config ∘ f)
+    ADT.⟦ d ⟨ l , r ⟩ ⟧ (config ∘ f)
   ∎
 
 preserves-⊇ : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
-  → (expr : 2ADT Variant D₁ A)
-  → 2ADT.⟦ expr ⟧ ⊆[ 2ADT-map-config f⁻¹ ] 2ADT.⟦ rename f expr ⟧
+  → (expr : ADT Variant D₁ A)
+  → ADT.⟦ expr ⟧ ⊆[ ADT-map-config f⁻¹ ] ADT.⟦ rename f expr ⟧
 preserves-⊇ f f⁻¹ is-inverse (leaf v) config = refl
 preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config =
-    2ADT.⟦ d ⟨ l , r ⟩ ⟧ config
+    ADT.⟦ d ⟨ l , r ⟩ ⟧ config
   ≡⟨⟩
-    (if config d then 2ADT.⟦ l ⟧ config else 2ADT.⟦ r ⟧ config)
+    (if config d then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config)
   ≡⟨ Eq.cong₂ (if config d then_else_) (preserves-⊇ f f⁻¹ is-inverse l config) (preserves-⊇ f f⁻¹ is-inverse r config) ⟩
-    (if config d then 2ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else 2ADT.⟦ rename f r ⟧ (config ∘ f⁻¹))
-  ≡˘⟨ Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (2ADT.⟦ rename f l ⟧ (config ∘ f⁻¹))) (2ADT.⟦ rename f r ⟧ (config ∘ f⁻¹)) ⟩
-    (if config (f⁻¹ (f d)) then 2ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else 2ADT.⟦ rename f r ⟧ (config ∘ f⁻¹))
+    (if config d then ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else ADT.⟦ rename f r ⟧ (config ∘ f⁻¹))
+  ≡˘⟨ Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (ADT.⟦ rename f l ⟧ (config ∘ f⁻¹))) (ADT.⟦ rename f r ⟧ (config ∘ f⁻¹)) ⟩
+    (if config (f⁻¹ (f d)) then ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else ADT.⟦ rename f r ⟧ (config ∘ f⁻¹))
   ≡⟨⟩
-    2ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹)
+    ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹)
   ≡⟨⟩
-    2ADT.⟦ rename f (d ⟨ l , r ⟩) ⟧ (config ∘ f⁻¹)
+    ADT.⟦ rename f (d ⟨ l , r ⟩) ⟧ (config ∘ f⁻¹)
   ∎
 
 preserves : ∀ {D₁ D₂ : 𝔽} {A : 𝔸}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
-  → (e : 2ADT Variant D₁ A)
-  → 2ADT.⟦ rename f e ⟧ ≅[ 2ADT-map-config f ][ 2ADT-map-config f⁻¹ ] 2ADT.⟦ e ⟧
+  → (e : ADT Variant D₁ A)
+  → ADT.⟦ rename f e ⟧ ≅[ ADT-map-config f ][ ADT-map-config f⁻¹ ] ADT.⟦ e ⟧
 preserves f f⁻¹ is-inverse expr = preserves-⊆ f f⁻¹ expr and preserves-⊇ f f⁻¹ is-inverse expr
 
-2ADT-rename : ∀ {D₁ D₂ : 𝔽}
+ADT-rename : ∀ {D₁ D₂ : 𝔽}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
-  → LanguageCompiler (2ADTL Variant D₁) (2ADTL Variant D₂)
-2ADT-rename f f⁻¹ is-inverse .LanguageCompiler.compile = rename f
-2ADT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = 2ADT-map-config f⁻¹
-2ADT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = 2ADT-map-config f
-2ADT-rename f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves f f⁻¹ is-inverse expr)
+  → LanguageCompiler (ADTL Variant D₁) (ADTL Variant D₂)
+ADT-rename f f⁻¹ is-inverse .LanguageCompiler.compile = rename f
+ADT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .to = ADT-map-config f⁻¹
+ADT-rename f f⁻¹ is-inverse .LanguageCompiler.config-compiler expr .from = ADT-map-config f
+ADT-rename f f⁻¹ is-inverse .LanguageCompiler.preserves expr = ≅[]-sym (preserves f f⁻¹ is-inverse expr)
 
-2ADT-rename≽2ADT : ∀ {D₁ D₂ : Set}
+ADT-rename≽ADT : ∀ {D₁ D₂ : Set}
   → (f : D₁ → D₂)
   → (f⁻¹ : D₂ → D₁)
   → f⁻¹ ∘ f ≗ id
-  → 2ADTL Variant D₂ ≽ 2ADTL Variant D₁
-2ADT-rename≽2ADT f f⁻¹ is-inverse = expressiveness-from-compiler (2ADT-rename f f⁻¹ is-inverse)
+  → ADTL Variant D₂ ≽ ADTL Variant D₁
+ADT-rename≽ADT f f⁻¹ is-inverse = expressiveness-from-compiler (ADT-rename f f⁻¹ is-inverse)
diff --git a/src/Translation/Lang/2ADT/WalkSemantics.agda b/src/Translation/Lang/ADT/WalkSemantics.agda
similarity index 92%
rename from src/Translation/Lang/2ADT/WalkSemantics.agda
rename to src/Translation/Lang/ADT/WalkSemantics.agda
index 1c79fd5f..fb0c41ae 100644
--- a/src/Translation/Lang/2ADT/WalkSemantics.agda
+++ b/src/Translation/Lang/ADT/WalkSemantics.agda
@@ -1,13 +1,13 @@
 {-
-Walk semantics are equivalent to ordinary 2ADT semantics
-as long as the 2ADT does not contain any dead branches.
+Walk semantics are equivalent to ordinary ADT semantics
+as long as the ADT does not contain any dead branches.
 This means that configurations can be modelled as functions or as paths.
 Interestingly, we obtain a compiler that does not change the input
 expression but only translates configurations.
 -}
 open import Framework.Definitions using (𝔽; 𝕍; 𝔸)
 open import Relation.Binary using (DecidableEquality; Rel)
-module Translation.Lang.2ADT.WalkSemantics
+module Translation.Lang.ADT.WalkSemantics
   (F : 𝔽)
   (V : 𝕍)
   (_==_ : DecidableEquality F)
@@ -30,9 +30,9 @@ open import Data.EqIndexedSet hiding (_∈_)
 open Data.EqIndexedSet.≅-Reasoning
 
 open import Framework.VariabilityLanguage
-open import Lang.2ADT using (2ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
-open import Lang.2ADT.Path F V _==_
-open import Translation.Lang.2ADT.DeadElim F V _==_
+open import Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
+open import Lang.ADT.Path F V _==_
+open import Translation.Lang.ADT.DeadElim F V _==_
 
 open import Util.Suffix
 
@@ -42,7 +42,7 @@ the given tree.
 The conversion checks the configuration function at each choice,
 constructs the path accordingly, and recurses until it reaches a leaf.
 -}
-fun-to-path : ∀ {A} (e : 2ADT V F A) → Configuration F → PathConfig e
+fun-to-path : ∀ {A} (e : ADT V F A) → Configuration F → PathConfig e
 fun-to-path (leaf _) _ = [] is-valid tleaf
 fun-to-path (D ⟨ _ , _ ⟩) c with c D
 fun-to-path (D ⟨ l , _ ⟩) c | true  with fun-to-path l c
@@ -59,7 +59,7 @@ Otherwise, returns true.
 (The returned function returns true for all features that
 are not on a valid path.)
 -}
-path-to-fun : ∀ {A} (e : 2ADT V F A) → PathConfig e → Configuration F
+path-to-fun : ∀ {A} (e : ADT V F A) → PathConfig e → Configuration F
 path-to-fun .(leaf _) ([] is-valid tleaf) _ = true
 path-to-fun (.D ⟨ l , r ⟩) (((D ↣ .true) ∷ p) is-valid walk-left t) D' =
   if (isYes (D == D'))
@@ -95,7 +95,7 @@ Crucial lemma for proving preservation.
 path-to-fun returns the value b for a given feature D
 if the path given to path-to-fun contains the selection D ↣ b somewhere.
 -}
-path-to-fun-lem : ∀ {A} (D : F) (e : 2ADT V F A) (p q : Path) (t : p starts-at e)
+path-to-fun-lem : ∀ {A} (D : F) (e : ADT V F A) (p q : Path) (t : p starts-at e)
   → (b : Bool)
   → Unique p
   → p endswith ((D ↣ b) ∷ q)
@@ -121,7 +121,7 @@ endswith-path-contains _ (match .((_ ↣ _) ∷ _)) = here (fromWitness refl)
 endswith-path-contains b (later x) = there (endswith-path-contains b x)
 
 path-to-fun-step-l-inner2 : ∀ {A}
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → (p : Path) → (t : p starts-at l)
   → All (different (D ↣ true)) p
     -------------------------------------------------------------------
@@ -134,7 +134,7 @@ path-to-fun-step-l-inner2 D l r p t all-dims-in-p-different-to-D E E∈p with D
 
 -- clone-and-own from path-to-fun-step-l-inner2
 path-to-fun-step-r-inner2 : ∀ {A}
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → (p : Path) → (t : p starts-at r)
   → All (different (D ↣ false)) p
     -------------------------------------------------------------------
@@ -147,10 +147,10 @@ path-to-fun-step-r-inner2 D l r p t all-dims-in-p-different-to-D E E∈p with D
 
 path-to-fun-step-l-inner : ∀ {A}
   -- for a choice D ⟨ l , r ⟩
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → (lp : Path)
   -- if there is a subexpression e
-  → (e : 2ADT V F A) (ep : Path)
+  → (e : ADT V F A) (ep : Path)
   -- (i.e., all paths starting in l end in paths starting in e)
   → (tlp : lp starts-at l)
   → (tep : ep starts-at e)
@@ -194,9 +194,9 @@ path-to-fun-step-l-inner D l r lp (D' ⟨ a , b ⟩) ((.D' ↣ false) ∷ ep) tl
 -- This is a huge copy and paste blob from
 -- path-to-fun-step-r-inner
 path-to-fun-step-r-inner : ∀ {A}
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → (rp : Path)
-  → (e : 2ADT V F A) (ep : Path)
+  → (e : ADT V F A) (ep : Path)
   → (trp : rp starts-at r)
   → (tep : ep starts-at e)
   → (sub : rp endswith ep)
@@ -218,7 +218,7 @@ path-to-fun-step-r-inner D l r lp (D' ⟨ a , b ⟩) ((.D' ↣ false) ∷ ep) tl
   = refl
 
 path-to-fun-step-l : ∀ {A}
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → Undead (D ⟨ l , r ⟩)
   → (p : Path)
   → (t : p starts-at l)
@@ -228,7 +228,7 @@ path-to-fun-step-l D l r u p t with u ((D ↣ true) ∷ p) (walk-left t)
 ... | u ∷ uu = path-to-fun-step-l-inner D l r p l p t t (match p) u uu
 
 path-to-fun-step-r : ∀ {A}
-  → (D : F) (l r : 2ADT V F A)
+  → (D : F) (l r : ADT V F A)
   → Undead (D ⟨ l , r ⟩)
   → (p : Path)
   → (t : p starts-at r)
@@ -239,7 +239,7 @@ path-to-fun-step-r D l r u p t with u ((D ↣ false) ∷ p) (walk-right t)
 
 path-to-fun-head : ∀ {A}
   → (D : F)
-  → (l r : 2ADT V F A)
+  → (l r : ADT V F A)
   → (b : Bool)
   → (p : Path)
   → (t : ((D ↣ b) ∷ p) starts-at (D ⟨ l , r ⟩))
@@ -252,7 +252,7 @@ path-to-fun-head D l r .false p (walk-right t) with D == D
 ... | no  D≢D = ⊥-elim (D≢D refl)
 
 preservation-path-configs-conf : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → (u : Undead e)
   → ⟦ e ⊚ u ⟧ᵤ ⊆[ fun-to-path e ] walk e
 preservation-path-configs-conf (leaf _) _ _ = refl
@@ -272,7 +272,7 @@ preservation-path-configs-conf (_ ⟨ _ , r ⟩) u c | false with fun-to-path r
 ... | _ rewrite (sym eq) = preservation-path-configs-conf r (undead-right u) c
 
 preservation-path-configs-fnoc : ∀ {A : 𝔸}
-  → (e : 2ADT V F A)
+  → (e : ADT V F A)
   → (u : Undead e)
   → walk e ⊆[ path-to-fun e ] ⟦ e ⊚ u ⟧ᵤ
 preservation-path-configs-fnoc (leaf v) _ (.[] is-valid tleaf) = refl
@@ -294,13 +294,13 @@ preservation-path-configs-fnoc (D ⟨ l , r ⟩) u ((.(D ↣ false) ∷ p) is-va
   = refl
 
 preservation : ∀ {A : 𝔸}
-  → (e : Undead2ADT A)
+  → (e : UndeadADT A)
   → ⟦ e ⟧ᵤ ≅[ fun-to-path (node e) ][ path-to-fun (node e) ] walk (node e)
 preservation e =
     preservation-path-configs-conf (node e) (undead e)
   , preservation-path-configs-fnoc (node e) (undead e)
 
 -- We cannot construct a LanguageCompiler because
--- we cannot construct a VariabilityLanguage for 2ADT with walk semantics because
+-- we cannot construct a VariabilityLanguage for ADT with walk semantics because
 -- configurations for walk semantics (PathConfig) depend on the input expression
 -- which currently, cannot be modelled within our framework.
diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md
index 313216ee..6bfc9780 100644
--- a/src/Translation/LanguageMap.lagda.md
+++ b/src/Translation/LanguageMap.lagda.md
@@ -47,7 +47,7 @@ open CCC using (CCCL)
 open NCC using (NCCL)
 open 2CC using (2CCL)
 open NADT using (NADTL)
-open 2ADT using (2ADTL)
+open ADT using (ADTL)
 open OC using (WFOCL)
 
 open CCC.Encode using () renaming (encoder to CCC-Rose-encoder)
@@ -63,12 +63,12 @@ import Translation.Lang.NCC-to-2CC Variant mkArtifact as NCC-to-2CC
 import Translation.Lang.2CC-to-NCC Variant mkArtifact as 2CC-to-NCC
 import Translation.Lang.Transitive.CCC-to-2CC Variant mkArtifact as CCC-to-2CC
 import Translation.Lang.Transitive.2CC-to-CCC Variant mkArtifact as 2CC-to-CCC
-import Translation.Lang.2CC-to-2ADT Variant mkArtifact as 2CC-to-2ADT
-import Translation.Lang.2ADT-to-2CC Variant mkArtifact as 2ADT-to-2CC
-import Translation.Lang.2ADT.DeadElim as DeadElim
-import Translation.Lang.2ADT-to-VariantList as 2ADT-to-VariantList
+import Translation.Lang.2CC-to-ADT Variant mkArtifact as 2CC-to-ADT
+import Translation.Lang.ADT-to-2CC Variant mkArtifact as ADT-to-2CC
+import Translation.Lang.ADT.DeadElim as DeadElim
+import Translation.Lang.ADT-to-VariantList as ADT-to-VariantList
 import Translation.Lang.VariantList-to-CCC as VariantList-to-CCC
-import Translation.Lang.2ADT-to-NADT Variant mkArtifact as 2ADT-to-NADT
+import Translation.Lang.ADT-to-NADT Variant mkArtifact as ADT-to-NADT
 import Translation.Lang.NADT-to-CCC Variant mkArtifact as NADT-to-CCC
 import Translation.Lang.OC-to-2CC as OC-to-2CC
 ```
@@ -96,18 +96,18 @@ open 2CC-to-CCC using (2CC→CCC) public
 ## Choices vs Algebraic Decision Trees
 
 ```agda
-open 2CC-to-2ADT using (2CC→2ADT) public
-open 2ADT-to-2CC using (2ADT→2CC) public
+open 2CC-to-ADT using (2CC→ADT) public
+open ADT-to-2CC using (ADT→2CC) public
 
 module _ {F : 𝔽} (_==_ : DecidableEquality F) where
   open DeadElim F Variant _==_ using (kill-dead-compiler) public
 
-  open 2ADT-to-VariantList F Variant _==_ using (2ADT→VariantList) public
+  open ADT-to-VariantList F Variant _==_ using (ADT→VariantList) public
 
 module _ {F : 𝔽} (D : F) where
   open VariantList-to-CCC.Translate F D Variant mkArtifact CCC-Rose-encoder using (VariantList→CCC) public
 
-open 2ADT-to-NADT using (2ADT→NADT) public
+open ADT-to-NADT using (ADT→NADT) public
 NADT→CCC : ∀ {F : 𝔽} → LanguageCompiler (NADTL Variant F) (CCCL F)
 NADT→CCC {F} = NADT-to-CCC.NADT→CCC {F = F} CCC-Rose-encoder
 ```
@@ -181,20 +181,20 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ)
   2CC≽CCC : 2CCL F ≽ CCCL F
   2CC≽CCC = ≽-trans (2CC-rename≽2CC f f⁻¹ f⁻¹∘f≗id) CCC-to-2CC.2CC≽CCC
 
-  2CC≽2ADT : 2CCL F ≽ 2ADTL Variant F
-  2CC≽2ADT = 2ADT-to-2CC.2CC≽2ADT (CCC-Rose-encoder ⊕ (CCC→2CC ⊕ 2CC-rename f f⁻¹ f⁻¹∘f≗id))
+  2CC≽ADT : 2CCL F ≽ ADTL Variant F
+  2CC≽ADT = ADT-to-2CC.2CC≽ADT (CCC-Rose-encoder ⊕ (CCC→2CC ⊕ 2CC-rename f f⁻¹ f⁻¹∘f≗id))
 
-  2ADT≽2CC : 2ADTL Variant F ≽ 2CCL F
-  2ADT≽2CC = 2CC-to-2ADT.2ADT≽2CC
+  ADT≽2CC : ADTL Variant F ≽ 2CCL F
+  ADT≽2CC = 2CC-to-ADT.ADT≽2CC
 
-  VariantList≽2ADT : (_==_ : DecidableEquality F) → VariantListL ≽ 2ADTL Variant F
-  VariantList≽2ADT _==_ = 2ADT-to-VariantList.VariantList≽2ADT F Variant _==_
+  VariantList≽ADT : (_==_ : DecidableEquality F) → VariantListL ≽ ADTL Variant F
+  VariantList≽ADT _==_ = ADT-to-VariantList.VariantList≽ADT F Variant _==_
 
   CCC≽VariantList : F → CCCL F ≽ VariantListL
   CCC≽VariantList D = VariantList-to-CCC.Translate.CCC≽VariantList F D Variant mkArtifact CCC-Rose-encoder
 
-  NADT≽2ADT : NADTL Variant F ≽ 2ADTL Variant F
-  NADT≽2ADT = 2ADT-to-NADT.NADT≽2ADT
+  NADT≽ADT : NADTL Variant F ≽ ADTL Variant F
+  NADT≽ADT = ADT-to-NADT.NADT≽ADT
 
   CCC≽NADT : ∀ {F : 𝔽} → CCCL F ≽ NADTL Variant F
   CCC≽NADT {F} = NADT-to-CCC.CCC≽NADT {F} CCC-Rose-encoder
@@ -215,17 +215,17 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ)
   CCC≋2CC : CCCL F ≋ 2CCL F
   CCC≋2CC = CCC≽2CC , 2CC≽CCC
 
-  2CC≋2ADT : 2CCL F ≋ 2ADTL Variant F
-  2CC≋2ADT = 2CC≽2ADT , 2ADT≽2CC
+  2CC≋ADT : 2CCL F ≋ ADTL Variant F
+  2CC≋ADT = 2CC≽ADT , ADT≽2CC
 
-  2ADT≋NADT : 2ADTL Variant F ≋ NADTL Variant F
-  2ADT≋NADT = ≽-trans 2ADT≽2CC (≽-trans 2CC≽CCC CCC≽NADT) , NADT≽2ADT
+  ADT≋NADT : ADTL Variant F ≋ NADTL Variant F
+  ADT≋NADT = ≽-trans ADT≽2CC (≽-trans 2CC≽CCC CCC≽NADT) , NADT≽ADT
 
-  2ADT≋VariantList : DecidableEquality F → F → 2ADTL Variant F ≋ VariantListL
-  2ADT≋VariantList _==_ D = ≽-trans 2ADT≽2CC (≽-trans 2CC≽CCC (CCC≽VariantList D)) , VariantList≽2ADT _==_
+  ADT≋VariantList : DecidableEquality F → F → ADTL Variant F ≋ VariantListL
+  ADT≋VariantList _==_ D = ≽-trans ADT≽2CC (≽-trans 2CC≽CCC (CCC≽VariantList D)) , VariantList≽ADT _==_
 
   VariantList≋CCC : DecidableEquality F → F → VariantListL ≋ CCCL F
-  VariantList≋CCC _==_ D = ≽-trans (VariantList≽2ADT _==_) (≽-trans 2ADT≽2CC 2CC≽CCC) , CCC≽VariantList D
+  VariantList≋CCC _==_ D = ≽-trans (VariantList≽ADT _==_) (≽-trans ADT≽2CC 2CC≽CCC) , CCC≽VariantList D
 ```
 
 
@@ -244,11 +244,11 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f
   2CC-is-complete : Complete (2CCL F)
   2CC-is-complete = completeness-by-expressiveness CCC-is-complete 2CC≽CCC
 
-  2ADT-is-complete : Complete (2ADTL Variant F)
-  2ADT-is-complete = completeness-by-expressiveness 2CC-is-complete 2ADT≽2CC
+  ADT-is-complete : Complete (ADTL Variant F)
+  ADT-is-complete = completeness-by-expressiveness 2CC-is-complete ADT≽2CC
 
   NADT-is-complete : Complete (NADTL Variant F)
-  NADT-is-complete = completeness-by-expressiveness 2ADT-is-complete NADT≽2ADT
+  NADT-is-complete = completeness-by-expressiveness ADT-is-complete NADT≽ADT
 
   open OC.IncompleteOnRose using (OC-is-incomplete)
 
@@ -260,11 +260,11 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f
 ```
 
 ```agda
-2ADT-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (2ADTL Variant F)
-2ADT-is-sound {F} _==_ = soundness-by-expressiveness VariantList-is-Sound (2ADT-to-VariantList.VariantList≽2ADT F Variant _==_)
+ADT-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (ADTL Variant F)
+ADT-is-sound {F} _==_ = soundness-by-expressiveness VariantList-is-Sound (ADT-to-VariantList.VariantList≽ADT F Variant _==_)
 
 2CC-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (2CCL F)
-2CC-is-sound _==_ = soundness-by-expressiveness (2ADT-is-sound _==_) 2CC-to-2ADT.2ADT≽2CC
+2CC-is-sound _==_ = soundness-by-expressiveness (ADT-is-sound _==_) 2CC-to-ADT.ADT≽2CC
 
 NCC-is-sound : ∀ {F : 𝔽} (n : ℕ≥ 2) (_==_ : DecidableEquality F) → Sound (NCCL n F)
 NCC-is-sound n _==_ = soundness-by-expressiveness (2CC-is-sound (decidableEquality-× _==_ Fin._≟_)) (NCC-to-2CC.2CC≽NCC n)