module Proarrow.Category.Instance.PointedHask where

import Data.Kind (Type)
import GHC.Generics (Generic)
import Prelude (Eq, Maybe (..), Show, const, ($), (>>=), type (~))

import Data.Void (Void, absurd)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Applicative (liftA2)
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), CopyDiscard, Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Object.Copower (Copowered (..))
import Proarrow.Object.Initial (HasInitialObject (..), HasZeroObject (..))
import Proarrow.Object.Power (Powered (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))

type data POINTED = P Type
type instance UN P (P a) = a

type Pointed :: CAT POINTED
data Pointed a b where
  Pt :: {forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt :: a -> Maybe b} -> Pointed (P a) (P b)

toHask :: P a ~> P b -> (Maybe a -> Maybe b)
toHask :: forall a b. (P a ~> P b) -> Maybe a -> Maybe b
toHask (Pt a -> Maybe b
f) = (Maybe a -> (a -> Maybe b) -> Maybe b
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Maybe b
f)

instance Profunctor Pointed where
  dimap :: forall (c :: POINTED) (a :: POINTED) (b :: POINTED) (d :: POINTED).
(c ~> a) -> (b ~> d) -> Pointed a b -> Pointed c d
dimap = (c ~> a) -> (b ~> d) -> Pointed a b -> Pointed c d
Pointed c a -> Pointed b d -> Pointed a b -> Pointed c d
forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: POINTED) (b :: POINTED) r.
((Ob a, Ob b) => r) -> Pointed a b -> r
\\ Pt{} = r
(Ob a, Ob b) => r
r
instance Promonad Pointed where
  id :: forall (a :: POINTED). Ob a => Pointed a a
id = (UN P a -> Maybe (UN P a)) -> Pointed (P (UN P a)) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just
  Pt a -> Maybe b
f . :: forall (b :: POINTED) (c :: POINTED) (a :: POINTED).
Pointed b c -> Pointed a b -> Pointed a c
. Pt a -> Maybe b
g = (a -> Maybe b) -> Pointed (P a) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\a
a -> a -> Maybe b
g a
a Maybe b -> (b -> Maybe b) -> Maybe b
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Maybe b
b -> Maybe b
f)

-- | The category of types with an added point and point-preserving morphisms.
instance CategoryOf POINTED where
  type (~>) = Pointed
  type Ob a = (a ~ P (UN P a))

data These a b = This a | That b | These a b
  deriving (These a b -> These a b -> Bool
(These a b -> These a b -> Bool)
-> (These a b -> These a b -> Bool) -> Eq (These a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
$c== :: forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
== :: These a b -> These a b -> Bool
$c/= :: forall a b. (Eq a, Eq b) => These a b -> These a b -> Bool
/= :: These a b -> These a b -> Bool
Eq, Int -> These a b -> ShowS
[These a b] -> ShowS
These a b -> String
(Int -> These a b -> ShowS)
-> (These a b -> String)
-> ([These a b] -> ShowS)
-> Show (These a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> These a b -> ShowS
forall a b. (Show a, Show b) => [These a b] -> ShowS
forall a b. (Show a, Show b) => These a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> These a b -> ShowS
showsPrec :: Int -> These a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => These a b -> String
show :: These a b -> String
$cshowList :: forall a b. (Show a, Show b) => [These a b] -> ShowS
showList :: [These a b] -> ShowS
Show, (forall x. These a b -> Rep (These a b) x)
-> (forall x. Rep (These a b) x -> These a b)
-> Generic (These a b)
forall x. Rep (These a b) x -> These a b
forall x. These a b -> Rep (These a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (These a b) x -> These a b
forall a b x. These a b -> Rep (These a b) x
$cfrom :: forall a b x. These a b -> Rep (These a b) x
from :: forall x. These a b -> Rep (These a b) x
$cto :: forall a b x. Rep (These a b) x -> These a b
to :: forall x. Rep (These a b) x -> These a b
Generic)
instance HasBinaryProducts POINTED where
  type P a && P b = P (These a b)
  withObProd :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> a
fst = (These (UN P a) (UN P b) -> Maybe (UN P a))
-> Pointed (P (These (UN P a) (UN P b))) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\case This UN P a
a -> UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just UN P a
a; That UN P b
_ -> Maybe (UN P a)
forall a. Maybe a
Nothing; These UN P a
a UN P b
_ -> UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just UN P a
a)
  snd :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => (a && b) ~> b
snd = (These (UN P a) (UN P b) -> Maybe (UN P b))
-> Pointed (P (These (UN P a) (UN P b))) (P (UN P b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\case This UN P a
_ -> Maybe (UN P b)
forall a. Maybe a
Nothing; That UN P b
b -> UN P b -> Maybe (UN P b)
forall a. a -> Maybe a
Just UN P b
b; These UN P a
_ UN P b
b -> UN P b -> Maybe (UN P b)
forall a. a -> Maybe a
Just UN P b
b)
  Pt a -> Maybe b
f &&& :: forall (a :: POINTED) (x :: POINTED) (y :: POINTED).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Pt a -> Maybe b
g =
    (a -> Maybe (These b b)) -> Pointed (P a) (P (These b b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt
      ( \a
a -> case (a -> Maybe b
f a
a, a -> Maybe b
g a
a
a) of
          (Just b
a', Just b
b') -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> b -> These b b
forall a b. a -> b -> These a b
These b
a' b
b')
          (Just b
a', Maybe b
Nothing) -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> These b b
forall a b. a -> These a b
This b
a')
          (Maybe b
Nothing, Just b
b') -> These b b -> Maybe (These b b)
forall a. a -> Maybe a
Just (b -> These b b
forall a b. b -> These a b
That b
b')
          (Maybe b
Nothing, Maybe b
Nothing) -> Maybe (These b b)
forall a. Maybe a
Nothing
      )
instance HasTerminalObject POINTED where
  type TerminalObject = P Void
  terminate :: forall (a :: POINTED). Ob a => a ~> TerminalObject
terminate = (UN P a -> Maybe Void) -> Pointed (P (UN P a)) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Maybe Void -> UN P a -> Maybe Void
forall a b. a -> b -> a
const Maybe Void
forall a. Maybe a
Nothing)

instance HasBinaryCoproducts POINTED where
  type P a || P b = P (a || b)
  withObCoprod :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => a ~> (a || b)
lft = (UN P a -> Maybe (Either (UN P a) (UN P b)))
-> Pointed (P (UN P a)) (P (Either (UN P a) (UN P b)))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b))
forall a. a -> Maybe a
Just (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b)))
-> (UN P a -> Either (UN P a) (UN P b))
-> UN P a
-> Maybe (Either (UN P a) (UN P b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P a ~> (UN P a || UN P b)
UN P a -> Either (UN P a) (UN P b)
forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
forall a b. (Ob a, Ob b) => a ~> (a || b)
lft)
  rgt :: forall (a :: POINTED) (b :: POINTED). (Ob a, Ob b) => b ~> (a || b)
rgt = (UN P b -> Maybe (Either (UN P a) (UN P b)))
-> Pointed (P (UN P b)) (P (Either (UN P a) (UN P b)))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b))
forall a. a -> Maybe a
Just (Either (UN P a) (UN P b) -> Maybe (Either (UN P a) (UN P b)))
-> (UN P b -> Either (UN P a) (UN P b))
-> UN P b
-> Maybe (Either (UN P a) (UN P b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. UN P b ~> (UN P a || UN P b)
UN P b -> Either (UN P a) (UN P b)
forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
forall a b. (Ob a, Ob b) => b ~> (a || b)
rgt)
  Pt a -> Maybe b
f ||| :: forall (x :: POINTED) (a :: POINTED) (y :: POINTED).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Pt a -> Maybe b
g = (Either a a -> Maybe b) -> Pointed (P (Either a a)) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a ~> Maybe b
a -> Maybe b
f (a ~> Maybe b) -> (a ~> Maybe b) -> (a || a) ~> Maybe b
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall x a y. (x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a ~> Maybe b
a -> Maybe b
g)
instance HasInitialObject POINTED where
  type InitialObject = P Void
  initiate :: forall (a :: POINTED). Ob a => InitialObject ~> a
initiate = (Void -> Maybe (UN P a)) -> Pointed (P Void) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt Void -> Maybe (UN P a)
forall a. Void -> a
absurd

instance MonoidalProfunctor Pointed where
  par0 :: Pointed Unit Unit
par0 = (() -> Maybe ()) -> Pointed (P ()) (P ())
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt () -> Maybe ()
forall a. a -> Maybe a
Just
  Pt a -> Maybe b
f par :: forall (x1 :: POINTED) (x2 :: POINTED) (y1 :: POINTED)
       (y2 :: POINTED).
Pointed x1 x2 -> Pointed y1 y2 -> Pointed (x1 ** y1) (x2 ** y2)
`par` Pt a -> Maybe b
g = ((a, a) -> Maybe (b, b)) -> Pointed (P (a, a)) (P (b, b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\(a
a, a
b) -> ((b ** b) ~> (b, b)) -> (Maybe b ** Maybe b) ~> Maybe (b, b)
forall a b c.
(Ob a, Ob b) =>
((a ** b) ~> c) -> (Maybe a ** Maybe b) ~> Maybe c
forall {j} {k} (f :: j -> k) (a :: j) (b :: j) (c :: j).
(Applicative f, Ob a, Ob b) =>
((a ** b) ~> c) -> (f a ** f b) ~> f c
liftA2 (b ** b) ~> (b, b)
(b, b) -> (b, b)
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id (a -> Maybe b
f a
a, a -> Maybe b
g a
b))

-- | The smash product of pointed sets.
-- Monoids relative to the smash product are absorption monoids.
instance Monoidal POINTED where
  type Unit = P ()
  type P a ** P b = P (a, b)
  withOb2 :: forall (a :: POINTED) (b :: POINTED) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: POINTED). Ob a => (Unit ** a) ~> a
leftUnitor = (((), UN P a) -> Maybe (UN P a))
-> Pointed (P ((), UN P a)) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just (UN P a -> Maybe (UN P a))
-> (((), UN P a) -> UN P a) -> ((), UN P a) -> Maybe (UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (() && UN P a) ~> UN P a
((), UN P a) -> UN P a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
forall a b. (Ob a, Ob b) => (a && b) ~> b
snd)
  leftUnitorInv :: forall (a :: POINTED). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN P a -> Maybe ((), UN P a))
-> Pointed (P (UN P a)) (P ((), UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (((), UN P a) -> Maybe ((), UN P a)
forall a. a -> Maybe a
Just (((), UN P a) -> Maybe ((), UN P a))
-> (UN P a -> ((), UN P a)) -> UN P a -> Maybe ((), UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. ((),))
  rightUnitor :: forall (a :: POINTED). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN P a, ()) -> Maybe (UN P a))
-> Pointed (P (UN P a, ())) (P (UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (UN P a -> Maybe (UN P a)
forall a. a -> Maybe a
Just (UN P a -> Maybe (UN P a))
-> ((UN P a, ()) -> UN P a) -> (UN P a, ()) -> Maybe (UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (UN P a && ()) ~> UN P a
(UN P a, ()) -> UN P a
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst)
  rightUnitorInv :: forall (a :: POINTED). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN P a -> Maybe (UN P a, ()))
-> Pointed (P (UN P a)) (P (UN P a, ()))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((UN P a, ()) -> Maybe (UN P a, ())
forall a. a -> Maybe a
Just ((UN P a, ()) -> Maybe (UN P a, ()))
-> (UN P a -> (UN P a, ())) -> UN P a -> Maybe (UN P a, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (,()))
  associator :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (((UN P a, UN P b), UN P c) -> Maybe (UN P a, (UN P b, UN P c)))
-> Pointed
     (P ((UN P a, UN P b), UN P c)) (P (UN P a, (UN P b, UN P c)))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\((UN P a
a, UN P b
b), UN P c
c) -> (UN P a, (UN P b, UN P c)) -> Maybe (UN P a, (UN P b, UN P c))
forall a. a -> Maybe a
Just (UN P a
a, (UN P b
b, UN P c
c)))
  associatorInv :: forall (a :: POINTED) (b :: POINTED) (c :: POINTED).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = ((UN P a, (UN P b, UN P c)) -> Maybe ((UN P a, UN P b), UN P c))
-> Pointed
     (P (UN P a, (UN P b, UN P c))) (P ((UN P a, UN P b), UN P c))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\(UN P a
a, (UN P b
b, UN P c
c)) -> ((UN P a, UN P b), UN P c) -> Maybe ((UN P a, UN P b), UN P c)
forall a. a -> Maybe a
Just ((UN P a
a, UN P b
b), UN P c
c))

instance SymMonoidal POINTED where
  swap :: forall (a :: POINTED) (b :: POINTED).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = ((UN P a, UN P b) -> Maybe (UN P b, UN P a))
-> Pointed (P (UN P a, UN P b)) (P (UN P b, UN P a))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((UN P b, UN P a) -> Maybe (UN P b, UN P a)
forall a. a -> Maybe a
Just ((UN P b, UN P a) -> Maybe (UN P b, UN P a))
-> ((UN P a, UN P b) -> (UN P b, UN P a))
-> (UN P a, UN P b)
-> Maybe (UN P b, UN P a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (UN P a ** UN P b) ~> (UN P b ** UN P a)
(UN P a, UN P b) -> (UN P b, UN P a)
forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
forall a b. (Ob a, Ob b) => (a ** b) ~> (b ** a)
swap)

-- This doesn't quite work, see tests.
-- There should be a closed structure, not sure if that can be done in Haskell.
-- https://ncatlab.org/nlab/show/pointed+object#ClosedMonoidalStructure
-- instance Closed POINTED where
--   type P a ~~> P b = P (a -> Maybe b)
--   withObExp r = r
--   curry (Pt f) = Pt (\a -> Just (\b -> f (a, b)))
--   apply = Pt (\(f, b) -> f b)

instance Powered Type POINTED where
  type P a ^ n = P (n -> Maybe a)
  withObPower :: forall (a :: POINTED) n r. (Ob a, Ob n) => (Ob (a ^ n) => r) -> r
withObPower Ob (a ^ n) => r
r = r
Ob (a ^ n) => r
r
  power :: forall (a :: POINTED) (b :: POINTED) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> a ~> (b ^ n)
power n ~> HomObj Type a b
f = (UN P a -> Maybe (n -> Maybe (UN P b)))
-> Pointed (P (UN P a)) (P (n -> Maybe (UN P b)))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (\UN P a
a -> (n -> Maybe (UN P b)) -> Maybe (n -> Maybe (UN P b))
forall a. a -> Maybe a
Just \n
n -> Pointed (P (UN P a)) (P (UN P b)) -> UN P a -> Maybe (UN P b)
forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt (n ~> HomObj Type a b
n -> Pointed (P (UN P a)) (P (UN P b))
f n
n) UN P a
a)
  unpower :: forall (b :: POINTED) n (a :: POINTED).
(Ob b, Ob n) =>
(a ~> (b ^ n)) -> n ~> HomObj Type a b
unpower (Pt a -> Maybe b
f) n
n = (a -> Maybe (UN P b)) -> Pointed (P a) (P (UN P b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \a
a -> a -> Maybe b
f a
a Maybe b -> (b -> Maybe (UN P b)) -> Maybe (UN P b)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((n -> Maybe (UN P b)) -> n -> Maybe (UN P b)
forall a b. (a -> b) -> a -> b
$ n
n)

instance Copowered Type POINTED where
  type n *. P a = P (n, a)
  withObCopower :: forall (a :: POINTED) n r. (Ob a, Ob n) => (Ob (n *. a) => r) -> r
withObCopower Ob (n *. a) => r
r = r
Ob (n *. a) => r
r
  copower :: forall (a :: POINTED) (b :: POINTED) n.
(Ob a, Ob b) =>
(n ~> HomObj Type a b) -> (n *. a) ~> b
copower n ~> HomObj Type a b
f = ((n, UN P a) -> Maybe (UN P b))
-> Pointed (P (n, UN P a)) (P (UN P b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \(n
n, UN P a
a) -> Pointed (P (UN P a)) (P (UN P b)) -> UN P a -> Maybe (UN P b)
forall a b. Pointed (P a) (P b) -> a -> Maybe b
unPt (n ~> HomObj Type a b
n -> Pointed (P (UN P a)) (P (UN P b))
f n
n) UN P a
a
  uncopower :: forall (a :: POINTED) n (b :: POINTED).
(Ob a, Ob n) =>
((n *. a) ~> b) -> n ~> HomObj Type a b
uncopower (Pt a -> Maybe b
f) n
n = (UN P a -> Maybe b) -> Pointed (P (UN P a)) (P b)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \UN P a
a -> a -> Maybe b
f (n
n, UN P a
a)

instance Monoid (P Void) where
  mempty :: Unit ~> P Void
mempty = (() -> Maybe Void) -> Pointed (P ()) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Maybe Void -> () -> Maybe Void
forall a b. a -> b -> a
const Maybe Void
forall a. Maybe a
Nothing)
  mappend :: (P Void ** P Void) ~> P Void
mappend = ((Void, Void) -> Maybe Void) -> Pointed (P (Void, Void)) (P Void)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (Void -> Maybe Void
forall a. a -> Maybe a
Just (Void -> Maybe Void)
-> ((Void, Void) -> Void) -> (Void, Void) -> Maybe Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (Void && Void) ~> Void
(Void, Void) -> Void
forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
forall a b. (Ob a, Ob b) => (a && b) ~> a
fst)

-- | Lift Hask monoids.
memptyDefault :: (Monoid a) => Unit ~> P a
memptyDefault :: forall a. Monoid a => Unit ~> P a
memptyDefault = (() -> Maybe a) -> Pointed (P ()) (P a)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (() -> a) -> () -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Unit ~> a
() -> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty)

mappendDefault :: (Monoid a) => P a ** P a ~> P a
mappendDefault :: forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault = ((a, a) -> Maybe a) -> Pointed (P (a, a)) (P a)
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> ((a, a) -> a) -> (a, a) -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (a ** a) ~> a
(a, a) -> a
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend)

-- | Conjunction with False = Nothing, True = Just ()
instance Monoid (P ()) where
  mempty :: Unit ~> P ()
mempty = Unit ~> P ()
forall a. Monoid a => Unit ~> P a
memptyDefault
  mappend :: (P () ** P ()) ~> P ()
mappend = (P () ** P ()) ~> P ()
forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault

instance Monoid (P [a]) where
  mempty :: Unit ~> P [a]
mempty = Unit ~> P [a]
forall a. Monoid a => Unit ~> P a
memptyDefault
  mappend :: (P [a] ** P [a]) ~> P [a]
mappend = (P [a] ** P [a]) ~> P [a]
forall a. Monoid a => (P a ** P a) ~> P a
mappendDefault

instance Comonoid (P x) where
  counit :: P x ~> Unit
counit = (x -> Maybe ()) -> Pointed (P x) (P ())
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt (() -> Maybe ()
forall a. a -> Maybe a
Just (() -> Maybe ()) -> (x -> ()) -> x -> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> Unit
x -> ()
forall {k} (c :: k). Comonoid c => c ~> Unit
counit)
  comult :: P x ~> (P x ** P x)
comult = (x -> Maybe (x, x)) -> Pointed (P x) (P (x, x))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt ((x, x) -> Maybe (x, x)
forall a. a -> Maybe a
Just ((x, x) -> Maybe (x, x)) -> (x -> (x, x)) -> x -> Maybe (x, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. x ~> (x ** x)
x -> (x, x)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult)
instance CopyDiscard POINTED

-- | Categories with a zero object can be seen as categories enriched in Pointed.
underlyingPt :: (HasZeroObject k) => (a :: k) ~> b -> Unit ~> P (a ~> b)
underlyingPt :: forall k (a :: k) (b :: k).
HasZeroObject k =>
(a ~> b) -> Unit ~> P (a ~> b)
underlyingPt a ~> b
f = (() -> Maybe (a ~> b)) -> Pointed (P ()) (P (a ~> b))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \() -> (a ~> b) -> Maybe (a ~> b)
forall a. a -> Maybe a
Just a ~> b
f

enrichedPt :: (Ob (a :: k), Ob b, HasZeroObject k) => Unit ~> P (a ~> b) -> a ~> b
enrichedPt :: forall k (a :: k) (b :: k).
(Ob a, Ob b, HasZeroObject k) =>
(Unit ~> P (a ~> b)) -> a ~> b
enrichedPt (Pt a -> Maybe b
f) = case a -> Maybe b
f () of Just b
g -> b
a ~> b
g; Maybe b
Nothing -> a ~> b
forall (a :: k) (b :: k). (Ob a, Ob b) => a ~> b
forall k (a :: k) (b :: k). (HasZeroObject k, Ob a, Ob b) => a ~> b
zero

compPt :: (Ob (a :: k), Ob b, Ob c, HasZeroObject k) => P (b ~> c) ** P (a ~> b) ~> P (a ~> c)
compPt :: forall k (a :: k) (b :: k) (c :: k).
(Ob a, Ob b, Ob c, HasZeroObject k) =>
(P (b ~> c) ** P (a ~> b)) ~> P (a ~> c)
compPt = ((b ~> c, a ~> b) -> Maybe (a ~> c))
-> Pointed (P (b ~> c, a ~> b)) (P (a ~> c))
forall a b. (a -> Maybe b) -> Pointed (P a) (P b)
Pt \(b ~> c
bc, a ~> b
ab) -> (a ~> c) -> Maybe (a ~> c)
forall a. a -> Maybe a
Just (b ~> c
bc (b ~> c) -> (a ~> b) -> a ~> c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> b
ab)