sMartin Escardo 2012

\begin{code}

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

module EffectfulForcing.MFPSAndVariations.Combinators where

open import MLTT.Spartan hiding (rec)

ΔΆ : {X Y : 𝓀 Μ‡ } β†’ X β†’ Y β†’ X
ΔΆ x y = x

Ş : {X Y Z : 𝓀 Μ‡ } β†’ (X β†’ Y β†’ Z) β†’ (X β†’ Y) β†’ X β†’ Z
Ş f g x = f x (g x)

iter : {X : 𝓀 Μ‡ } β†’ (X β†’ X) β†’ X β†’ β„• β†’ X
iter f x  0       = x
iter f x (succ n) = f (iter f x n)

rec : {X : 𝓀 Μ‡ } β†’ (β„• β†’ X β†’ X) β†’ X β†’ β„• β†’ X
rec f x  0       = x
rec f x (succ n) = f n (rec f x n)

\end{code}