{-# OPTIONS --no-termination-check #-}

open import Prelude
open import Algebra

module Hyper.MonadComonadic {โ„“}  {๐‘€ : Type โ„“ โ†’ Type โ„“} {๐บ : Type โ„“ โ†’ Type โ„“}
  (mon   : Monad ๐‘€)
  (comon : Comonad ๐บ) where


infixr 1 _โ†ฌ_ _โ†ฌโ€ฒ_
_โ†ฌโ€ฒ_ : Type โ„“ โ†’ Type โ„“ โ†’ Type โ„“
record _โ†ฌ_ (A : Type โ„“) (B : Type โ„“) : Type โ„“

{-# NO_POSITIVITY_CHECK #-}
record _โ†ฌ_ A B where
  inductive; constructor hyp
  infixl 4 _ยท_
  field _ยท_ : ๐บ (B โ†ฌโ€ฒ A) โ†’ B
A โ†ฌโ€ฒ B = ๐‘€ (B โ†ฌ A) โ†’ B

open _โ†ฌ_

open Monad mon
open Comonad comon

pure : A โ†’ ๐‘€ A
pure = return

_<*>_ : ๐‘€ (A โ†’ B) โ†’ ๐‘€ A โ†’ ๐‘€ B
fs <*> xs = do
  f โ† fs
  x โ† xs
  pure (f x)

infixr 9 _โŠ™_ _โŠ™โ€ฒ_ _โŠ™โ€ณ_
mutual
  _โŠ™โ€ณ_ : (B โ†ฌโ€ฒ C) โ†’ ๐‘€ (A โ†ฌ B) โ†’ (A โ†ฌโ€ฒ C)
  (f โŠ™โ€ณ g) k = f โฆ‡ g โŠ™ k โฆˆ

  _โŠ™โ€ฒ_ : B โ†ฌ C โ†’ ๐บ (A โ†ฌโ€ฒ B) โ†’ (A โ†ฌโ€ฒ C)
  (f โŠ™โ€ฒ g) k = f ยท cmap (_โŠ™โ€ณ k) g

  _โŠ™_ : B โ†ฌ C โ†’ A โ†ฌ B โ†’ A โ†ฌ C
  f โŠ™ g ยท k = f ยท extend (g โŠ™โ€ฒ_) k

k : B โ†’ A โ†ฌ B
k x ยท _ = x

๐•€ : A โ†ฌ A
๐•€ ยท x = extract x โฆ‡ ๐•€ โฆˆ

infixr 5 _โ—ƒ_
_โ—ƒ_ : (A โ†’ B) โ†’ A โ†ฌ B โ†’ A โ†ฌ B
f โ—ƒ xs ยท k = f (extract k โฆ‡ xs โฆˆ)

โ–ณ : (A โ†’ B) โ†’ A โ†ฌ B
โ–ณ f = f โ—ƒ โ–ณ f

โ–ฝ : A โ†ฌ B โ†’ ๐บ A โ†’ B
โ–ฝ h x = h ยท cmap const x

cata : {C : Type โ„“} โ†’ ((๐บ (๐‘€ C โ†’ A) โ†’ B) โ†’ C) โ†’ A โ†ฌ B โ†’ C
cata ฯ• h = ฯ• ฮป k โ†’ h ยท cmap (_โˆ˜ mmap (cata ฯ•)) k

ana : {C : Type โ„“} โ†’ (C โ†’ ๐บ (๐‘€ C โ†’ A) โ†’ B) โ†’ C โ†’ A โ†ฌ B
ana ฯˆ r ยท k = ฯˆ r (cmap (_โˆ˜ mmap (ana ฯˆ)) k)

๐•„ : A โ†ฌ A โ†ฌ B โ†’ A โ†ฌ B
๐•„ = cata ฮป where g ยท k โ†’ g k ยท k

๐•‚ : A โ†ฌ B โ†ฌ A
๐•‚ ยท x ยท y = extract x โฆ‡ ๐•‚ โฆˆ