blob: c032978e0c24e455bcffdc4681f0f0721f9bf315 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
{-# 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 aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where
field
Carrierᵢ : Set i
_≈ᵢ_ : B.Rel Carrierᵢ iℓ
isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_
F : Carrierᵢ → Language a 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
-- ≈ᵗ-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 = {!!}
-- }
-- }
|
