diff options
Diffstat (limited to 'src/Cfe/Language/Indexed/Homogeneous.agda')
| -rw-r--r-- | src/Cfe/Language/Indexed/Homogeneous.agda | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda index c032978..a1e284a 100644 --- a/src/Cfe/Language/Indexed/Homogeneous.agda +++ b/src/Cfe/Language/Indexed/Homogeneous.agda @@ -31,17 +31,3 @@ record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a _≈ᵗ_ : IRel Tagged (iℓ ⊔ aℓ) _≈ᵗ_ (i , l∈Fi) (j , m∈Fj) = Σ (i ≈ᵢ j) λ i≈j → ≈ᴸ (F j) (f (cong i≈j) l∈Fi) m∈Fj - - -- ≈ᵗ-refl : Reflexive Tagged _≈ᵗ_ - -- ≈ᵗ-refl {l} {i , l∈Fi} = reflᵢ , {!≈ᴸ-refl!} - - -- ⋃ : Language (i ⊔ a) (iℓ ⊔ aℓ) - -- ⋃ = record - -- { Carrier = Tagged - -- ; _≈_ = _≈ᵗ_ - -- ; isEquivalence = record - -- { refl = λ i≈j → {!!} - -- ; sym = {!!} - -- ; trans = {!!} - -- } - -- } |