Mender-style in Agda (without positifity/termination checks)

Mendler.agda

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

module Mendler where

open import Data.Bool
-- open import Data.Product
-- open import Data.String

data μ (F : Set → Set) : Set where
  In : F (μ F) → μ F

mit : ∀{F}{a : Set} → (∀{r} → (r → a) → F r → a) → μ F → a
mit φ (In x) = φ (mit φ) x

data μ' (F : Set → Set) (a : Set) : Set where
  In' : F (μ' F a) → μ' F a
  Inv : a → μ' F a

msfit' : ∀{F}{a} →
         (∀{r} → (a → r a) → (r a → a) → F (r a) → a) → μ' F a → a
msfit' φ (In' x) = φ Inv (msfit' φ) x
msfit' φ (Inv v) = v

msfit : ∀{F}{a} →
        (∀{r} → (a → r a) → (r a → a) → F (r a) → a) → (∀{a} → μ' F a) → a 
msfit φ r = msfit' φ r

data N r : Set where
  Z : N r
  S : r → N r

Nat = μ N

zero : Nat
zero = In Z
succ : Nat → Nat
succ n = In (S n)

one = succ zero
two = succ one
three = succ two

plusφ : ∀{r} → (r → Nat → Nat) → N r → Nat → Nat
plusφ plus Z     m = m
plusφ plus (S n) m = succ (plus n m)

plus = mit plusφ

nnn = plus two three

data L a r : Set where
  Nil  : L a r
  Cons : a → r → L a r

List = λ a → μ (L a)
nil : ∀{a} → List a
nil = In Nil
cons : ∀{a} → a → List a → List a 
cons x xs = In (Cons x xs)

l1 = cons true nil
l2 = cons false l2

data E r : Set where
  App : r → E r
  Lam : (r → r) → E r