oxij

-- Make Agda as unsafe as Haskell is
{-# OPTIONS
  --type-in-type
  --no-termination-check #-}

-- `type-in-type` for impredicative Π-types (Set → Set : Set)
-- `no-termination-check` for blowing up

module Church where

oxij

-- The trick for proving that nested-recursion == recursion with accumulator for all arguments (in Agda).
-- Example for Nat. Should be generalizable.

module NumTest where

import Level

data _≡_ {α} {A : Set α} (a : A) : A → Set α where
  refl : a ≡ a