blob: 52d46443ccf973b2eaf5da2daf85ec9bae7e6068 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary
module Cfe.Language.Properties
{c ℓ} {setoid : Setoid c ℓ}
where
open Setoid setoid renaming (Carrier to A)
open import Cfe.Language setoid
open Language
open import Data.List
open import Data.List.Relation.Binary.Equality.Setoid setoid
open import Function
open import Level
open import Relation.Binary.Construct.InducedPoset
_≤′_ : ∀ {a aℓ} → Rel (Language a aℓ) (c ⊔ a)
_≤′_ = _≤_
------------------------------------------------------------------------
-- Properties of _≤_
≤-refl : ∀ {a aℓ} → Reflexive (_≤′_ {a} {aℓ})
≤-refl = id
≤-trans : ∀ {a b c aℓ bℓ cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
≤-trans A≤B B≤C = B≤C ∘ A≤B
≤-poset : ∀ {a aℓ} → Poset (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) (c ⊔ a) (c ⊔ a)
≤-poset {a} {aℓ} = InducedPoset (_≤′_ {a} {aℓ}) id (λ i≤j j≤k → j≤k ∘ i≤j)
-- ------------------------------------------------------------------------
-- -- Properties of _∪_
-- ∪-cong-≤ : Congruent₂ _≤_ _∪_
-- ∪-cong-≤ A≤B C≤D = map A≤B C≤D
-- ∪-cong : Congruent₂ _≈_ _∪_
-- ∪-cong {A} {B} {C} {D} = ≤-cong₂→≈-cong₂ {_∪_} (λ A≤B C≤D → map A≤B C≤D) {A} {B} {C} {D}
|
