Martin Escardo 20-21 December 2012

\begin{code}

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

module InfSearchable where

open import Two
open import CurryHoward
open import Equality

putative-root : {X : Set}  (X  )  X  Prp
putative-root p x₀ = ( \x  p x  )  p x₀  

root-lower-bound : {X : Set}  bin-rel X  (X  )  X  Prp
root-lower-bound R p l =  x  p x    R l x

upper-bound-of-root-lower-bounds : {X : Set}  bin-rel X  (X  )  X  Prp
upper-bound-of-root-lower-bounds R p u =  l  root-lower-bound R p l  R l u

inf-searchable : (X : Set)  bin-rel X  Prp
inf-searchable X R = ∀(p : X  ) 
                           \(x₀ : X)  putative-root p x₀ 
                                        root-lower-bound R p x₀ 
                                        upper-bound-of-root-lower-bounds R p x₀

\end{code}