\begin{code}
{-# OPTIONS --cubical --safe --postfix-projections #-}

open import Algebra
open import Level

module Control.Monad.Weighted.Eliminators {β„“} {𝑅 : Type β„“} (rng : Semiring 𝑅) where

open Semiring rng

open import Level
open import Path
open import HLevels
open import Control.Monad.Weighted.Definition rng
open import Control.Monad.Weighted.Functor rng
open import Control.Monad.Weighted.Functor.TypeDef
open import Data.Sigma

private
  variable
    p q : Level
    P : Weighted A β†’ Type p
    Q : Weighted A β†’ Type q

module _ {A : Type a} {P : Weighted A β†’ Type p} where
\end{code}
%<*coherent>
\begin{code}
  record Coherent (ψ : Alg A P) : Type (p β„“βŠ” a β„“βŠ” β„“) where
    field  c-set : βˆ€ xs β†’ isSet (P xs)
           c-dup : βˆ€ p q x xs ψ⟨xs⟩ β†’    ψ (p  β—ƒ x ∷ (q β—ƒ x ∷ xs) ⟨ ψ (q β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩)
                                           ≑[ i ≔ P (dup p q x xs i)   ]≑
                                             ψ ((p + q) β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩)
           c-com : βˆ€ p x q y xs ψ⟨xs⟩ β†’  ψ (p  β—ƒ x ∷ (q β—ƒ y ∷ xs) ⟨ ψ (q β—ƒ y ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩)
                                           ≑[ i ≔ P (com p x q y xs i) ]≑
                                             ψ (q β—ƒ y ∷ (p β—ƒ x ∷ xs) ⟨ ψ (p β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩)
           c-del : βˆ€ x xs ψ⟨xs⟩ β†’        ψ (0# β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ≑[ i ≔ P (del x xs i) ]≑ ψ⟨xs⟩
\end{code}
%</coherent>
\begin{code}
open Coherent public
\end{code}
%<*elim-decl>
\begin{code}
Ξ¨ :  (A : Type a) (P : Weighted A β†’ Type p) β†’
     Type _
Ξ¨ A P = Ξ£ (Alg A P) Coherent
\end{code}
%</elim-decl>
\begin{code}
infixr 1 Ξ¨
syntax Ξ¨ A (Ξ» v β†’ e) = Ξ¨[ v ⦂ A ] e

\end{code}
%<*recursor-decl>
\begin{code}
Ξ¦ : Type a β†’ Type b β†’ Type (a β„“βŠ” b β„“βŠ” β„“)
Ξ¦ A B = Ξ¨ A (Ξ» _ β†’ B)
\end{code}
%</recursor-decl>
%<*runner-ty>
\begin{code}
⟦_⟧ : Ξ¨ A P β†’ (xs : Weighted A) β†’ P xs
\end{code}
%</runner-ty>
\begin{code}
⟦ alg ⟧ []                    = alg .fst []
⟦ alg ⟧ (p β—ƒ x ∷ xs)          = alg .fst (p β—ƒ x ∷ xs ⟨ ⟦ alg ⟧ xs ⟩)
⟦ alg ⟧ (dup p q x xs i)      = alg .snd .c-dup p q x xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (com p x q y xs i)    = alg .snd .c-com p x q y xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (del x xs i)          = alg .snd .c-del x xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (trunc xs ys p q i j) =
  isOfHLevel→isOfHLevelDep 2
    (alg .snd .c-set)
    (⟦ alg ⟧ xs) (⟦ alg ⟧ ys)
    (cong ⟦ alg ⟧ p) (cong ⟦ alg ⟧ q)
    (trunc xs ys p q)
    i j

prop-coh : {A : Type a} {P : Weighted A β†’ Type p} {alg : Alg A P} β†’ (βˆ€ xs β†’ isProp (P xs)) β†’ Coherent alg
prop-coh P-isProp .c-set xs = isProp→isSet (P-isProp xs)
prop-coh {P = P} {alg = alg} P-isProp .c-dup p q x xs ψ⟨xs⟩ =
 toPathP (P-isProp (p + q β—ƒ x ∷ xs) (transp (Ξ» i β†’ P (dup p q x xs i)) i0 (alg (p β—ƒ x ∷ (q β—ƒ x ∷ xs) ⟨ alg (q β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩))) (alg ((p + q) β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩)))
prop-coh {P = P} {alg = alg} P-isProp .c-com p x q y xs ψ⟨xs⟩ =
  toPathP (P-isProp (q β—ƒ y ∷ p β—ƒ x ∷ xs) (transp (Ξ» i β†’ P (com p x q y xs i)) i0 (alg (p β—ƒ x ∷ (q β—ƒ y ∷ xs) ⟨ alg (q β—ƒ y ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩))) (alg (q β—ƒ y ∷ (p β—ƒ x ∷ xs) ⟨ alg (p β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩)))
prop-coh {P = P} {alg = alg} P-isProp .c-del x xs ψ⟨xs⟩ =
  toPathP (P-isProp xs (transp (Ξ» i β†’ P (del x xs i)) i0 (alg (0# β—ƒ x ∷ xs ⟨ ψ⟨xs⟩ ⟩))) ψ⟨xs⟩)

infix 4 _⊜_
record AnEquality (A : Type a) : Type (a β„“βŠ” β„“) where
  constructor _⊜_
  field lhs rhs : Weighted A
open AnEquality public

EqualityProof-Alg : {B : Type b} (A : Type a) (P : Weighted A β†’ AnEquality B) β†’ Type (a β„“βŠ” b β„“βŠ” β„“)
EqualityProof-Alg A P = Alg A (Ξ» xs β†’ let Pxs = P xs in lhs Pxs ≑ rhs Pxs)

eq-coh : {A : Type a} {B : Type b} {P : Weighted A β†’ AnEquality B} {alg : EqualityProof-Alg A P} β†’ Coherent alg
eq-coh {P = P} = prop-coh Ξ» xs β†’ let Pxs = P xs in trunc (lhs Pxs) (rhs Pxs)
\end{code}