\begin{code}
{-# OPTIONS --cubical --safe #-}
open import Algebra
open import Level

module Control.Monad.Weighted.Functor {ā„“} {š‘… : Type ā„“} (rng : Semiring š‘…) where

open Semiring rng

open import Level
open import Control.Monad.Weighted.Definition rng
open import Function
open import Path
open import Prelude

open import Control.Monad.Weighted.Functor.TypeDef

private
  variable
    p q : Level
    P : Weighted A ā†’ Type p
    Q : Weighted A ā†’ Type q
private
  module DisplayFunctors where
    module SimpleFunctor where
\end{code}
%<*simple-functor-def>
\begin{code}
      data š”š (A : Type a) (B : Type b) :
                    Type (a ā„“āŠ” b ā„“āŠ” ā„“) where
        []     : š”š A B
        _ā—ƒ_āˆ·_  :  š‘… ā†’ A ā†’
                  B ā†’ š”š A B
\end{code}
%</simple-functor-def>
%<*functor-def>
\begin{code}
    data š”š (A : Type a) (P : Weighted A ā†’ Type p) :
                    Type (a ā„“āŠ” p ā„“āŠ” ā„“) where
      []        : š”š A P
      _ā—ƒ_āˆ·_āŸØ_āŸ©  :  š‘… ā†’ A ā†’
                  (xs : Weighted A) ā†’ P xs ā†’ š”š A P
\end{code}
%</functor-def>
\begin{code}
š”š : (A : Type a) ā†’ (Weighted A ā†’ Type p) ā†’ Type (a ā„“āŠ” p ā„“āŠ” ā„“)
š”š A = š”š-F š‘… (Weighted A) A
\end{code}
%<*map>
\begin{code}
map : (P ā‡’ Q) ā†’ š”š A P ā†’ š”š A Q
map f []                      = []
map f (w ā—ƒ x āˆ· xs āŸØ ĻˆāŸØxsāŸ© āŸ©)  =
  w ā—ƒ x āˆ· xs āŸØ f ĻˆāŸØxsāŸ© āŸ©
\end{code}
%</map>
%<*wrap>
\begin{code}
āŸŖ_āŸ« : š”š A P ā†’ Weighted A
āŸŖ [] āŸ«                = []
āŸŖ w ā—ƒ x āˆ· xs āŸØ _ āŸ© āŸ«  = w ā—ƒ x āˆ· xs
\end{code}
%</wrap>
%<*wrap-map>
\begin{code}
map-id :  (f : P ā‡’ Q) (xs : š”š A P) ā†’
          āŸŖ xs āŸ« ā‰” āŸŖ map f xs āŸ«
map-id f []                 = refl
map-id f (_ ā—ƒ _ āˆ· _ āŸØ _ āŸ©)  = refl
\end{code}
%</wrap-map>
%<*alg>
\begin{code}
Alg :  (A : Type a) (P : Weighted A ā†’ Type p) ā†’
       Type _
Alg A P = (xs : š”š A P) ā†’ P āŸŖ xs āŸ«
\end{code}
%</alg>