Zub.agda

record Preorder (A : Set) : Set1 where
  field rel : (x y : A) → Set
  field ident : ∀{x} → rel x x
  field compo : ∀{x y z} → rel x y → rel y z → rel x z

open Preorder public

-- "indiscrete if P has a least element, discrete otherwise"
data Zub {A} (P : Preorder A) : A → A → Set where
  refl : ∀{x} → Zub P x x
  -- If P has an initial element, become an indiscrete relation.
  huh : ∀{a} → (∀ b → rel P a b) → ∀{x y} → Zub P x y

zub : ∀{A} → Preorder A → Preorder A
zub P .rel = Zub P
zub P .ident = refl
zub P .compo refl x = x
zub P .compo (huh p) x = huh p