diff options
Diffstat (limited to 'src/Cfe/Language/Indexed/Homogeneous.agda')
| -rw-r--r-- | src/Cfe/Language/Indexed/Homogeneous.agda | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda index a1e284a..44e3b6c 100644 --- a/src/Cfe/Language/Indexed/Homogeneous.agda +++ b/src/Cfe/Language/Indexed/Homogeneous.agda @@ -16,18 +16,15 @@ open _≈_ open Setoid over using () renaming (Carrier to C) -record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where +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 aℓ + 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 - - _≈ᵗ_ : IRel Tagged (iℓ ⊔ aℓ) - _≈ᵗ_ (i , l∈Fi) (j , m∈Fj) = Σ (i ≈ᵢ j) λ i≈j → ≈ᴸ (F j) (f (cong i≈j) l∈Fi) m∈Fj |