module AlgebraicSignature where
open import InitialAlgebra public
open import Prelude public
open import Size
record Sig : Set₁ where
constructor mkSig
field
Op : Set
Ar : Op → Set
open Sig public
data 𝕎 (Σ : Sig) : Set where
sup : (a : Op Σ) → (Ar Σ a → 𝕎 Σ) → 𝕎 Σ
infixr 6 _⊕_
_⊕_ : Sig → Sig → Sig
Op (Σ ⊕ Σ') = Op Σ ⊎ Op Σ'
Ar (Σ ⊕ Σ') (ι₁ a) = Ar Σ a
Ar (Σ ⊕ Σ') (ι₂ a') = Ar Σ' a'
⨁ : (A : Set)(B : A → Sig) → Sig
Op (⨁ A Σ) = ∑ x ∶ A , Op (Σ x)
Ar (⨁ A Σ) (x , a) = Ar (Σ x) a
syntax ⨁ A (λ x → Σ) = ⨁ x ∶ A , Σ
emp : Sig
Op emp = 𝟘
Ar emp ()
bin : Sig
Op bin = 𝔹
Ar bin false = 𝟘
Ar bin true = 𝔹
record Filtered
(Σ : Sig)
(κ : Set)
{{_ : Size κ}}
:
Set₁
where
field
⨆ˢ : (a : Op Σ)(f : Ar Σ a → κ) → κ
<⨆ˢ :
{a : Op Σ}
(f : Ar Σ a → κ)
(x : Ar Σ a)
→
f x < ⨆ˢ a f
<ᵇ⨆ˢ :
{a : Op Σ}
(f : Ar Σ a → κ)
(x : Ar Σ a)
→
f x <ᵇ ⨆ˢ a f
<ᵇ⨆ˢ f x = <inst (<⨆ˢ f x)
open Filtered{{...}} public
Filtered⨁ :
(κ : Set)
{{_ : Size κ}}
(A : Set)
(Σ : A → Sig)
{{_ : Filtered (⨁ A Σ) κ}}
(x : A)
→
Filtered (Σ x) κ
⨆ˢ {{Filtered⨁ _ _ _ x}} a = ⨆ˢ (x , a)
<⨆ˢ{{Filtered⨁ _ _ _ _}} = <⨆ˢ
Filtered⊕l :
(κ : Set)
{{_ : Size κ}}
(Σ Σ' : Sig)
{{_ : Filtered (Σ ⊕ Σ') κ}}
→
Filtered Σ κ
⨆ˢ {{Filtered⊕l _ _ _}} a = ⨆ˢ (ι₁ a)
<⨆ˢ {{Filtered⊕l _ _ _}} = <⨆ˢ
Filtered⊕r :
(κ : Set)
{{_ : Size κ}}
(Σ Σ' : Sig)
{{_ : Filtered (Σ ⊕ Σ') κ}}
→
Filtered Σ' κ
⨆ˢ {{Filtered⊕r _ _ _}} a = ⨆ˢ (ι₂ a)
<⨆ˢ {{Filtered⊕r _ _ _}} = <⨆ˢ
module _ {Σ : Sig} where
infix 4 _≼_ _≺_
mutual
data _≼_ : 𝕎 Σ → 𝕎 Σ → Prop where
sup≼ :
{a : Op Σ}
{f : Ar Σ a → 𝕎 Σ}
{i : 𝕎 Σ}
(f<i : ∀ x → f x ≺ i)
→
sup a f ≼ i
data _≺_ : 𝕎 Σ → 𝕎 Σ → Prop where
≺sup :
{a : Op Σ}
{f : Ar Σ a → 𝕎 Σ}
(x : Ar Σ a)
{i : 𝕎 Σ}
(i≼fx : i ≼ f x)
→
i ≺ sup a f
≼refl : ∀ i → i ≼ i
≼refl (sup _ f) = sup≼ λ x → ≺sup x (≼refl (f x))
mutual
≼≼ : ∀{i j k} → j ≼ k → i ≼ j → i ≼ k
≼≼ j≼k (sup≼ f≺i) = sup≼ λ x → ≼≺ j≼k (f≺i x)
≼≺ : ∀{i j k} → j ≼ k → i ≺ j → i ≺ k
≼≺ (sup≼ f≺i) (≺sup x i≼fx) = ≺≼ (f≺i x) i≼fx
≺≼ : ∀{i j k } → j ≺ k → i ≼ j → i ≺ k
≺≼ (≺sup x i≼fx) i≼j = ≺sup x (≼≼ i≼fx i≼j)
≺→≼ : ∀{i j} → i ≺ j → i ≼ j
≺→≼ (≺sup x (sup≼ f≺i)) = sup≼ (λ y → ≺sup x (≺→≼ (f≺i y)))
≺≺ : ∀{i j k} → j ≺ k → i ≺ j → i ≺ k
≺≺ (≺sup x i≼fx) i≺j = ≺sup x (≺→≼ (≼≺ i≼fx i≺j))
≺iswf : wf.iswf _≺_
≺iswf i = wf.acc λ j j≺i → α i j (≺→≼ j≺i)
where
α : ∀ i j → j ≼ i → wf.Acc _≺_ j
α (sup _ f) j j≼i = wf.acc α'
where
α' : ∀ k → k ≺ j → wf.Acc _≺_ k
α' k k≺j with ≼≺ j≼i k≺j
... | ≺sup x k≼fx = α (f x) k k≼fx
plump : Sig → Set
plump Σ = 𝕎 (bin ⊕ Σ)
instance
SizePlump : {Σ : Sig} → Size (plump Σ)
_<_ {{thin{{SizePlump{Σ}}}}} = _≺_
<< {{thin{{SizePlump{Σ}}}}} = ≺≺
Oˢ {{SizePlump{Σ}}} = sup (ι₁ false) λ()
_⊔ˢ_ {{SizePlump{Σ}}} i j = sup (ι₁ true) λ{true → i ; false → j}
<⊔ˢl {{SizePlump{Σ}}} = ≺sup true (≼refl _)
<⊔ˢr {{SizePlump {Σ}}} = ≺sup false (≼refl _)
<iswf {{SizePlump {Σ}}} = ≺iswf
FilteredPlump : {Σ : Sig} → Filtered Σ (plump Σ)
⨆ˢ {{FilteredPlump}} a f = sup (ι₂ a) f
<⨆ˢ {{FilteredPlump}} f x = ≺sup x (≼refl (f x))