rename 𝕂 to ℂ

Author: pmbittner

README.md

@@ -352,7 +352,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
 | Definition 4.8  | Non-empty Indexed Set             | `empty`                                                            | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md)                                         | The library definition is a predicate that ensures an indexed set to be non-empty.                                                                                 |
 | Definition 4.9  | Variant Map                       | `VMap`                                                             | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda)                                       | This is the finite and non-empty indexed set definition mentioned above.                                                                                           |
 | Definition 4.10 | Semantic Domain                   | `VMap`                                                             | [src/Framework/VariantMap.agda](src/Framework/VariantMap.agda)                                       | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements.                                                             |
-| Definition 4.11 | configuration language 𝐶          | `𝕂`                                                                | [src/Framework/Definitions.agda](src/Framework/Definitions.agda)                                     |                                                                                                                                                                    | -- TODO Use C instead of K if constructors are removed completely
+| Definition 4.11 | configuration language 𝐶          | `ℂ`                                                                | [src/Framework/Definitions.agda](src/Framework/Definitions.agda)                                     |                                                                                                                                                                    |
 | Definition 4.12 | variability language 𝐿            | `𝔼`                                                                | [src/Framework/Definitions.agda](src/Framework/Definitions.agda)                                     |                                                                                                                                                                    |
 | Definition 4.13 | ⟦.⟧                               | `𝔼-Semantics`                                                      | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md)             |                                                                                                                                                                    |
 |                 |                                   | `VariabilityLanguage`                                              | [src/Framework/VariabilityLanguage.lagda.md](src/Framework/VariabilityLanguage.lagda.md)             | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics.                                                                                                           |

src/Framework/Compiler.agda

@@ -37,7 +37,7 @@ record LanguageCompiler {V} (Γ₁ Γ₂ : VariabilityLanguage V) : Set₁ where
   fnoc : ∀ {A} → L₁ A → Config Γ₂ → Config Γ₁
   fnoc e = from (config-compiler e)
 
-_⊕ᶜᶜ_ : ∀ {K₁ K₂ K₃ : 𝕂}
+_⊕ᶜᶜ_ : ∀ {K₁ K₂ K₃ : ℂ}
   → K₁ ⇔ K₂
   → K₂ ⇔ K₃
   → K₁ ⇔ K₃
@@ -47,7 +47,7 @@ _⊕ᶜᶜ_ : ∀ {K₁ K₂ K₃ : 𝕂}
   }
 
 ⊕ᶜᶜ-stable :
-  ∀ {K₁ K₂ K₃ : 𝕂}
+  ∀ {K₁ K₂ K₃ : ℂ}
     (1→2 : K₁ ⇔ K₂) (2→3 : K₂ ⇔ K₃)
   → to-is-Embedding 1→2
   → to-is-Embedding 2→3

src/Framework/Definitions.agda

@@ -61,8 +61,8 @@ selections language.
 𝕊 = Set
 
 -- Set of configuration languages
-𝕂 : Set₁
-𝕂 = Set
+ℂ : Set₁
+ℂ = Set
 
 {-
 The set of expressions of a variability language.

src/Framework/VariabilityLanguage.lagda.md

@@ -11,14 +11,14 @@ We model this set in terms of a function (see IndexedSet).
 Hence, the semantics is a function that configures an expression
 `e : E A` to a variant `v : V A` for any domain `A : 𝔸`.
 ```agda
-𝔼-Semantics : 𝕍 → 𝕂 → 𝔼 → Set₁
+𝔼-Semantics : 𝕍 → ℂ → 𝔼 → Set₁
 𝔼-Semantics V K E = ∀ {A : 𝔸} → E A → K → V A
 
 record VariabilityLanguage (V : 𝕍) : Set₂ where
   constructor ⟪_,_,_⟫
   field
     Expression : 𝔼
-    Config     : 𝕂
+    Config     : ℂ
     Semantics  : 𝔼-Semantics V Config Expression
 open VariabilityLanguage public
 ```

src/Lang/2CC.lagda.md

@@ -52,7 +52,7 @@ We define `true` to mean choosing the left alternative and `false` to choose the
 Defining it the other way around is also possible but we have to pick one definition and stay consistent.
 We choose this order to follow the known _if c then a else b_ pattern where the evaluation of a condition _c_ to true means choosing the then-branch, which is the left one.
 ```agda
-Configuration : (Dimension : 𝔽) → 𝕂
+Configuration : (Dimension : 𝔽) → ℂ
 Configuration Dimension = Dimension → Bool
 
 ⟦_⟧ : ∀ {i : Size} {Dimension : 𝔽} → 𝔼-Semantics (Rose ∞) (Configuration Dimension) (2CC Dimension i)

src/Lang/CCC.lagda.md

@@ -51,7 +51,7 @@ Thus, and for much simpler proofs, we choose the functional semantics.
 
 First, we define configurations as functions that evaluate dimensions by tags:
 ```agda
-Configuration : (Dimension : 𝔽) → 𝕂
+Configuration : (Dimension : 𝔽) → ℂ
 Configuration Dimension = Dimension → ℕ
 ```
 

src/Lang/NCC.lagda.md

@@ -46,7 +46,7 @@ data NCC (n : ℕ≥ 2) (Dimension : 𝔽) : Size → 𝔼 where
 ## Semantics
 
 ```agda
-Configuration : (n : ℕ≥ 2) → (Dimension : 𝔽) → 𝕂
+Configuration : (n : ℕ≥ 2) → (Dimension : 𝔽) → ℂ
 Configuration n Dimension = Dimension → Fin (ℕ≥.toℕ n)
 
 ⟦_⟧ : ∀ {i : Size} {Dimension : 𝔽} {n : ℕ≥ 2} → 𝔼-Semantics (Rose ∞) (Configuration n Dimension) (NCC n Dimension i)

src/Lang/OC.lagda.md

@@ -77,7 +77,7 @@ children-wf (Root _ es) = es
 
 Let's first define configurations. Configurations of option calculus tell us which options to in- or exclude. We define `true` to mean "include" and `false` to mean "exclude". Defining it the other way around would also be fine as long as we are consistent. Yet, our way of defining it is in line with if-semantics and how it is usually implemented in papers and tools.
 ```agda
-Configuration : 𝔽 → 𝕂
+Configuration : 𝔽 → ℂ
 Configuration Option = Option → Bool
 ```