Merge pull request #12 from pmbittner/benjamin/no-F

Remove the annotation language from `VariabilityLanguage`

src/Framework/V2/Compiler.agda

@@ -6,34 +6,34 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≗_)
 open import Data.Product using (_×_)
 open import Function using (id; _∘_)
 
-ConfigTranslation : ∀ (F₁ : 𝔽) (S₁ : 𝕊) (F₂ : 𝔽) (S₂ : 𝕊) → Set
-ConfigTranslation F₁ S₁ F₂ S₂ = S₁ F₁ → S₂ F₂
+ConfigTranslation : ∀ (S₁ : 𝕊) (S₂ : 𝕊) → Set
+ConfigTranslation S₁ S₂ = S₁ → S₂
 
-record ConfigCompiler (F₁ : 𝔽) (S₁ : 𝕊) (F₂ : 𝔽) (S₂ : 𝕊) : Set where
+record ConfigCompiler (S₁ : 𝕊) (S₂ : 𝕊) : Set where
   field
-    to   : ConfigTranslation F₁ S₁ F₂ S₂
-    from : ConfigTranslation F₂ S₂ F₁ S₁
+    to   : ConfigTranslation S₁ S₂
+    from : ConfigTranslation S₂ S₁
 open ConfigCompiler public
 
 {-|
 A translated configuration is extensionally equal.
 Fixme: Give me a proper name not this ugly one.
 -}
-ExtensionallyEqual-Translation : ∀ {F S Sel} → ConfigEvaluator F S Sel → ConfigTranslation F S F S → Set
+ExtensionallyEqual-Translation : ∀ {F S Sel} → ConfigEvaluator F S Sel → ConfigTranslation S S → Set
 ExtensionallyEqual-Translation evalConfig f = ∀ c → evalConfig (f c) ≗ evalConfig c
 
-ExtensionallyEqual : ∀ {F S Sel} → ConfigEvaluator F S Sel → ConfigCompiler F S F S → Set
+ExtensionallyEqual : ∀ {F S Sel} → ConfigEvaluator F S Sel → ConfigCompiler S S → Set
 ExtensionallyEqual {F} {S} evalConfig record { to = to ; from = from } =
   ExtensionallyEqual-Translation {F} {S} evalConfig to × ExtensionallyEqual-Translation {F} {S} evalConfig from
 
 -- We identify a configuration to be the same if it can be uniquely translated back
 -- (i.e., if `to` is an embedding into the second configuration language via its inverse `from`).
 -- We do not require the inverse direction `from`, being an embedding of configurations from `C₂` into `C₁`, because `C₂` could be larger than `C₁` (when interpreted as a set).
 -- For example, the set of features in `C₂` could be bigger (e.g., when going from core choice calculus to binary choice calculus) but all information can be derived by `conf` from our initial configuration `c₁`.
-Stable : ∀ {F₁ S₁ F₂ S₂} → ConfigCompiler F₁ S₁ F₂ S₂ → Set
+Stable : ∀ {S₁ S₂} → ConfigCompiler S₁ S₂ → Set
 Stable cc = from cc ∘ to cc ≗ id
 
-record LanguageCompiler {V F₁ F₂ S₁ S₂} (Γ₁ : VariabilityLanguage V F₁ S₁) (Γ₂ : VariabilityLanguage V F₂ S₂) : Set₁ where
+record LanguageCompiler {V S₁ S₂} (Γ₁ : VariabilityLanguage V S₁) (Γ₂ : VariabilityLanguage V S₂) : Set₁ where
   private
     L₁ = Expression Γ₁
     L₂ = Expression Γ₂
@@ -42,7 +42,7 @@ record LanguageCompiler {V F₁ F₂ S₁ S₂} (Γ₁ : VariabilityLanguage V F
 
   field
     compile         : ∀ {A} → L₁ A → L₂ A
-    config-compiler : ConfigCompiler F₁ S₁ F₂ S₂
+    config-compiler : ConfigCompiler S₁ S₂
     preserves : ∀ {A} → let open IVSet V A using (_≅[_][_]_) in
                 ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂
                 -- TODO: It might nice to have syntax
@@ -58,16 +58,16 @@ record LanguageCompiler {V F₁ F₂ S₁ S₂} (Γ₁ : VariabilityLanguage V F
 --        To preserve semantics, most of the time, additional requirements on the
 --        config translations are required which are currently not part of the
 --        preservation theorem here. Maybe we have to add these constraints as type parameters here?
-record ConstructCompiler {V F₁ S₁ F₂ S₂} (VC₁ : VariabilityConstruct V F₁ S₁) (VC₂ : VariabilityConstruct V F₂ S₂) : Set₁ where
+record ConstructCompiler {V S₁ S₂} (VC₁ : VariabilityConstruct V S₁) (VC₂ : VariabilityConstruct V S₂) : Set₁ where
   open VariabilityConstruct VC₁ renaming (Construct to C₁; construct-semantics to sem₁)
   open VariabilityConstruct VC₂ renaming (Construct to C₂; construct-semantics to sem₂)
 
   field
-    compile : ∀ {E A} → C₁ F₁ E A → C₂ F₂ E A
-    config-compiler : ConfigCompiler F₁ S₁ F₂ S₂
+    compile : ∀ {E A} → C₁ E A → C₂ E A
+    config-compiler : ConfigCompiler S₁ S₂
     stable : Stable config-compiler
-    preserves : ∀ {Γ : VariabilityLanguage V F₁ S₁} {A}
-      → (c : C₁ F₁ (Expression Γ) A)
+    preserves : ∀ {Γ : VariabilityLanguage V S₁} {A}
+      → (c : C₁ (Expression Γ) A)
       → let open IVSet V A using (_≅_) in
         sem₁ id Γ c ≅ sem₂ (to config-compiler) Γ (compile c)
 
@@ -76,36 +76,36 @@ Compiles languages below constructs.
 This means that an expression in a language Γ₁ of which we know that it has a specific
 syntactic construct VC at the top is compiled to Γ₂ retaining the very same construct at the top.
 -}
-record ConstructFunctor {V F S} (VC : VariabilityConstruct V F S) : Set₁ where
+record ConstructFunctor {V S} (VC : VariabilityConstruct V S) : Set₁ where
   open VariabilityConstruct VC
   open LanguageCompiler using (conf; fnoc; compile; config-compiler)
 
   field
     map : ∀ {A} {L₁ L₂ : 𝔼}
       → (L₁ A → L₂ A)
-      → Construct F L₁ A
-      → Construct F L₂ A
-    preserves : ∀ {F'} {S'} {Γ₁ : VariabilityLanguage V F S} {Γ₂ : VariabilityLanguage V F' S'} {A}
+      → Construct L₁ A
+      → Construct L₂ A
+    preserves : ∀ {S'} {Γ₁ : VariabilityLanguage V S} {Γ₂ : VariabilityLanguage V S'} {A}
       → let open IVSet V A using (_≅[_][_]_) in
       ∀ (t : LanguageCompiler Γ₁ Γ₂)
-      → (c : Construct F (Expression Γ₁) A)
+      → (c : Construct (Expression Γ₁) A)
       → Stable (config-compiler t)
       → construct-semantics id Γ₁ c
           ≅[ conf t ][ fnoc t ]
         construct-semantics (fnoc t) Γ₂ (map (compile t) c)
 
-_⊕ᶜᶜ_ : ∀ {F₁ F₂ F₃} {S₁ S₂ S₃}
-  → ConfigCompiler F₁ S₁ F₂ S₂
-  → ConfigCompiler F₂ S₂ F₃ S₃
-  → ConfigCompiler F₁ S₁ F₃ S₃
+_⊕ᶜᶜ_ : ∀ {S₁ S₂ S₃}
+  → ConfigCompiler S₁ S₂
+  → ConfigCompiler S₂ S₃
+  → ConfigCompiler S₁ S₃
 1→2 ⊕ᶜᶜ 2→3 = record
   { to   = to   2→3 ∘ to   1→2
   ; from = from 1→2 ∘ from 2→3
   }
 
 ⊕ᶜᶜ-stable :
-  ∀ {F₁ F₂ F₃} {S₁ S₂ S₃}
-    (1→2 : ConfigCompiler F₁ S₁ F₂ S₂) (2→3 : ConfigCompiler F₂ S₂ F₃ S₃)
+  ∀ {S₁ S₂ S₃}
+    (1→2 : ConfigCompiler S₁ S₂) (2→3 : ConfigCompiler S₂ S₃)
   → Stable 1→2
   → Stable 2→3
     --------------------
@@ -124,14 +124,14 @@ _⊕ᶜᶜ_ : ∀ {F₁ F₂ F₃} {S₁ S₂ S₃}
     id c₁
   ∎
 
-_⊕ˡ_ : ∀ {V} {F₁ F₂ F₃} {S₁ S₂ S₃}
-        {Γ₁ : VariabilityLanguage V F₁ S₁}
-        {Γ₂ : VariabilityLanguage V F₂ S₂}
-        {Γ₃ : VariabilityLanguage V F₃ S₃}
+_⊕ˡ_ : ∀ {V} {S₁ S₂ S₃}
+        {Γ₁ : VariabilityLanguage V S₁}
+        {Γ₂ : VariabilityLanguage V S₂}
+        {Γ₃ : VariabilityLanguage V S₃}
       → LanguageCompiler Γ₁ Γ₂
       → LanguageCompiler Γ₂ Γ₃
       → LanguageCompiler Γ₁ Γ₃
-_⊕ˡ_ {V} {F₁} {F₂} {F₃} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record
+_⊕ˡ_ {V} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record
   { compile = compile L₂→L₃ ∘ compile L₁→L₂
   ; config-compiler = record { to = conf'; from = fnoc' }
   ; preserves = p
@@ -141,10 +141,10 @@ _⊕ˡ_ {V} {F₁} {F₂} {F₃} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L
         ⟦_⟧₁ = Semantics Γ₁
         ⟦_⟧₃ = Semantics Γ₃
 
-        conf' : S₁ F₁ → S₃ F₃
+        conf' : S₁ → S₃
         conf' = conf L₂→L₃ ∘ conf L₁→L₂
 
-        fnoc' : S₃ F₃ → S₁ F₁
+        fnoc' : S₃ → S₁
         fnoc' = fnoc L₁→L₂ ∘ fnoc L₂→L₃
 
         module _ {A : 𝔸} where
@@ -154,11 +154,11 @@ _⊕ˡ_ {V} {F₁} {F₂} {F₃} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L
           p : ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' ][ fnoc' ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃
           p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e))
 
--- _⊕ᶜ_ : ∀ {F S} {VC₁ VC₂ VC₃ : VariabilityConstruct F S}
+-- _⊕ᶜ_ : ∀ {S} {VC₁ VC₂ VC₃ : VariabilityConstruct S}
 --   → ConstructCompiler VC₁ VC₂
 --   → ConstructCompiler VC₂ VC₃
 --   → ConstructCompiler VC₁ VC₃
--- _⊕ᶜ_ {F} {S} {VC₁} {_} {VC₃} 1→2 2→3 = record
+-- _⊕ᶜ_ {S} {VC₁} {_} {VC₃} 1→2 2→3 = record
 --   { compile = compile 2→3 ∘ compile 1→2
 --   ; config-compiler = cc
 --   ; stable = stb
@@ -168,7 +168,7 @@ _⊕ˡ_ {V} {F₁} {F₂} {F₃} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L
 --         open VariabilityConstruct VC₁ renaming (Construct to C₁; construct-semantics to sem₁)
 --         open VariabilityConstruct VC₃ renaming (construct-semantics to sem₃)
 
---         cc : ConfigCompiler F S F S
+--         cc : ConfigCompiler S S
 --         cc = config-compiler 1→2 ⊕ᶜᶜ config-compiler 2→3
 
 --         stb : Stable cc
@@ -177,8 +177,8 @@ _⊕ˡ_ {V} {F₁} {F₂} {F₃} {S₁} {S₂} {S₃} {Γ₁} {Γ₂} {Γ₃} L
 --         module Pres {V : 𝕍} {A : 𝔸} where
 --           open IVSet V A using (_≅_; ≅-trans)
 
---           p : ∀ {Γ : VariabilityLanguage V F S}
---               → (c : C₁ F (Expression Γ) A)
+--           p : ∀ {Γ : VariabilityLanguage V S}
+--               → (c : C₁ (Expression Γ) A)
 --               → sem₁ Γ id c ≅ sem₃ Γ (to cc) (compile 2→3 (compile 1→2 c))
 --           p c = ≅-trans (preserves 1→2 c) {!preserves 2→3 (compile 1→2 c)!} --
 --           -- p c₁ = ≅-trans (preserves 1→2 c₁) (preserves 2→3 (compile 1→2 c₁))

src/Framework/V2/Constructs/Artifact.agda

@@ -16,23 +16,23 @@ import Data.IndexedSet
 open import Framework.V2.Constructs.Plain.Artifact public
 
 Syntax : ℂ
-Syntax _ E A = Artifact A (E A)
+Syntax E A = Artifact A (E A)
 
-Semantics : ∀ {V : 𝕍} (F : 𝔽) (S : 𝕊)
-  → F ⊢ Syntax ∈ₛ V
-  → ℂ-Semantics V F S Syntax
-Semantics _ _ V-has-Artifact conf-comp (syn _ with-sem ⟦_⟧) a c
+Semantics : ∀ {V : 𝕍} (S : 𝕊)
+  → Syntax ∈ₛ V
+  → ℂ-Semantics V S Syntax
+Semantics _ V-has-Artifact conf-comp (syn _ with-sem ⟦_⟧) a c
   = cons V-has-Artifact (map-children (λ e → ⟦ e ⟧ c) a)
 
-map-children-preserves : ∀ {V : 𝕍} {F₁ F₂ : 𝔽} {S₁ S₂ : 𝕊} {Γ₁ : VariabilityLanguage V F₁ S₁} {Γ₂ : VariabilityLanguage V F₂ S₂} {A}
+map-children-preserves : ∀ {V : 𝕍} {S₁ S₂ : 𝕊} {Γ₁ : VariabilityLanguage V S₁} {Γ₂ : VariabilityLanguage V S₂} {A}
   → let open IVSet V A using (_≅_; _≅[_][_]_) in
-  ∀ (mkArtifact : F₁ ⊢ Syntax ∈ₛ V)
+  ∀ (mkArtifact : Syntax ∈ₛ V)
   → (t : LanguageCompiler Γ₁ Γ₂)
-  → (at : Syntax F₁ (Expression Γ₁) A)
-  → Semantics F₁ S₁ mkArtifact id Γ₁ at
+  → (at : Syntax (Expression Γ₁) A)
+  → Semantics S₁ mkArtifact id Γ₁ at
       ≅[ conf t ][ fnoc t ]
-    Semantics F₁ S₁ mkArtifact (fnoc t) Γ₂ (map-children (compile t) at)
-map-children-preserves {V} {F₁} {F₂} {S₁} {S₂} {Γ₁} {Γ₂} {A} mkArtifact t (a -< cs >-) =
+    Semantics S₁ mkArtifact (fnoc t) Γ₂ (map-children (compile t) at)
+map-children-preserves {V} {S₁} {S₂} {Γ₁} {Γ₂} {A} mkArtifact t (a -< cs >-) =
     ≅[]-begin
       (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₁ c) cs >-))
     ≅[]⟨ t-⊆ , t-⊇ ⟩

src/Framework/V2/Constructs/Choices.agda

@@ -171,26 +171,26 @@ module VLChoice₂ where
   open import Framework.V2.Compiler as Comp using (LanguageCompiler; ConfigTranslation; ConstructFunctor; Stable)
   open LanguageCompiler
 
-  Syntax : ℂ
+  Syntax : 𝔽 → ℂ
   Syntax F E A = Choice₂.Syntax F (E A)
 
-  Semantics : ∀ (V : 𝕍) (F : 𝔽) → ℂ-Semantics V F Config Syntax
+  Semantics : ∀ (V : 𝕍) (F : 𝔽) → ℂ-Semantics V (Config F) (Syntax F)
   Semantics _ _ fnoc (syn _ with-sem ⟦_⟧) chc c = ⟦ Standard-Semantics chc (fnoc c) ⟧ c
 
-  Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V F Config
-  Construct V F = con Syntax with-sem Semantics V F
+  Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V (Config F)
+  Construct V F = con Syntax F with-sem Semantics V F
 
-  map-compile-preserves : ∀ {V} {F₁ F₂ : 𝔽} {S₂ : 𝕊} {Γ₁ : VariabilityLanguage V F₁ Config} {Γ₂ : VariabilityLanguage V F₂ S₂} {A}
+  map-compile-preserves : ∀ {V} {F : 𝔽} {S₂ : 𝕊} {Γ₁ : VariabilityLanguage V (Config F)} {Γ₂ : VariabilityLanguage V S₂} {A}
     → let open IVSet V A using (_≅_; _≅[_][_]_) in
     ∀ (t : LanguageCompiler Γ₁ Γ₂)
-    → (chc : Syntax F₁ (Expression Γ₁) A)
+    → (chc : Syntax F (Expression Γ₁) A)
     → Stable (config-compiler t)
-    → Semantics V F₁ id Γ₁ chc
+    → Semantics V F id Γ₁ chc
         ≅[ conf t ][ fnoc t ]
-      Semantics V F₁ (fnoc t) Γ₂ (map (compile t) chc)
-  map-compile-preserves {V} {F₁} {_} {_} {Γ₁} {Γ₂} {A} t chc stable =
+      Semantics V F (fnoc t) Γ₂ (map (compile t) chc)
+  map-compile-preserves {V} {F} {_} {Γ₁} {Γ₂} {A} t chc stable =
     ≅[]-begin
-      Semantics V F₁ id Γ₁ chc
+      Semantics V F id Γ₁ chc
     ≅[]⟨⟩
       (λ c → ⟦ Standard-Semantics chc c ⟧₁ c)
     -- First compiler proof composition:
@@ -203,7 +203,7 @@ module VLChoice₂ where
     ≐˘[ c ]⟨ Eq.cong (λ x → ⟦ x ⟧₂ c) (map-preserves (compile t) chc (fnoc t c)) ⟩
       (λ c → ⟦ Standard-Semantics (map (compile t) chc) (fnoc t c) ⟧₂ c)
     ≅[]⟨⟩
-      Semantics V F₁ (fnoc t) Γ₂ (map (compile t) chc)
+      Semantics V F (fnoc t) Γ₂ (map (compile t) chc)
     ≅[]-∎
     where module I = IVSet V A
           open I using (_≅[_][_]_; _⊆[_]_)
@@ -251,32 +251,32 @@ module VLChoiceₙ where
   open import Framework.V2.Compiler as Comp using (LanguageCompiler; ConfigTranslation; ConstructFunctor; Stable)
   open LanguageCompiler
 
-  Syntax : ℂ
+  Syntax : 𝔽 → ℂ
   Syntax F E A = Choiceₙ.Syntax F (E A)
 
-  Semantics : ∀ (V : 𝕍) (F : 𝔽) → ℂ-Semantics V F Config Syntax
+  Semantics : ∀ (V : 𝕍) (F : 𝔽) → ℂ-Semantics V (Config F) (Syntax F)
   Semantics _ _ fnoc (syn E with-sem ⟦_⟧) choice c = ⟦ Choiceₙ.Standard-Semantics choice (fnoc c) ⟧ c
 
-  Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V F Config
-  Construct V F = con Syntax with-sem Semantics V F
+  Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V (Config F)
+  Construct V F = con Syntax F with-sem Semantics V F
 
   -- Interestingly, this proof is entirely copy and paste from VLChoice₂.map-compile-preserves.
   -- Only minor adjustments to adapt the theorem had to be made.
   -- Is there something useful to extract to a common definition here?
   -- This proof is oblivious of at least
   --   - the implementation of map, we only need the preservation theorem
   --   - the Standard-Semantics, we only need the preservation theorem of t, and that the config-compiler is stable.
-  map-compile-preserves : ∀ {V} {F₁ F₂ : 𝔽} {S₂ : 𝕊} {Γ₁ : VariabilityLanguage V F₁ Config} {Γ₂ : VariabilityLanguage V F₂ S₂} {A}
+  map-compile-preserves : ∀ {V} {F : 𝔽} {S₂ : 𝕊} {Γ₁ : VariabilityLanguage V (Config F)} {Γ₂ : VariabilityLanguage V S₂} {A}
     → let open IVSet V A using (_≅_; _≅[_][_]_) in
     ∀ (t : LanguageCompiler Γ₁ Γ₂)
-    → (chc : Syntax F₁ (Expression Γ₁) A)
+    → (chc : Syntax F (Expression Γ₁) A)
     → Stable (config-compiler t)
-    → Semantics V F₁ id Γ₁ chc
+    → Semantics V F id Γ₁ chc
         ≅[ conf t ][ fnoc t ]
-      Semantics V F₁ (fnoc t) Γ₂ (map (compile t) chc)
-  map-compile-preserves {V} {F₁} {_} {_} {Γ₁} {Γ₂} {A} t chc stable =
+      Semantics V F (fnoc t) Γ₂ (map (compile t) chc)
+  map-compile-preserves {V} {F} {_} {Γ₁} {Γ₂} {A} t chc stable =
     ≅[]-begin
-      Semantics V F₁ id Γ₁ chc
+      Semantics V F id Γ₁ chc
     ≅[]⟨⟩
       (λ c → ⟦ Standard-Semantics chc c ⟧₁ c)
     -- First compiler proof composition:
@@ -289,7 +289,7 @@ module VLChoiceₙ where
     ≐˘[ c ]⟨ Eq.cong (λ x → ⟦ x ⟧₂ c) (map-preserves (compile t) chc (fnoc t c)) ⟩
       (λ c → ⟦ Standard-Semantics (map (compile t) chc) (fnoc t c) ⟧₂ c)
     ≅[]⟨⟩
-      Semantics V F₁ (fnoc t) Γ₂ (map (compile t) chc)
+      Semantics V F (fnoc t) Γ₂ (map (compile t) chc)
     ≅[]-∎
     where module I = IVSet V A
           open I using (_≅[_][_]_; _⊆[_]_)

src/Framework/V2/Constructs/GrulerArtifacts.agda

@@ -19,50 +19,50 @@ record ParallelComposition {ℓ} (A : Set ℓ) : Set ℓ where
 
 module VLLeaf where
   Syntax : ℂ
-  Syntax _ _ A = Leaf A
+  Syntax _ A = Leaf A
 
   make-leaf :
-    ∀ {F : 𝔽} {E : 𝔼} → F ⊢ Syntax ∈ₛ E
+    ∀ {E : 𝔼} → Syntax ∈ₛ E
     → {A : 𝔸} → A
     → E A
   make-leaf mkLeaf a = cons mkLeaf (leaf a)
 
-  elim-leaf : ∀ {V} (F : 𝔽) → F ⊢ Syntax ∈ₛ V → ∀ {A} → Leaf A → V A
-  elim-leaf _ leaf∈V l = cons leaf∈V l
+  elim-leaf : ∀ {V} → Syntax ∈ₛ V → ∀ {A} → Leaf A → V A
+  elim-leaf leaf∈V l = cons leaf∈V l
 
-  Semantics : ∀ {V F S} → F ⊢ Syntax ∈ₛ V → ℂ-Semantics V F S Syntax
-  Semantics {F = F} leaf∈V _ _ l _ = elim-leaf F leaf∈V l
+  Semantics : ∀ {V S} → Syntax ∈ₛ V → ℂ-Semantics V S Syntax
+  Semantics {V} leaf∈V _ _ l _ = elim-leaf {V} leaf∈V l
 
-  Construct : ∀ (V : 𝕍) (F : 𝔽) (S : 𝕊)
-    → F ⊢ Syntax ∈ₛ V
-    → VariabilityConstruct V F S
-  Construct V F S mkLeaf = record
+  Construct : ∀ (V : 𝕍) (S : 𝕊)
+    → Syntax ∈ₛ V
+    → VariabilityConstruct V S
+  Construct V S mkLeaf = record
     { Construct = Syntax
-    ; construct-semantics = Semantics {V} {F} {S} mkLeaf
+    ; construct-semantics = Semantics {V} {S} mkLeaf
     }
 
-  Leaf∈ₛGrulerVariant : ∀ {F} → F ⊢ Syntax ∈ₛ GrulerVariant
+  Leaf∈ₛGrulerVariant : Syntax ∈ₛ GrulerVariant
   cons Leaf∈ₛGrulerVariant (leaf a) = asset a
   snoc Leaf∈ₛGrulerVariant (asset a) = just (leaf a)
   snoc Leaf∈ₛGrulerVariant (_ ∥ _) = nothing
   id-l Leaf∈ₛGrulerVariant (leaf _) = refl
 
 module VLParallelComposition where
   Syntax : ℂ
-  Syntax _ E A = ParallelComposition (E A)
+  Syntax E A = ParallelComposition (E A)
 
-  Semantics : ∀ {V : 𝕍} {F : 𝔽} {S : 𝕊} → F ⊢ Syntax ∈ₛ V → ℂ-Semantics V F S Syntax
+  Semantics : ∀ {V : 𝕍} {S : 𝕊} → Syntax ∈ₛ V → ℂ-Semantics V S Syntax
   Semantics leaf∈V _ (syn E with-sem ⟦_⟧) (l ∥ r) c = cons leaf∈V (⟦ l ⟧ c ∥ ⟦ r ⟧ c)
 
-  Construct : ∀ (V : 𝕍) (F : 𝔽) (S : 𝕊)
-    → F ⊢ Syntax ∈ₛ V
-    → VariabilityConstruct V F S
-  Construct V F S mkPC = record
+  Construct : ∀ (V : 𝕍) (S : 𝕊)
+    → Syntax ∈ₛ V
+    → VariabilityConstruct V S
+  Construct V S mkPC = record
     { Construct = Syntax
-    ; construct-semantics = Semantics {V} {F} {S} mkPC
+    ; construct-semantics = Semantics {V} {S} mkPC
     }
 
-  ParallelComposition∈ₛGrulerVariant : ∀ {F} → F ⊢ Syntax ∈ₛ GrulerVariant
+  ParallelComposition∈ₛGrulerVariant : Syntax ∈ₛ GrulerVariant
   cons ParallelComposition∈ₛGrulerVariant (l ∥ r) = l ∥ r
   snoc ParallelComposition∈ₛGrulerVariant (asset a) = nothing
   snoc ParallelComposition∈ₛGrulerVariant (l ∥ r) = just (l ∥ r)