A predicative version of Tarski's fixed-point theorem.

Tarski.agda

-- A predicative version of Tarski's fixed-point theorem

open import Level
open import Data.Product

module Tarski where

  -- a complete preorder with carrier at level a, the preorder is at level b,
  -- and suprema indexed by sets from level c
  record CompletePreorder a b c : Setω where
    infix 10 _≤_

    -- preorder structure
    field
      carrier : Set a
      _≤_ : carrier → carrier → Set b
      ≤-refl : ∀ x → x ≤ x
      ≤-tran : ∀ {x} y {z} → x ≤ y → y ≤ z → x ≤ z

    upper-bound : ∀ {I : Set c} (f : I → carrier) (x : carrier) → Set (b ⊔ c)
    upper-bound f x = ∀ i → f i ≤ x

    -- suprema
    field
      sup : ∀ {I : Set c} → (I → carrier) → carrier
      sup-is-upper : ∀ {I : Set c} {f : I → carrier} (i : I) → f i ≤ sup f
      sup-is-least : ∀ {I : Set c} {f : I → carrier} {x : carrier} → upper-bound f x → sup f ≤ x

    -- equivalence induced by the preorder
    infix 10 _≈_
    _≈_ : carrier → carrier → Set b
    x ≈ y = x ≤ y × y ≤ x

    is-monotone-endomap : (carrier → carrier) → Set (a ⊔ b)
    is-monotone-endomap h = ∀ {x y} → x ≤ y → h x ≤ h y


  module _ {a b} (P : CompletePreorder a b (a ⊔ b)) where

    open CompletePreorder P

    open Σ

    tarski : ∀ (h : carrier → carrier) → is-monotone-endomap h → Σ[ y ∈ carrier ] h y ≈ y
    tarski h monotone-h = y , (hy≤y , y≤hy)
      where
        postfix = Σ[ z ∈ carrier ] z ≤ h z

        p : postfix → carrier
        p (z , _) = z

        y = sup p

        y≤hy : y ≤ h y
        y≤hy = sup-is-least λ { (z , z≤hz) → ≤-tran (h z) z≤hz (monotone-h (sup-is-upper ((z , z≤hz)))) }

        hy≤y : h y ≤ y
        hy≤y = sup-is-upper ((h y) , (monotone-h y≤hy))