Martin Escardo and Paulo Oliva 2011

\begin{code}

{-# OPTIONS --without-K --no-termination-check #-}

\end{code}

We use Berger's modified bar recursion functional to realize the
K-Shift.

\begin{code}

module InfinitePigeon.K-Shift-MBR where

open import InfinitePigeon.Finite
open import InfinitePigeon.JK-Monads
open import InfinitePigeon.Logic
open import InfinitePigeon.Naturals

K-∀-shift-mbr : {R : Ω}
                {A : ℕ → Ω}
              → (∀(n : ℕ) → R → A n)                     -- efqs,
              → (∀(n : ℕ) → K(A n)) → K(∀(n : ℕ) → A n)  -- shift.

K-∀-shift-mbr {R} {A} efqs φs p =
 mbr {} (λ i → ⊥-elim (smaller-gives-is-nonzero i))
  where
   mbr : {m : ℕ} → (∀(i : smaller m) → A(embed i)) → R
   mbr {m} s = p(override s (λ n → efqs n (φs m (λ x → mbr(append {A} s x)))))

\end{code}