module Signature.Nat where

open import Stdlib
open import Signature

module Model where

  data Nat : Set where
    ze : Nat
    suc : (n : Nat)  Nat

ΣNat : Sig 
ΣNat = OpNat  ArNat / TyNat
  where OpNat :   Set
        OpNat tt =   

        ArNat : {tt : }  OpNat tt  Set
        ArNat (inj₁ tt) = 
        ArNat (inj₂ tt) = 

        TyNat : {tt : }{op : OpNat tt}  ArNat op  
        TyNat _ = tt

Nat : Set
Nat = μ ΣNat tt

ze : Nat
ze =  inj₁ tt ,  bot  ⊥-elim bot) 

su : Nat  Nat
su n =  inj₂ tt ,  { tt  n })