------------------------------------------------------------------------ -- Instantiation of Contractive for functions ------------------------------------------------------------------------ -- Taken from the paper. open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Contractive open import Level module Contractive.Function {A B : Set} {_<_ : Rel A zero} (isWFO : IsWellFoundedOrder _<_) (dec : Decidable _<_) (proof-irrelevance : ∀ {a a'} (p₁ p₂ : a < a') → p₁ ≡ p₂) where open import Relation.Nullary open import Relation.Unary open import Data.Empty ofe : OFE ofe = record { Carrier = A ; Domain = A → B ; _<_ = _<_ ; isWellFoundedOrder = isWFO ; Eq = λ a f g → f a ≡ g a ; isEquivalence = λ _ → record { refl = refl ; sym = sym ; trans = trans } } open OFE ofe hiding (_<_) private limU : (A → (A → B)) → A → B limU f a' = f a' a' lim↓ : B → ∀ a → (∀ x → x < a → A → B) → A → B lim↓ b a f a' with dec a' a lim↓ b a f a' | yes a'