module Proarrow.Preorder.Discrete where

import Prelude (type (~))

import Proarrow.Preorder (CProfunctor (..), CPromonad (..), Dict (..), POS, PreorderOf (..), type (:-) (..))

newtype DISCRETE k = D k
instance CProfunctor ((~) :: POS (DISCRETE k)) where
  cdimap :: forall (c :: DISCRETE k) (a :: DISCRETE k) (b :: DISCRETE k)
       (d :: DISCRETE k).
(c <= a, b <= d, a ~ b) :- (c ~ d)
cdimap = ((c ~ a, b ~ d, a ~ b) => Dict (c ~ d))
-> (c ~ a, b ~ d, a ~ b) :- (c ~ d)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (c ~ d)
(c ~ a, b ~ d, a ~ b) => Dict (c ~ d)
forall (a :: Constraint). a => Dict a
Dict
  obs :: forall (a :: DISCRETE k) (b :: DISCRETE k).
(a ~ b) :- (COb a, COb b)
obs = ((a ~ b) => Dict (() :: Constraint, () :: Constraint))
-> (a ~ b) :- (() :: Constraint, () :: Constraint)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (() :: Constraint, () :: Constraint)
(a ~ b) => Dict (() :: Constraint, () :: Constraint)
forall (a :: Constraint). a => Dict a
Dict
instance CPromonad ((~) :: POS (DISCRETE k)) where
  cid :: forall (a :: DISCRETE k). COb a => (() :: Constraint) :- (a ~ a)
cid = ((() :: Constraint) => Dict (a ~ a))
-> (() :: Constraint) :- (a ~ a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (a ~ a)
(() :: Constraint) => Dict (a ~ a)
forall (a :: Constraint). a => Dict a
Dict
  ccomp :: forall (a :: DISCRETE k) (b :: DISCRETE k) (c :: DISCRETE k).
(b ~ c, a ~ b) :- (a ~ c)
ccomp = ((b ~ c, a ~ b) => Dict (a ~ c)) -> (b ~ c, a ~ b) :- (a ~ c)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Dict (a ~ c)
(b ~ c, a ~ b) => Dict (a ~ c)
forall (a :: Constraint). a => Dict a
Dict
instance PreorderOf (DISCRETE k) where
  type (<=) = (~)