{-# OPTIONS --sized-types #-}

module ZilibowitzRubenHenner4 where

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Size

data ℕ : {_ : Size} -> Set where
 zero : ∀ {size} → ℕ {↑ size} 
 suc  : ∀ {size} → ℕ {size} → ℕ {↑ size}

{-
data _≤_ : Rel (ℕ {∞}) where
 z≤n : ∀ {sm sn}              {n : ℕ {sn}}               → zero {sm} ≤ n
 s≤s : ∀ {sm sn} {m : ℕ {sm}} {n : ℕ {sn}} (m≤n : m ≤ n) → suc {sm} m ≤ suc {sn} n
-}

data _≤_ : Rel (ℕ {∞}) where
 z≤n : ∀              {n : ℕ {∞}}               → zero {∞} ≤ n
 s≤s : ∀  {m : ℕ {∞}} {n : ℕ {∞}} (m≤n : m ≤ n) → suc {∞} m ≤ suc {∞} n

antisym : Antisymmetric _≡_ _≤_
antisym z≤n       z≤n       = refl
antisym (s≤s m≤n) (s≤s n≤m) with antisym m≤n n≤m
...                         | refl = refl