reflexitive relation on natural numbers on Agda2

gistfile1.hs

module FooBarNat where

-- cheat on the exam; look the Standard library

Relation : Set -> Set -> Set1
Relation A B = A -> B -> Set

Reflexivity : (A : Set) -> Relation A A -> Set
Reflexivity A P = (i : A) -> P i i

record ReflexiveRelation (A : Set) (_≈_ : Relation A A) : Set where
  field
    refl : Reflexivity A _≈_

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

data _≤_ : Relation Nat Nat where
  zeroIsMinimal : ∀ {n} -> zero ≤ n
  liftSuccessor : ∀ {m n} (p : m ≤ n) -> succ m ≤ succ n

≤-refl : (x : Nat) -> x ≤ x
≤-refl zero     = zeroIsMinimal
≤-refl (succ n) = liftSuccessor (≤-refl n)

≤isReflexive : ReflexiveRelation Nat (_≤_)
≤isReflexive = record { refl = ≤-refl }