Proarrow.Category.Instance.PointedHask
data POINTED Source Comments #
Constructors
The smash product of pointed sets. Monoids relative to the smash product are absorption monoids.
Defined in Proarrow.Category.Instance.PointedHask
Associated Types
Methods
withOb2 :: forall (a :: POINTED) (b :: POINTED) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Comments #
leftUnitor :: forall (a :: POINTED). Ob a => ((Unit :: POINTED) ** a) ~> a Source Comments #
leftUnitorInv :: forall (a :: POINTED). Ob a => a ~> ((Unit :: POINTED) ** a) Source Comments #
rightUnitor :: forall (a :: POINTED). Ob a => (a ** (Unit :: POINTED)) ~> a Source Comments #
rightUnitorInv :: forall (a :: POINTED). Ob a => a ~> (a ** (Unit :: POINTED)) Source Comments #
associator :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Comments #
associatorInv :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Comments #
swap :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Comments #
The category of types with an added point and point-preserving morphisms.
withObCoprod :: forall (a :: POINTED) (b :: POINTED) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Comments #
lft :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => a ~> (a || b) Source Comments #
rgt :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => b ~> (a || b) Source Comments #
(|||) :: forall (x :: POINTED) (a :: POINTED) (y :: POINTED). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Comments #
(+++) :: forall (a :: POINTED) (b :: POINTED) (x :: POINTED) (y :: POINTED). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Comments #
withObProd :: forall (a :: POINTED) (b :: POINTED) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Comments #
fst :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> a Source Comments #
snd :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> b Source Comments #
(&&&) :: forall (a :: POINTED) (x :: POINTED) (y :: POINTED). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Comments #
(***) :: forall (a :: POINTED) (b :: POINTED) (x :: POINTED) (y :: POINTED). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Comments #
withObCopower :: forall (a :: POINTED) n r. Ob a => (Ob (n *. a) => r) -> r Source Comments #
copower :: forall (a :: POINTED) (b :: POINTED) n. (Ob a, Ob b) => (n -> a ~> b) -> (n *. a) ~> b Source Comments #
uncopower :: forall (a :: POINTED) n (b :: POINTED). Ob a => ((n *. a) ~> b) -> n -> a ~> b Source Comments #
withObExp :: forall (a :: POINTED) (b :: POINTED) r. (Ob a, Ob b) => (Ob (a ~~> b) => r) -> r Source Comments #
curry :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Comments #
uncurry :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED). (Ob b, Ob c) => (a ~> (b ~~> c)) -> (a ** b) ~> c Source Comments #
(^^^) :: forall (a :: POINTED) (b :: POINTED) (x :: POINTED) (y :: POINTED). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Comments #
initiate :: forall (a :: POINTED). Ob a => (InitialObject :: POINTED) ~> a Source Comments #
withObPower :: forall (a :: POINTED) n r. Ob a => (Ob (a ^ n) => r) -> r Source Comments #
power :: forall (a :: POINTED) (b :: POINTED) n. (Ob a, Ob b) => (n -> a ~> b) -> a ~> (b ^ n) Source Comments #
unpower :: forall (b :: POINTED) (a :: POINTED) n. Ob b => (a ~> (b ^ n)) -> n -> a ~> b Source Comments #
terminate :: forall (a :: POINTED). Ob a => a ~> (TerminalObject :: POINTED) Source Comments #
id :: forall (a :: POINTED). Ob a => Pointed a a Source Comments #
(.) :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED). Pointed b c -> Pointed a b -> Pointed a c Source Comments #
par0 :: Pointed (Unit :: POINTED) (Unit :: POINTED) Source Comments #
par :: forall (x1 :: POINTED) (x2 :: POINTED) (y1 :: POINTED) (y2 :: POINTED). Pointed x1 x2 -> Pointed y1 y2 -> Pointed (x1 ** y1) (x2 ** y2) Source Comments #
dimap :: forall (c :: POINTED) (a :: POINTED) (b :: POINTED) (d :: POINTED). (c ~> a) -> (b ~> d) -> Pointed a b -> Pointed c d Source Comments #
(\\) :: forall (a :: POINTED) (b :: POINTED) r. ((Ob a, Ob b) => r) -> Pointed a b -> r Source Comments #
counit :: 'P x ~> (Unit :: POINTED) Source Comments #
comult :: 'P x ~> ('P x ** 'P x) Source Comments #
mempty :: (Unit :: POINTED) ~> 'P Void Source Comments #
mappend :: ('P Void ** 'P Void) ~> 'P Void Source Comments #
Conjunction with False = Nothing, True = Just ()
mempty :: (Unit :: POINTED) ~> 'P () Source Comments #
mappend :: ('P () ** 'P ()) ~> 'P () Source Comments #
mempty :: (Unit :: POINTED) ~> 'P [a] Source Comments #
mappend :: ('P [a] ** 'P [a]) ~> 'P [a] Source Comments #
data Pointed (a :: POINTED) (b :: POINTED) where Source Comments #
Fields
toHask :: ('P a ~> 'P b) -> Maybe a -> Maybe b Source Comments #
data These a b Source Comments #
memptyDefault :: Monoid a => (Unit :: POINTED) ~> 'P a Source Comments #
Lift Hask monoids.
mappendDefault :: Monoid a => ('P a ** 'P a) ~> 'P a Source Comments #