Agda proof of the Knaster-Tarski Fixpoint Theorem

Fixpoint.agda

-- A proof of the Knaster-Tarski Fixpoint Theorem
-- See https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem
module Fixpoint where

open import Level
open import Data.Product

open import Relation.Binary
open import Relation.Binary.Morphism

record IsCompleteLattice {a i ℓ₁ ℓ₂} {A : Set a}
                         (_≈_ : Rel A ℓ₁) -- The underlying equality
                         (_≤_ : Rel A ℓ₂) -- The partial order.
                         (⋀ : {I : Set i} → (I → A) → A)
                         (⋁ : {I : Set i} → (I → A) → A)
                         : Set (a ⊔ suc i ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    sup : ∀ {I : Set i} {P : I → A} → (xi : I) → ⋀ P ≤ P xi
    inf : ∀ {I : Set i} {P : I → A} → (xi : I) → P xi ≤ ⋁ P
    supremum : ∀ {I : Set i} {P : I → A} → (x : A) → (∀ {xi} → x ≤ P xi) → x ≤ ⋀ P
    infinum : ∀ {I : Set i} {P : I → A} → (x : A) → (∀ {xi} → P xi ≤ x) → ⋁ P ≤ x

record CompleteLattice c i ℓ₁ ℓ₂ : Set (suc (c ⊔ i ⊔ ℓ₁ ⊔ ℓ₂)) where
  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ₁
    _≤_ : Rel Carrier ℓ₂
    ⋀ : {I : Set i} → (I → Carrier) → Carrier
    ⋁ : {I : Set i} → (I → Carrier) → Carrier
    isPartialOrder : IsPartialOrder _≈_ _≤_
    isCompleteLattice : IsCompleteLattice _≈_ _≤_ ⋀ ⋁

  open IsPartialOrder isPartialOrder public
  open IsCompleteLattice isCompleteLattice public

record Fixpoint {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (F : A → A) : Set (a ⊔ ℓ) where
  field
    point : A
    isFixpoint : F point ≈ point

module _ {c ℓ₁ ℓ₂} (L : CompleteLattice c (c ⊔ ℓ₂) ℓ₁ ℓ₂) where
  open CompleteLattice L

  tarski-fixpoint : ∀ {F : Carrier → Carrier} → IsOrderMonomorphism _≈_ _≈_ _≤_ _≤_ F → Fixpoint _≈_ F
  tarski-fixpoint {F = F} monotone = record
    { point = point
    ; isFixpoint =
      let fix-≤ = supremum (F point) λ {(x , Fx≤x)} → trans (monotone.mono (sup (x , Fx≤x))) Fx≤x
          fix-≥ = sup ((F point) , monotone.mono fix-≤)
      in antisym fix-≤ fix-≥
    }
    where
      module monotone = IsOrderMonomorphism monotone

      point : Carrier
      point = ⋀ {Σ[ x ∈ Carrier ] (F x ≤ x)} proj₁

  least-fixpoint : ∀ {F : Carrier → Carrier} → (monotone : IsOrderMonomorphism _≈_ _≈_ _≤_ _≤_ F) → (x : Fixpoint _≈_ F) → Fixpoint.point (tarski-fixpoint monotone) ≤ Fixpoint.point x
  least-fixpoint {F = F} monotone x = sup ((Fixpoint.point x) , reflexive (Fixpoint.isFixpoint x))
    where
      module monotone = IsOrderMonomorphism monotone