Naïm Camille Favier ncfavier

L ⊣ R

adjunct : (L a → b) → (a → R b)
coadjunct : (a → R b) → (L a → b)
unit : a → RL a
counit : LR b → b
Lmap : (a → b) → (L a → L b)
Rmap : (a → b) → (R a → R b)

instance Monoid a => MonadFix ((,) a) where
  mfix :: (b -> (a, b)) -> (a, b)
  mfix f = let (a, b) = f b in (a, b)
  -- or
  mfix f = fix (f . snd)

The laws are proved in section 4.5 of Value Recursion in Monadic Computations

	open import Cat.Functor.Naturality
	open import Cat.Functor.Bifunctor
	open import Cat.Functor.Coherence
	open import Cat.Instances.Product
	open import Cat.Functor.Compose
	open import Cat.Diagram.Monad
	open import Cat.Monoidal.Base
	open import Cat.Functor.Base
	open import Cat.Prelude

	canonical-elements⇒type-like : is-set Carrier → canonical-elements → type-like c
	canonical-elements⇒type-like set
	record { canon = canon
	; canon-≈ = canon-≈
	; canon-≡ = canon-≡ }
	=
	record { type-like-to = Σ _ λ a → canon a ≡ a
	; type-like-≅ = record { iso = record { _⟨$⟩_ = λ a → canon a , canon-≡ _ _ (canon-≈ a)
	; cong = λ s → Σ-≡ (canon-≡ _ _ s) set }
	; inv = record { _⟨$⟩_ = fst

	{-# LANGUAGE LambdaCase, BlockArguments, ViewPatterns #-}
	import Data.MemoTrie

	count :: [Int] -> Int
	count = memoFix \ go -> \case
	[0, 0, 0, 0, 0] -> 1
	[a, b, c, d, e] -> sum $ [go [b, c, d, e, a - n] \| n <- [1,3..a]]
	<> [go [e, d, c, b, a - n] \| n <- [2,4..a]]

	main = print $ 2 * count (replicate 5 14)

	function! s:unbackslash(str)
	return substitute(a:str, '\\\(.\)', '\1', 'g')
	endfunction

	" Parse a shell command line into a list of words, à la Perl's shellwords or
	" Python's shlex.split.
	function! s:shellwords(str)
	let l:args = []
	let l:len = len(a:str)
	let l:i = 0