Naïm Camille Favier ncfavier

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

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)

	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

	{-# LANGUAGE BlockArguments #-}

	import Control.Monad
	import Data.Foldable
	import Data.Map (Map)
	import Data.Map qualified as Map
	import Data.Set (Set)
	import Data.Set qualified as Set
	import Data.Sequence qualified as Seq
	import Data.PriorityQueue.FingerTree qualified as PQ

	import Data.Bits
	import Data.Foldable

	{-
	Two implementations of A372325 (https://oeis.org/A372325).

	The first one ties the knot on the sequence itself, but needs the first
	three values in order to get bootstrapped.
	Using a cleverer takeWhile we could produce the first 0, but in order to
	produce 2 we need to know that 1 isn't in the sequence, which we only

	module Lan where

	open import Categories.Kan
	open import Data.Product
	open import Level
	open import Function renaming (id to funId)
	open import Categories.Functor
	open import Categories.Category.Instance.Sets
	open Functor
	open import Relation.Binary.PropositionalEquality

	{-# OPTIONS --cubical #-}
	open import Cubical.Data.Int
	open import Cubical.Data.Int.Divisibility
	open import Cubical.Data.Nat
	open import Cubical.Foundations.Everything
	open import Data.List
	open import Data.List.NonEmpty as List⁺

	data Vertex : Type where
	a b c : Vertex