From da429008d25ac87ec67a4fb18a5cbee0ba756bcf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 5 Apr 2021 14:31:57 +0100
Subject: Clean-up Language hierarchy.

---
 src/Cfe/Language/Indexed/Homogeneous.agda | 30 ------------------------------
 1 file changed, 30 deletions(-)
 delete mode 100644 src/Cfe/Language/Indexed/Homogeneous.agda

(limited to 'src/Cfe/Language/Indexed/Homogeneous.agda')

diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda
deleted file mode 100644
index 44e3b6c..0000000
--- a/src/Cfe/Language/Indexed/Homogeneous.agda
+++ /dev/null
@@ -1,30 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary as B using (Setoid)
-
-module Cfe.Language.Indexed.Homogeneous
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open import Cfe.Language over
-open import Level
-open import Data.List
-open import Data.Product
-open import Relation.Binary.Indexed.Heterogeneous
-
-open _≈_
-
-open Setoid over using () renaming (Carrier to C)
-
-record IndexedLanguage i iℓ a : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a)) where
-  field
-    Carrierᵢ : Set i
-    _≈ᵢ_ : B.Rel Carrierᵢ iℓ
-    isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_
-    F : Carrierᵢ → Language a
-    cong : F B.Preserves _≈ᵢ_ ⟶ _≈_
-
-  open B.IsEquivalence isEquivalenceᵢ using () renaming (refl to reflᵢ; sym to symᵢ; trans to transᵢ) public
-
-  Tagged : List C → Set (i ⊔ a)
-  Tagged l = ∃[ i ] l ∈ F i
-- 
cgit v1.2.3