-- A universe for equality types
module Eq where

import Data.String as String
open String using (String)
open import Data.Nat
open import Data.Bool

data EqType : Set where
  nat    : EqType
  bool   : EqType
  string : EqType

El : EqType → Set
El nat    = ℕ
El bool   = Bool
El string = String

_==_ : ∀ {u} → El u → El u → Bool
_==_ {nat} zero zero = true
_==_ {nat} zero (suc n) = false
_==_ {nat} (suc n) zero = false
_==_ {nat} (suc n) (suc m) = n == m
_==_ {bool} true y = y
_==_ {bool} false y = not y
_==_ {string} x y = String._==_ x y