fake agda for preorder theory

not-actually-agda.agda

record Preorder (A : Set) : Set1 where
  _≤_   : A → A → Set
  refl  : {a} → a ≤ a
  trans : {a b c} → a ≤ b → b ≤ c → a ≤ c

record is-lub {A} (P : Preorder A) {I} (a : I → A) (⋁a : A) : Set where
  bound : (i : I) → a i ≤ ⋁a
  least : (b : A) → ((i : I) → a i ≤ b) → ⋁a ≤ b

module _ {A B} (P : Preorder A) (Q : Preorder B) (f : A → B) where
  mono : Set
  mono = {x y} → x P.≤ y → f x Q.≤ f y

  ωcont : Set
  ωcont = (x : ℕ → A) → (i ≤ j → x i P.≤ x j) →   -- Gimme an ω-chain xᵢ
          (⋁x : A) → is-lub P x ⋁x →              -- and its limit ⋁ᵢ xᵢ
          is-lub Q (f ∘ x) (f ⋁x)                 -- then f(⋁ᵢ xᵢ) = ⋁ᵢ xᵢ