{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Proarrow.Category.Instance.FinHask where

import Data.Coerce qualified as P
import Data.Containers.ListUtils (nubOrd)
import Data.Data (Proxy (..))
import Data.Kind (Type)
import Data.List (genericLength)
import Data.List qualified as P
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as M
import Data.Universe.Class (Finite (..), Universe (..))
import Data.Universe.Helpers (Tagged (..), retag)
import Data.Void (Void)
import GHC.TypeNats (KnownNat, Nat, natVal, withKnownNat, withSomeSNat)
import Prelude (Bool (..), ($))
import Prelude qualified as P

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..), distLProd, distRProd)
import Proarrow.Category.Topos (ElementaryTopos, HasEpiMonoFactorization (..), HasSubobjectClassifier (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..), pushoutDefault)
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts (..))
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , diag
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))

newtype Fin (n :: Nat) = Fin {forall (n :: Nat). Fin n -> Int
unFin :: P.Int}
  deriving newtype (Fin n -> Fin n -> Bool
(Fin n -> Fin n -> Bool) -> (Fin n -> Fin n -> Bool) -> Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). Fin n -> Fin n -> Bool
== :: Fin n -> Fin n -> Bool
$c/= :: forall (n :: Nat). Fin n -> Fin n -> Bool
/= :: Fin n -> Fin n -> Bool
P.Eq, Eq (Fin n)
Eq (Fin n) =>
(Fin n -> Fin n -> Ordering)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Bool)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> Ord (Fin n)
Fin n -> Fin n -> Bool
Fin n -> Fin n -> Ordering
Fin n -> Fin n -> Fin n
forall (n :: Nat). Eq (Fin n)
forall (n :: Nat). Fin n -> Fin n -> Bool
forall (n :: Nat). Fin n -> Fin n -> Ordering
forall (n :: Nat). Fin n -> Fin n -> Fin n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). Fin n -> Fin n -> Ordering
compare :: Fin n -> Fin n -> Ordering
$c< :: forall (n :: Nat). Fin n -> Fin n -> Bool
< :: Fin n -> Fin n -> Bool
$c<= :: forall (n :: Nat). Fin n -> Fin n -> Bool
<= :: Fin n -> Fin n -> Bool
$c> :: forall (n :: Nat). Fin n -> Fin n -> Bool
> :: Fin n -> Fin n -> Bool
$c>= :: forall (n :: Nat). Fin n -> Fin n -> Bool
>= :: Fin n -> Fin n -> Bool
$cmax :: forall (n :: Nat). Fin n -> Fin n -> Fin n
max :: Fin n -> Fin n -> Fin n
$cmin :: forall (n :: Nat). Fin n -> Fin n -> Fin n
min :: Fin n -> Fin n -> Fin n
P.Ord, Int -> Fin n -> ShowS
[Fin n] -> ShowS
Fin n -> String
(Int -> Fin n -> ShowS)
-> (Fin n -> String) -> ([Fin n] -> ShowS) -> Show (Fin n)
forall (n :: Nat). Int -> Fin n -> ShowS
forall (n :: Nat). [Fin n] -> ShowS
forall (n :: Nat). Fin n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). Int -> Fin n -> ShowS
showsPrec :: Int -> Fin n -> ShowS
$cshow :: forall (n :: Nat). Fin n -> String
show :: Fin n -> String
$cshowList :: forall (n :: Nat). [Fin n] -> ShowS
showList :: [Fin n] -> ShowS
P.Show, Integer -> Fin n
Fin n -> Fin n
Fin n -> Fin n -> Fin n
(Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Fin n -> Fin n)
-> (Integer -> Fin n)
-> Num (Fin n)
forall (n :: Nat). Integer -> Fin n
forall (n :: Nat). Fin n -> Fin n
forall (n :: Nat). Fin n -> Fin n -> Fin n
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: forall (n :: Nat). Fin n -> Fin n -> Fin n
+ :: Fin n -> Fin n -> Fin n
$c- :: forall (n :: Nat). Fin n -> Fin n -> Fin n
- :: Fin n -> Fin n -> Fin n
$c* :: forall (n :: Nat). Fin n -> Fin n -> Fin n
* :: Fin n -> Fin n -> Fin n
$cnegate :: forall (n :: Nat). Fin n -> Fin n
negate :: Fin n -> Fin n
$cabs :: forall (n :: Nat). Fin n -> Fin n
abs :: Fin n -> Fin n
$csignum :: forall (n :: Nat). Fin n -> Fin n
signum :: Fin n -> Fin n
$cfromInteger :: forall (n :: Nat). Integer -> Fin n
fromInteger :: Integer -> Fin n
P.Num)

instance (KnownNat n) => Universe (Fin n) where
  universe :: [Fin n]
universe = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
P.coerce @[P.Int] [Int
Item [Int]
0 .. (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
1)]

instance (KnownNat n) => Finite (Fin n) where
  cardinality :: Tagged (Fin n) Nat
cardinality = Nat -> Tagged (Fin n) Nat
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))

type data FINHASK = FH Type

type FinHask :: CAT FINHASK
data FinHask a b where
  FinHask :: (Ob (FH a), Ob (FH b)) => {forall a b. FinHask (FH a) (FH b) -> Map a b
unFinHask :: Map a b} -> FinHask (FH a) (FH b)

instance P.Show (FinHask a b) where
  show :: FinHask a b -> String
show (FinHask Map a b
m) = Map a b -> String
forall a. Show a => a -> String
P.show Map a b
m
deriving instance P.Eq (FinHask a b)
deriving instance P.Ord (FinHask a b)
instance (Ob a, Ob b) => Universe (FinHask a b) where
  universe :: [FinHask a b]
universe = [(UN FH a, UN FH b)] -> FinHask a b
[(UN FH a, UN FH b)] -> FinHask (FH (UN FH a)) (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList ([(UN FH a, UN FH b)] -> FinHask a b)
-> [[(UN FH a, UN FH b)]] -> [FinHask a b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> (UN FH a -> [(UN FH a, UN FH b)])
-> [UN FH a] -> [[(UN FH a, UN FH b)]]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
P.traverse (\UN FH a
a -> (UN FH a
a,) (UN FH b -> (UN FH a, UN FH b))
-> [UN FH b] -> [(UN FH a, UN FH b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> [UN FH b]
forall a. Universe a => [a]
universe) [UN FH a]
forall a. Universe a => [a]
universe
instance (Ob a, Ob b) => Finite (FinHask a b) where
  cardinality :: Tagged (FinHask a b) Nat
cardinality =
    (Nat -> Nat -> Nat)
-> Tagged (FinHask a b) Nat
-> Tagged (FinHask a b) Nat
-> Tagged (FinHask a b) Nat
forall a b c.
(a -> b -> c)
-> Tagged (FinHask a b) a
-> Tagged (FinHask a b) b
-> Tagged (FinHask a b) c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
P.liftA2
      Nat -> Nat -> Nat
forall a b. (Num a, Integral b) => a -> b -> a
(P.^)
      (forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
forall s b t. Tagged s b -> Tagged t b
retag @_ @_ @(FinHask a b) (forall a. Finite a => Tagged a Nat
cardinality @(UN FH b)))
      (forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
forall s b t. Tagged s b -> Tagged t b
retag @_ @_ @(FinHask a b) (forall a. Finite a => Tagged a Nat
cardinality @(UN FH a)))

(!) :: (P.Ord (UN FH a)) => FinHask a b -> UN FH a -> UN FH b
FinHask Map a b
m ! :: forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! UN FH a
a = case a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
UN FH a
a Map a b
m of
  P.Just b
x -> b
UN FH b
x
  Maybe b
P.Nothing -> String -> UN FH b
forall a. HasCallStack => String -> a
P.error (String -> UN FH b) -> String -> UN FH b
forall a b. (a -> b) -> a -> b
$ String
"Index " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ a -> String
forall a. Show a => a -> String
P.show a
UN FH a
a String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
" out of bounds for " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ Map a b -> String
forall a. Show a => a -> String
P.show Map a b
m

arr :: (Ob (FH a), Ob (FH b)) => (a -> b) -> FinHask (FH a) (FH b)
arr :: forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr a -> b
f = [(a, b)] -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList [(a
x, a -> b
f a
x) | a
x <- [a]
forall a. Finite a => [a]
universeF]

reifyList :: [a] -> (forall l. (Ob (FH l)) => Map l a -> r) -> r
reifyList :: forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [a]
xs forall l. Ob (FH l) => Map l a -> r
k =
  Nat -> (forall (n :: Nat). SNat n -> r) -> r
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat ([a] -> Nat
forall i a. Num i => [a] -> i
genericLength [a]
xs) \ @n SNat n
snat ->
    SNat n -> (KnownNat n => r) -> r
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
snat (forall l. Ob (FH l) => Map l a -> r
k @(Fin n) ([(Fin n, a)] -> Map (Fin n) a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Fin n] -> [a] -> [(Fin n, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Fin n]
forall a. Finite a => [a]
universeF [a]
xs)))

fromList :: (Ob (FH a), Ob (FH b)) => [(a, b)] -> FinHask (FH a) (FH b)
fromList :: forall a b.
(Ob (FH a), Ob (FH b)) =>
[(a, b)] -> FinHask (FH a) (FH b)
fromList = Map a b -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask (Map a b -> FinHask (FH a) (FH b))
-> ([(a, b)] -> Map a b) -> [(a, b)] -> FinHask (FH a) (FH 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
. [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList

toList :: (Ob (FH a), Ob (FH b)) => FinHask (FH a) (FH b) -> [(a, b)]
toList :: forall a b.
(Ob (FH a), Ob (FH b)) =>
FinHask (FH a) (FH b) -> [(a, b)]
toList (FinHask Map a b
m) = Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
Map a b
m

instance Profunctor FinHask where
  dimap :: forall (c :: FINHASK) (a :: FINHASK) (b :: FINHASK) (d :: FINHASK).
(c ~> a) -> (b ~> d) -> FinHask a b -> FinHask c d
dimap = (c ~> a) -> (b ~> d) -> FinHask a b -> FinHask c d
FinHask c a -> FinHask b d -> FinHask a b -> FinHask 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 :: FINHASK) (b :: FINHASK) r.
((Ob a, Ob b) => r) -> FinHask a b -> r
\\ FinHask{} = r
(Ob a, Ob b) => r
r
instance Promonad FinHask where
  id :: forall (a :: FINHASK). Ob a => FinHask a a
id = (UN FH a -> UN FH a) -> FinHask (FH (UN FH a)) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH a -> UN FH a
forall a. Ob a => a -> a
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id
  FinHask Map a b
l . :: forall (b :: FINHASK) (c :: FINHASK) (a :: FINHASK).
FinHask b c -> FinHask a b -> FinHask a c
. FinHask Map a b
r = Map a b -> FinHask (FH a) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a -> b) -> Map a a -> Map a b
forall a b. (a -> b) -> Map a a -> Map a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Map a b
l Map a b -> a -> b
forall k a. Ord k => Map k a -> k -> a
M.!) Map a a
Map a b
r)
instance CategoryOf FINHASK where
  type (~>) = FinHask
  type Ob a = (Is FH a, Finite (UN FH a), P.Ord (UN FH a), P.Show (UN FH a))

instance HasInitialObject FINHASK where
  type InitialObject = FH Void
  initiate :: forall (a :: FINHASK). Ob a => InitialObject ~> a
initiate = Map Void (UN FH a) -> FinHask (FH Void) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map Void (UN FH a)
forall k a. Map k a
M.empty
instance HasBinaryCoproducts FINHASK where
  type FH a || FH b = FH (P.Either a b)
  withObCoprod :: forall (a :: FINHASK) (b :: FINHASK) 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 :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => a ~> (a || b)
lft = (UN FH a -> Either (UN FH a) (UN FH b))
-> FinHask (FH (UN FH a)) (FH (Either (UN FH a) (UN FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH a -> Either (UN FH a) (UN FH b)
forall a b. a -> Either a b
P.Left
  rgt :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => b ~> (a || b)
rgt = (UN FH b -> Either (UN FH a) (UN FH b))
-> FinHask (FH (UN FH b)) (FH (Either (UN FH a) (UN FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr UN FH b -> Either (UN FH a) (UN FH b)
forall a b. b -> Either a b
P.Right
  FinHask Map a b
l ||| :: forall (x :: FINHASK) (a :: FINHASK) (y :: FINHASK).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FinHask Map a b
r = Map (Either a a) b -> FinHask (FH (Either a a)) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a -> Either a a) -> Map a b -> Map (Either a a) b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> Either a a
forall a b. a -> Either a b
P.Left Map a b
l Map (Either a a) b -> Map (Either a a) b -> Map (Either a a) b
forall a. Semigroup a => a -> a -> a
P.<> (a -> Either a a) -> Map a b -> Map (Either a a) b
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys a -> Either a a
forall a b. b -> Either a b
P.Right Map a b
Map a b
r)

instance HasTerminalObject FINHASK where
  type TerminalObject = FH ()
  terminate :: forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate = (UN FH a -> ()) -> FinHask (FH (UN FH a)) (FH ())
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH a
_ -> ()
instance HasBinaryProducts FINHASK where
  type FH a && FH b = FH (a, b)
  withObProd :: forall (a :: FINHASK) (b :: FINHASK) 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 :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => (a && b) ~> a
fst = ((UN FH a, UN FH b) -> UN FH a)
-> FinHask (FH (UN FH a, UN FH b)) (FH (UN FH a))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr (UN FH a, UN FH b) -> UN FH a
forall a b. (a, b) -> a
P.fst
  snd :: forall (a :: FINHASK) (b :: FINHASK). (Ob a, Ob b) => (a && b) ~> b
snd = ((UN FH a, UN FH b) -> UN FH b)
-> FinHask (FH (UN FH a, UN FH b)) (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr (UN FH a, UN FH b) -> UN FH b
forall a b. (a, b) -> b
P.snd
  FinHask Map a b
l &&& :: forall (a :: FINHASK) (x :: FINHASK) (y :: FINHASK).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FinHask Map a b
r =
    Map a (b, b) -> FinHask (FH a) (FH (b, b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask
      ( (a -> b -> b -> Maybe (b, b))
-> (Map a b -> Map a (b, b))
-> (Map a b -> Map a (b, b))
-> Map a b
-> Map a b
-> Map a (b, b)
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
M.mergeWithKey
          (\a
_ b
a b
b -> (b, b) -> Maybe (b, b)
forall a. a -> Maybe a
P.Just (b
a, b
b))
          (\Map a b
_ -> Map a (b, b)
forall k a. Map k a
M.empty)
          (\Map a b
_ -> Map a (b, b)
forall k a. Map k a
M.empty)
          Map a b
l
          Map a b
Map a b
r
      )

instance MonoidalProfunctor FinHask where
  one :: FinHask Unit Unit
one = FinHask Unit Unit
FinHask (FH ()) (FH ())
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINHASK). Ob a => FinHask a a
id
  ** :: forall (x1 :: FINHASK) (x2 :: FINHASK) (y1 :: FINHASK)
       (y2 :: FINHASK).
FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2)
(**) = (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
FinHask x1 x2 -> FinHask y1 y2 -> FinHask (x1 ** y1) (x2 ** y2)
forall k (a :: k) (b :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
forall (a :: FINHASK) (b :: FINHASK) (x :: FINHASK) (y :: FINHASK).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***)

instance Monoidal FINHASK where
  type a ** b = a && b
  type Unit = TerminalObject
  withOb2 :: forall (a :: FINHASK) (b :: FINHASK) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @a @b = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @a @b
  leftUnitor :: forall (a :: FINHASK). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && FH (UN FH a)) ~> FH (UN FH a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: FINHASK). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
FH (UN FH a) ~> (TerminalObject && FH (UN FH a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: FINHASK). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(FH (UN FH a) && TerminalObject) ~> FH (UN FH a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: FINHASK). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
FH (UN FH a) ~> (FH (UN FH a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(HasProducts FINHASK, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(HasProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(HasProducts FINHASK, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c

instance SymMonoidal FINHASK where
  swap :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @a @b = forall {k} (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> (b && a)
forall (a :: FINHASK) (b :: FINHASK).
(HasBinaryProducts FINHASK, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

instance Closed FINHASK where
  type a ~~> b = FH (FinHask a b)
  withObExp :: forall (a :: FINHASK) (b :: FINHASK) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry f :: (a ** b) ~> c
f@FinHask{} = (UN FH a -> FinHask (FH (UN FH b)) (FH b))
-> FinHask (FH (UN FH a)) (FH (FinHask (FH (UN FH b)) (FH b)))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH a
a -> (UN FH b -> b) -> FinHask (FH (UN FH b)) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \UN FH b
b -> (a ** b) ~> c
FinHask (FH (UN FH a, UN FH b)) (FH b)
f FinHask (FH (UN FH a, UN FH b)) (FH b)
-> UN FH (FH (UN FH a, UN FH b)) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! (UN FH a
a, UN FH b
b)
  apply :: forall (a :: FINHASK) (b :: FINHASK).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = ((FinHask (FH (UN FH a)) (FH (UN FH b)), UN FH a) -> UN FH b)
-> FinHask
     (FH (FinHask (FH (UN FH a)) (FH (UN FH b)), UN FH a))
     (FH (UN FH b))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(FinHask (FH (UN FH a)) (FH (UN FH b))
m, UN FH a
x) -> FinHask (FH (UN FH a)) (FH (UN FH b))
m FinHask (FH (UN FH a)) (FH (UN FH b))
-> UN FH (FH (UN FH a)) -> UN FH (FH (UN FH b))
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! UN FH a
UN FH (FH (UN FH a))
x

instance Distributive FINHASK where
  distL :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(BiCCC FINHASK, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c
  distR :: forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @a @b @c = forall {k} (a :: k) (b :: k) (c :: k).
(BiCCC k, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
forall (a :: FINHASK) (b :: FINHASK) (c :: FINHASK).
(BiCCC FINHASK, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c
  absorbL :: forall (a :: FINHASK).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL = Map (UN FH a, Void) Void -> FinHask (FH (UN FH a, Void)) (FH Void)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map (UN FH a, Void) Void
forall k a. Map k a
M.empty
  absorbR :: forall (a :: FINHASK).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR = Map (Void, UN FH a) Void -> FinHask (FH (Void, UN FH a)) (FH Void)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map (Void, UN FH a) Void
forall k a. Map k a
M.empty

instance (Ob (FH a)) => Comonoid (FH a) where
  counit :: FH a ~> Unit
counit = FH a ~> Unit
FH a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate
  comult :: FH a ~> (FH a ** FH a)
comult = FH a ~> (FH a ** FH a)
FH a ~> (FH a && FH a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag

instance CopyDiscard FINHASK

instance Monoid (FH ()) where
  mempty :: Unit ~> FH ()
mempty = Unit ~> FH ()
FH () ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate
  mappend :: (FH () ** FH ()) ~> FH ()
mappend = (FH () ** FH ()) ~> FH ()
FH ((), ()) ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINHASK). Ob a => a ~> TerminalObject
terminate

-- | >>> let f :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,1), (2,1), (3,0)]
-- >>> let g :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1), (3,0)]
-- >>> let h :: FinHask (FH (Fin 3)) (FH (Fin 4)) = fromList [(0,3), (1,2), (2,3)]
-- >>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
-- "(fromList [(0,2),(1,3)],fromList [(0,1),(1,0),(2,1)],fromList [(0,3),(1,2),(2,3)])"
instance HasEqualizers FINHASK where
  equalize :: forall (a :: FINHASK) (b :: FINHASK) r.
(a ~> b) -> (a ~> b) -> (forall (e :: FINHASK). (e ~> a) -> r) -> r
equalize f :: a ~> b
f@FinHask{} a ~> b
g forall (e :: FINHASK). (e ~> a) -> r
k =
    let groups :: [a]
groups = [a
x | a
x <- [a]
forall a. Finite a => [a]
universeF, a ~> b
FinHask (FH a) (FH b)
f FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
x UN FH (FH b) -> UN FH (FH b) -> Bool
forall a. Eq a => a -> a -> Bool
P.== a ~> b
FinHask (FH a) (FH b)
g FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
x]
    in [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [a]
groups \Map l a
e -> (FH l ~> a) -> r
forall (e :: FINHASK). (e ~> a) -> r
k (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map l a
e)
  factorEqualizer :: forall (e :: FINHASK) (x :: FINHASK) (e' :: FINHASK).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (FinHask Map a b
incl) (FinHask Map a b
h) =
    let invIncl :: Map b a
invIncl = [(b, a)] -> Map b a
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(b
v, a
ky) | (a
ky, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
incl]
    in Map a a -> FinHask (FH a) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((Map b a
invIncl Map b a -> b -> a
forall k a. Ord k => Map k a -> k -> a
M.!) (b -> a) -> Map a b -> Map a a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map a b
Map a b
h)

-- | Example 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black)
-- >>> data Color = Red | Blue | Black deriving (P.Eq, P.Ord, P.Show, P.Enum, P.Bounded, Universe, Finite)
-- >>> let f :: FinHask (FH (Fin 6)) (FH Color) = fromList [(0,Red), (1,Blue), (2,Red), (3,Red), (4,Black), (5,Blue)]
-- >>> let g :: FinHask (FH (Fin 4)) (FH Color) = fromList [(0,Black), (1,Red), (2,Blue), (3,Red)]
-- >>> (pullback f g \(FinHask l) (FinHask r) -> P.show (P.zip (M.elems l) (M.elems r))) :: P.String
-- "[(0,1),(0,3),(1,2),(2,1),(2,3),(3,1),(3,3),(4,0),(5,2)]"
instance HasPullbacks FINHASK where
  pullback :: forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (FinHask Map a b
f) (FinHask Map a b
g) forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r
k =
    let
      gByValue :: Map b [a]
gByValue = ([a] -> [a] -> [a]) -> [(b, [a])] -> Map b [a]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith (([a] -> [a] -> [a]) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(P.++)) [(b
v, [a
Item [a]
y]) | (a
y, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
g]
      groups :: [(a, a)]
groups = [(a
x, a
y) | (a
x, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
f, a
y <- [a] -> b -> Map b [a] -> [a]
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault [] b
v Map b [a]
Map b [a]
gByValue]
    in
      [(a, a)] -> (forall l. Ob (FH l) => Map l (a, a) -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [(a, a)]
groups \Map l (a, a)
e -> (FH l ~> a) -> (FH l ~> b) -> r
forall (p :: FINHASK). (p ~> a) -> (p ~> b) -> r
k (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a, a) -> a
forall a b. (a, b) -> a
P.fst ((a, a) -> a) -> Map l (a, a) -> Map l a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map l (a, a)
e)) (Map l a -> FinHask (FH l) (FH a)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((a, a) -> a
forall a b. (a, b) -> b
P.snd ((a, a) -> a) -> Map l (a, a) -> Map l a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map l (a, a)
e))

instance HasCoequalizers FINHASK where
  coequalize :: forall (a :: FINHASK) (b :: FINHASK) r.
(a ~> b) -> (a ~> b) -> (forall (c :: FINHASK). (b ~> c) -> r) -> r
coequalize (FinHask @_ @b Map a b
f) (FinHask Map a b
g) forall (c :: FINHASK). (b ~> c) -> r
k =
    let
      find :: Map a a -> a -> a
find Map a a
m a
i = a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe a
i (Map a a -> a -> a
find Map a a
m) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ a -> Map a a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
i Map a a
m
      union :: Map a a -> (a, a) -> Map a a
union Map a a
m (a
i, a
j) = let ri :: a
ri = Map a a -> a -> a
forall {a}. Ord a => Map a a -> a -> a
find Map a a
m a
i; rj :: a
rj = Map a a -> a -> a
forall {a}. Ord a => Map a a -> a -> a
find Map a a
m a
j in if a
ri a -> a -> Bool
forall a. Eq a => a -> a -> Bool
P.== a
rj then Map a a
m else a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
ri a
rj Map a a
m
      unionFind :: Map b b
unionFind = (Map b b -> (b, b) -> Map b b) -> Map b b -> [(b, b)] -> Map b b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl Map b b -> (b, b) -> Map b b
forall {a}. Ord a => Map a a -> (a, a) -> Map a a
union Map b b
forall k a. Map k a
M.empty ([b] -> [b] -> [(b, b)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
f) (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
Map a b
g))
      step :: Map b [b] -> b -> Map b [b]
step Map b [b]
m b
x = ([b] -> [b] -> [b]) -> b -> [b] -> Map b [b] -> Map b [b]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
(P.++) (Map b b -> b -> b
forall {a}. Ord a => Map a a -> a -> a
find Map b b
unionFind b
x) [b
Item [b]
x] Map b [b]
m
      groups :: [[b]]
groups = Map b [b] -> [[b]]
forall k a. Map k a -> [a]
M.elems (Map b [b] -> [[b]]) -> Map b [b] -> [[b]]
forall a b. (a -> b) -> a -> b
$ (Map b [b] -> b -> Map b [b]) -> Map b [b] -> [b] -> Map b [b]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl Map b [b] -> b -> Map b [b]
step Map b [b]
forall k a. Map k a
M.empty (forall a. Finite a => [a]
universeF @b)
    in
      [[b]] -> (forall l. Ob (FH l) => Map l [b] -> r) -> r
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList [[b]]
groups \Map l [b]
ce ->
        let invMap :: Map b l
invMap = [(b, l)] -> Map b l
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(b, l)] -> Map b l) -> [(b, l)] -> Map b l
forall a b. (a -> b) -> a -> b
$ ((l, [b]) -> [(b, l)]) -> [(l, [b])] -> [(b, l)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
P.concatMap (\(l
l, [b]
bs) -> (b -> (b, l)) -> [b] -> [(b, l)]
forall a b. (a -> b) -> [a] -> [b]
P.map (,l
l) [b]
bs) ([(l, [b])] -> [(b, l)]) -> [(l, [b])] -> [(b, l)]
forall a b. (a -> b) -> a -> b
$ Map l [b] -> [(l, [b])]
forall k a. Map k a -> [(k, a)]
M.toList Map l [b]
ce
        in (b ~> FH l) -> r
forall (c :: FINHASK). (b ~> c) -> r
k (Map b l -> FinHask (FH b) (FH l)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map b l
invMap)
  factorCoequalizer :: forall (c :: FINHASK) (x :: FINHASK) (c' :: FINHASK).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (FinHask Map a b
q) (FinHask Map a b
h) =
    let reps :: Map b a
reps = (a -> a -> a) -> [(b, a)] -> Map b a
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith (\a
_ a
old -> a
old) [(b
v, a
ky) | (a
ky, b
v) <- Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
M.toList Map a b
q]
    in Map b b -> FinHask (FH b) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((Map a b
h Map a b -> a -> b
forall k a. Ord k => Map k a -> k -> a
M.!) (a -> b) -> Map b a -> Map b b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Map b a
Map b a
reps)

-- | Exercise 6.22 of Seven Sketches
-- >>> let l :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,0), (2,1), (3,2)]
-- >>> let r :: FinHask (FH (Fin 4)) (FH (Fin 5)) = fromList [(0,0), (1,2), (2,4), (3,4)]
-- >>> (pushout l r \l' r' -> P.show (l', r')) :: P.String
-- "(fromList [(0,1),(1,3),(2,3)],fromList [(0,1),(1,0),(2,1),(3,2),(4,3)])"
instance HasPushouts FINHASK where
  pushout :: forall (o :: FINHASK) (a :: FINHASK) (b :: FINHASK) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FINHASK). (a ~> p) -> (b ~> p) -> r)
-> r
pushout = (o ~> a)
-> (o ~> b)
-> (forall (p :: FINHASK). (a ~> p) -> (b ~> p) -> r)
-> r
forall {k} (o :: k) (a :: k) (b :: k) r.
(HasCoequalizers k, HasCoproducts k) =>
(o ~> a)
-> (o ~> b) -> (forall (p :: k). (a ~> p) -> (b ~> p) -> r) -> r
pushoutDefault

-- | >>> import Proarrow.Colimit.Pushout (isEpi)
-- >>> let f :: FinHask (FH (Fin 3)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1)]
-- >>> (pushout f f \(FinHask g1) (FinHask g2) -> P.show (g1, g2)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isEpi (f :: FinHask (FH (Fin 3)) (FH (Fin 3)))
-- True
-- >>> import Proarrow.Limit.Pullback (isMono)
-- >>> (pullback f f \(FinHask l) (FinHask r) -> P.show (l, r)) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
-- >>> isMono f
-- True
-- >>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
-- >>> (case factorize f of p :.: q -> P.show (p, q) \\ p \\ q) :: P.String
-- "(fromList [(0,0),(1,1),(2,2)],fromList [(0,2),(1,0),(2,1)])"
-- >>> (classifyImage f, classifyKernelPair f)
-- (fromList [(0,True),(1,True),(2,True)],fromList [((0,0),True),((0,1),False),((0,2),False),((1,0),False),((1,1),True),((1,2),False),((2,0),False),((2,1),False),((2,2),True)])
-- >>> [and, or, implies] :: [FinHask (FH (Bool, Bool)) (FH Bool)]
-- [fromList [((False,False),False),((False,True),False),((True,False),False),((True,True),True)],fromList [((False,False),False),((False,True),True),((True,False),True),((True,True),True)],fromList [((False,False),True),((False,True),True),((True,False),False),((True,True),True)]]
-- >>> false :: FinHask (FH ()) (FH Bool)
-- fromList [((),False)]
instance HasSubobjectClassifier FINHASK where
  type Omega = FH Bool
  true :: TerminalObject ~> Omega
true = (() -> Bool) -> FinHask (FH ()) (FH Bool)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \()
_ -> Bool
True
  classifyGraph :: forall (a :: FINHASK) (b :: FINHASK). (a ~> b) -> (a && b) ~> Omega
classifyGraph f :: a ~> b
f@FinHask{} = ((a, b) -> Bool) -> FinHask (FH (a, b)) (FH Bool)
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(a
a, b
b) -> a ~> b
FinHask (FH a) (FH b)
f FinHask (FH a) (FH b) -> UN FH (FH a) -> UN FH (FH b)
forall (a :: FINHASK) (b :: FINHASK).
Ord (UN FH a) =>
FinHask a b -> UN FH a -> UN FH b
! a
UN FH (FH a)
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
P.== b
b

instance HasEpiMonoFactorization FINHASK where
  factorize :: forall (a :: FINHASK) (b :: FINHASK).
(a ~> b) -> (:.:) (~>) (~>) a b
factorize (FinHask Map a b
f) = [b]
-> (forall l.
    Ob (FH l) =>
    Map l b -> (:.:) FinHask FinHask (FH a) (FH b))
-> (:.:) FinHask FinHask (FH a) (FH b)
forall a r. [a] -> (forall l. Ob (FH l) => Map l a -> r) -> r
reifyList ([b] -> [b]
forall a. Ord a => [a] -> [a]
nubOrd (Map a b -> [b]
forall k a. Map k a -> [a]
M.elems Map a b
f)) \Map l b
lb ->
    let invMap :: Map b l
invMap = [(b, l)] -> Map b l
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Map l b
lb Map l b -> l -> b
forall k a. Ord k => Map k a -> k -> a
M.! l
l, l
l) | l
l <- [l]
forall a. Finite a => [a]
universeF]
    in Map a l -> FinHask (FH a) (FH l)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask ((b -> l) -> Map a b -> Map a l
forall a b. (a -> b) -> Map a a -> Map a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Map b l
invMap Map b l -> b -> l
forall k a. Ord k => Map k a -> k -> a
M.!) Map a b
f) FinHask (FH a) (FH l)
-> FinHask (FH l) (FH b) -> (:.:) FinHask FinHask (FH a) (FH b)
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: Map l b -> FinHask (FH l) (FH b)
forall a b.
(Ob (FH a), Ob (FH b)) =>
Map a b -> FinHask (FH a) (FH b)
FinHask Map l b
lb

instance ElementaryTopos FINHASK