{-# OPTIONS --without-K #-}

open import Basis

module Algebra (T : Set → Set) ⦃ T-monad : Monad T ⦄ where

record Alg : Set₁ where
  constructor algebra
  field
    car : Set
    alg : T car → car
    law/η : ∀ x → alg (ret x) ≡ x
    law/μ : ∀ (m : T (T car)) → alg (map alg m) ≡ alg (join m)

F : Set → Alg
Alg.car (F A) = T A
Alg.alg (F A) = join
Alg.law/η (F A) _ = law/λ
Alg.law/μ (F A) m =
  ≡.seq
   (law/α m)
   (≡.seq
    (≡.cong (m >>=_) (funext λ _ → law/λ))
    (≡.inv (law/α m)))

U : Alg → Set
U = Alg.car

Alg/Π : (A : Set) → (A → Alg) → Alg

Alg.car (Alg/Π A B) =
  (x : A) → Alg.car (B x)

Alg.alg (Alg/Π A B) m x =
  Alg.alg (B x) (map (λ f → f x) m)

Alg.law/η (Alg/Π A B) f =
  depfunext λ x →
  ≡.seq
   (≡.cong (Alg.alg (B x)) law/λ)
   (Alg.law/η (B x) (f x))

Alg.law/μ (Alg/Π A B) m =
  depfunext λ x →
  ≡.seq
   (≡.cong
    (Alg.alg (B x))
    (≡.seq
     (law/α m)
     (≡.seq
      (≡.cong
       (m >>=_)
       (funext λ _ →
        ≡.seq law/λ (≡.inv law/λ)))
      (≡.inv
       (law/α m)))))
   (≡.seq
    (Alg.law/μ (B x) (map (map (λ f → f x)) m))
    (≡.cong
     (Alg.alg (B x))
     (≡.seq
      (law/α m)
      (≡.seq
       (≡.cong
        (m >>=_)
        (funext λ _ → law/λ))
       (≡.inv
        (law/α m))))))


Alg[_⇒_] : Set → Alg → Alg
Alg[ A ⇒ B ] = Alg/Π A λ _ → B