Natural number as Preorder ?

[lengyijun]

naturalnumber : Preorder
Carrier naturalnumber = ℕ
_≤_ naturalnumber = {! _≤ᵇ_!}
reflexive naturalnumber = {!!}
transitive naturalnumber = {!!}
propositional naturalnumber = {!!}

Error: Agda.Builtin.Bool.Bool !=< Set

[fredrikNordvallForsberg]

Looks like you've tried to use _≤ᵇ_ as the order relation, but this is a function returning a Boolean -- we want the relation to return evidence that one number is smaller than another. You could use _<_ from Data.Nat.Base instead.