Markov.agda

{-# OPTIONS --cubical-compatible #-}

open import Data.Nat.Base
open import Data.Product
open import Relation.Nullary
open import Relation.Unary

module Markov {p} (P : ℕ → Set p) (dec : Decidable P) .(h : Σ ℕ P) where

{-# TERMINATING #-}
markov′ : ∀ n → (∀ m → m <′ n → ¬ P m) → Σ ℕ P
markov′ n pf with dec n
...          | yes p = n , p
...          | no  p = markov′ (suc n) λ where
                         n ≤′-refl → p
                         m (≤′-step lt) → pf m lt

markov : Σ ℕ P
markov = markov′ zero λ _ ()