PLFA agda exercises
module Mendler (F : Set → Set) where
open import Data.Product using (_×_)

Alg : Set → Set₁
Alg X = ∀ (R : Set) → (R → X) → F R → X

test : Set → Set
test A = A × A

test′ : ∀ (R : Set) → Set
test′ A = A × A