{-# LANGUAGE TypeOperators , TypeFamilies , GADTs , RankNTypes , PatternSynonyms , FlexibleContexts , FlexibleInstances , NoImplicitPrelude , UndecidableInstances , ScopedTypeVariables , ConstraintKinds , MultiParamTypeClasses #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Category.Enriched.Poset3 -- License : BSD-style (see the file LICENSE) -- -- Maintainer : sjoerd@w3future.com -- Stability : experimental -- Portability : non-portable ----------------------------------------------------------------------------- module Data.Category.Enriched.Poset3 where import Data.Category.Boolean import Data.Category.Enriched data One data Two data Three data PosetTest a b where One :: PosetTest One One Two :: PosetTest Two Two Three :: PosetTest Three Three type family Poset3 a b where Poset3 Two One = Fls Poset3 Three One = Fls Poset3 Three Two = Fls Poset3 a b = Tru instance ECategory PosetTest where type V PosetTest = Boolean type PosetTest $ (a, b) = Poset3 a b hom One One = Tru hom One Two = Tru hom One Three = Tru hom Two One = Fls hom Two Two = Tru hom Two Three = Tru hom Three One = Fls hom Three Two = Fls hom Three Three = Tru id One = Tru id Two = Tru id Three = Tru comp One One One = Tru comp One One Two = Tru comp One One Three = Tru comp One Two One = F2T comp One Two Two = Tru comp One Two Three = Tru comp One Three One = F2T comp One Three Two = F2T comp One Three Three = Tru comp Two One One = Fls comp Two One Two = F2T comp Two One Three = F2T comp Two Two One = Fls comp Two Two Two = Tru comp Two Two Three = Tru comp Two Three One = Fls comp Two Three Two = F2T comp Two Three Three = Tru comp Three One One = Fls comp Three One Two = Fls comp Three One Three = F2T comp Three Two One = Fls comp Three Two Two = Fls comp Three Two Three = F2T comp Three Three One = Fls comp Three Three Two = Fls comp Three Three Three = Tru