{-# OPTIONS --universe-polymorphism #-}
module Data.Star.NP where

open import Relation.Binary using (Rel;_⇒_)
open import Data.Star public
open import Function
-- import Category as Cat

Star⁻¹ : ∀ {ℓ a} {A : Set a} → Rel A ℓ → Rel A _
Star⁻¹ = flip ∘ Star ∘ flip

evalStar : ∀ {a p q} {A : Set a}
             {P : Rel A p} {Q : Rel A q} (idQ : ∀ {x} → Q x x)
             (_∘Q_ : ∀ {x y z} → Q y z → Q x y → Q x z)
           → (P ⇒ Q) → Star P ⇒ Q
evalStar idQ _    _ ε        = idQ
evalStar idQ _∘Q_ f (x ◅ xs) = evalStar idQ _∘Q_ f xs ∘Q f x 

{-
evalStar' : ∀ {A : Set}
              {P Q : Rel A} (catQ : Cat.RawCategory Q)
            → (P ⇒ Q) → Star P ⇒ Q
evalStar' {P = P} {Q} catQ f = go
  where open Cat.RawCategory catQ
        go : Star P ⇒ Q
        go ε        = id catQ
        go (x ◅ xs) = f x ∘ go xs
-}