{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module Hask.Discrete where

import Hask.Core

data Discrete a = Discrete a

type instance Hom = (|~>|)

data (|~>|) (x :: Discrete a) (y :: Discrete b) where
  Refl :: x |~>| x

instance Category (|~>|) where
  id = Refl
  Refl . Refl = Refl