diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 00:00:04 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-05 00:04:46 +0000 |
| commit | 5302e4a27a64cb2a97120517df4b6998da7b3168 (patch) | |
| tree | ebe15b37e27e8ec7e4920200e15a40ae586bedbc /src/Cfe/Language/Indexed/Homogeneous.agda | |
| parent | ff3600687249a19ae63353f7791b137094f5a5a1 (diff) | |
Complete proofs up to Proposition 3.2 (excluding unrolling)
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 = {!!} - -- } - -- } |