Functor constrained by a regular expression

Functor.agda

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module Data.Functor
       (Alphabet : Set)
       (_≤_  : (a b : Alphabet) → Set)
       (_≟_  : (a b : Alphabet) → Dec (a ≡ b))
       (_≤?_ : (a b : Alphabet) → Dec (a ≤ b))
       where

open import RegExp.Search Alphabet _≤_ _≟_ _≤?_

open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.List
open import Function
open import lib.Nullary
open import Relation.Binary.PropositionalEquality

infixr 3 _`+_ _`*_
data Desc : Set₁ where
  `K   : (A : Set) → Desc       -- constant
  `X   : Desc                   -- recursive
  `L   : Desc                   -- leaf
  _`+_ : (d₁ d₂ : Desc) → Desc  -- disjunction
  _`*_ : (d₁ d₂ : Desc) → Desc  -- conjunction

⟦_⟧ : (d : Desc) (X : (e f : RegExp) → Set) (e f : RegExp) → Set
⟦ `K A     ⟧ X e f = A × e ≡ f
⟦ `X       ⟧ X e f = X e f
⟦ `L       ⟧ X e f = Σ[ a ∈ Alphabet ] (e ⟪ a) ≡ f
⟦ d₁ `+ d₂ ⟧ X e f = ⟦ d₁ ⟧ X e f ⊎ ⟦ d₂ ⟧ X e f
⟦ d₁ `* d₂ ⟧ X e f = Σ[ ef ∈ RegExp ] ⟦ d₁ ⟧ X e ef × ⟦ d₂ ⟧ X ef f

data `μ (d : Desc) (e f : RegExp) : Set where
  ⟨_⟩ : ⟦ d ⟧ (`μ d) e f → `μ d e f

μ : (d : Desc) (e : RegExp) → Set
μ d e = Σ[ f ∈ RegExp ] ([] ∈ f) × `μ d e f