From 02a0f87be944b1d43fda265058b891f419d25b65 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 16 Mar 2021 18:45:27 +0000 Subject: Change Language definition to respects instead of custom congruence. --- src/Cfe/Language/Indexed/Homogeneous.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'src/Cfe/Language/Indexed/Homogeneous.agda') 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 -- cgit v1.2.3