{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.FinSet where

import Data.Containers.ListUtils (nubOrd)
import Data.Data (Proxy (..))
import Data.Fin (Fin (..), fin0, fin1, split, weakenLeft, weakenRight)
import Data.IntMap qualified as IM
import Data.Maybe (fromMaybe)
import Data.Type.Nat (Mult, Nat (..), Nat0, Nat1, Nat2, Plus, SNat (..), SNatI, snat)
import Data.Vec.Lazy
  ( Vec (..)
  , chunks
  , concat
  , concatMap
  , reifyList
  , repeat
  , tabulate
  , toList
  , universe
  , zipWith
  , (!)
  , (++)
  )
import Prelude (($))
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.Optic (Iso', iso)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))

type data FINSET = FS Nat

type FinSet :: CAT FINSET
data FinSet a b where
  FinSet :: (SNatI n, SNatI m) => {forall (n :: Nat) (m :: Nat). FinSet (FS n) (FS m) -> Vec n (Fin m)
unFinSet :: Vec n (Fin m)} -> FinSet (FS n) (FS m)

deriving instance P.Show (FinSet a b)
deriving instance P.Eq (FinSet a b)

instance Profunctor FinSet where
  dimap :: forall (c :: FINSET) (a :: FINSET) (b :: FINSET) (d :: FINSET).
(c ~> a) -> (b ~> d) -> FinSet a b -> FinSet c d
dimap = (c ~> a) -> (b ~> d) -> FinSet a b -> FinSet c d
FinSet c a -> FinSet b d -> FinSet a b -> FinSet 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 :: FINSET) (b :: FINSET) r.
((Ob a, Ob b) => r) -> FinSet a b -> r
\\ FinSet{} = r
(Ob a, Ob b) => r
r
instance Promonad FinSet where
  id :: forall (a :: FINSET). Ob a => FinSet a a
id = Vec (UN FS a) (Fin (UN FS a))
-> FinSet (FS (UN FS a)) (FS (UN FS a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet Vec (UN FS a) (Fin (UN FS a))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe
  FinSet Vec n (Fin m)
l . :: forall (b :: FINSET) (c :: FINSET) (a :: FINSET).
FinSet b c -> FinSet a b -> FinSet a c
. FinSet Vec n (Fin m)
r = Vec n (Fin m) -> FinSet (FS n) (FS m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin n -> Fin m) -> Vec n (Fin n) -> Vec n (Fin m)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Vec n (Fin m)
l Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
!) Vec n (Fin n)
Vec n (Fin m)
r)
instance CategoryOf FINSET where
  type (~>) = FinSet
  type Ob a = (Is FS a, SNatI (UN FS a))

instance HasInitialObject FINSET where
  type InitialObject = FS Nat0
  initiate :: forall (a :: FINSET). Ob a => InitialObject ~> a
initiate = Vec Nat0 (Fin (UN FS a)) -> FinSet (FS Nat0) (FS (UN FS a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet Vec Nat0 (Fin (UN FS a))
forall a. Vec Nat0 a
VNil
instance HasBinaryCoproducts FINSET where
  type FS a || FS b = FS (Plus a b)
  withObCoprod :: forall (a :: FINSET) (b :: FINSET) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(FS a) @b Ob (a || b) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @a of
    SNat (UN FS a)
SZ -> r
Ob (a || b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FS a') @b r
Ob (a || b) => r
Ob (FS n1 || b) => r
r
  lft :: forall (a :: FINSET) (b :: FINSET). (Ob a, Ob b) => a ~> (a || b)
lft @(FS a) @(FS b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FS a) @(FS b) ((Ob (FS (UN FS a) || FS (UN FS b)) => a ~> (a || b))
 -> a ~> (a || b))
-> (Ob (FS (UN FS a) || FS (UN FS b)) => a ~> (a || b))
-> a ~> (a || b)
forall a b. (a -> b) -> a -> b
$ Vec (UN FS a) (Fin (Plus (UN FS a) (UN FS b)))
-> FinSet (FS (UN FS a)) (FS (Plus (UN FS a) (UN FS b)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin (UN FS a) -> Fin (Plus (UN FS a) (UN FS b)))
-> Vec (UN FS a) (Fin (UN FS a))
-> Vec (UN FS a) (Fin (Plus (UN FS a) (UN FS b)))
forall a b. (a -> b) -> Vec (UN FS a) a -> Vec (UN FS a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Proxy (UN FS b) -> Fin (UN FS a) -> Fin (Plus (UN FS a) (UN FS b))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy m -> Fin n -> Fin (Plus n m)
weakenLeft (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @b)) Vec (UN FS a) (Fin (UN FS a))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  rgt :: forall (a :: FINSET) (b :: FINSET). (Ob a, Ob b) => b ~> (a || b)
rgt @(FS a) @(FS b) = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FS a) @(FS b) ((Ob (FS (UN FS a) || FS (UN FS b)) => b ~> (a || b))
 -> b ~> (a || b))
-> (Ob (FS (UN FS a) || FS (UN FS b)) => b ~> (a || b))
-> b ~> (a || b)
forall a b. (a -> b) -> a -> b
$ Vec (UN FS b) (Fin (Plus (UN FS a) (UN FS b)))
-> FinSet (FS (UN FS b)) (FS (Plus (UN FS a) (UN FS b)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin (UN FS b) -> Fin (Plus (UN FS a) (UN FS b)))
-> Vec (UN FS b) (Fin (UN FS b))
-> Vec (UN FS b) (Fin (Plus (UN FS a) (UN FS b)))
forall a b. (a -> b) -> Vec (UN FS b) a -> Vec (UN FS b) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Proxy (UN FS a) -> Fin (UN FS b) -> Fin (Plus (UN FS a) (UN FS b))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy n -> Fin m -> Fin (Plus n m)
weakenRight (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @a)) Vec (UN FS b) (Fin (UN FS b))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  FinSet @a Vec n (Fin m)
l ||| :: forall (x :: FINSET) (a :: FINSET) (y :: FINSET).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| FinSet @b Vec n (Fin m)
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FS a) @(FS b) ((Ob (FS n || FS n) => (x || y) ~> a) -> (x || y) ~> a)
-> (Ob (FS n || FS n) => (x || y) ~> a) -> (x || y) ~> a
forall a b. (a -> b) -> a -> b
$ Vec (Plus n n) (Fin m) -> FinSet (FS (Plus n n)) (FS m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec n (Fin m)
l Vec n (Fin m) -> Vec n (Fin m) -> Vec (Plus n n) (Fin m)
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ Vec n (Fin m)
Vec n (Fin m)
r)

instance HasTerminalObject FINSET where
  type TerminalObject = FS Nat1
  terminate :: forall (a :: FINSET). Ob a => a ~> TerminalObject
terminate = Vec (UN FS a) (Fin Nat1) -> FinSet (FS (UN FS a)) (FS Nat1)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Fin Nat1 -> Vec (UN FS a) (Fin Nat1)
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Fin Nat1
Fin (Plus Nat0 Nat1)
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0)
instance HasBinaryProducts FINSET where
  type FS a && FS b = FS (Mult a b)
  withObProd :: forall (a :: FINSET) (b :: FINSET) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(FS a) @b Ob (a && b) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @a of
    SNat (UN FS a)
SZ -> r
Ob (a && b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS a') @b ((Ob (FS n1 && b) => r) -> r) -> (Ob (FS n1 && b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @b @(FS (Mult a' (UN FS b))) r
Ob (a && b) => r
Ob (b || FS (Mult n1 (UN FS b))) => r
r
  fst :: forall (a :: FINSET) (b :: FINSET). (Ob a, Ob b) => (a && b) ~> a
fst @(FS a) @(FS b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS a) @(FS b) ((Ob (FS (UN FS a) && FS (UN FS b)) => (a && b) ~> a)
 -> (a && b) ~> a)
-> (Ob (FS (UN FS a) && FS (UN FS b)) => (a && b) ~> a)
-> (a && b) ~> a
forall a b. (a -> b) -> a -> b
$ Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS a))
-> FinSet (FS (Mult (UN FS a) (UN FS b))) (FS (UN FS a))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat @a @b (Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS a)))
 -> Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS a)))
-> Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS a)))
-> Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS a))
forall a b. (a -> b) -> a -> b
$ (Fin (UN FS a) -> Vec (UN FS b) (Fin (UN FS a)))
-> Vec (UN FS a) (Fin (UN FS a))
-> Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS a)))
forall a b. (a -> b) -> Vec (UN FS a) a -> Vec (UN FS a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Fin (UN FS a) -> Vec (UN FS b) (Fin (UN FS a))
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Vec (UN FS a) (Fin (UN FS a))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  snd :: forall (a :: FINSET) (b :: FINSET). (Ob a, Ob b) => (a && b) ~> b
snd @(FS a) @(FS b) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS a) @(FS b) ((Ob (FS (UN FS a) && FS (UN FS b)) => (a && b) ~> b)
 -> (a && b) ~> b)
-> (Ob (FS (UN FS a) && FS (UN FS b)) => (a && b) ~> b)
-> (a && b) ~> b
forall a b. (a -> b) -> a -> b
$ Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS b))
-> FinSet (FS (Mult (UN FS a) (UN FS b))) (FS (UN FS b))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat @a @b (Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS b)))
 -> Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS b)))
-> Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS b)))
-> Vec (Mult (UN FS a) (UN FS b)) (Fin (UN FS b))
forall a b. (a -> b) -> a -> b
$ Vec (UN FS b) (Fin (UN FS b))
-> Vec (UN FS a) (Vec (UN FS b) (Fin (UN FS b)))
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Vec (UN FS b) (Fin (UN FS b))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)
  FinSet @_ @a Vec n (Fin m)
l &&& :: forall (a :: FINSET) (x :: FINSET) (y :: FINSET).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& FinSet @_ @b Vec n (Fin m)
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS a) @(FS b) ((Ob (FS m && FS m) => a ~> (x && y)) -> a ~> (x && y))
-> (Ob (FS m && FS m) => a ~> (x && y)) -> a ~> (x && y)
forall a b. (a -> b) -> a -> b
$ Vec n (Fin (Mult m m)) -> FinSet (FS n) (FS (Mult m m))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin m -> Fin m -> Fin (Mult m m))
-> Vec n (Fin m) -> Vec n (Fin m) -> Vec n (Fin (Mult m m))
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith Fin m -> Fin m -> Fin (Mult m m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult Vec n (Fin m)
l Vec n (Fin m)
Vec n (Fin m)
r)

instance Distributive FINSET where
  distL :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(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 :: FINSET) (b :: FINSET) (c :: FINSET).
(BiCCC FINSET, Ob a, Ob b, Ob c) =>
(a && (b || c)) ~> ((a && b) || (a && c))
distLProd @a @b @c
  distR :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(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 :: FINSET) (b :: FINSET) (c :: FINSET).
(BiCCC FINSET, Ob a, Ob b, Ob c) =>
((a || b) && c) ~> ((a && c) || (b && c))
distRProd @a @b @c
  absorbL :: forall (a :: FINSET). Ob a => (a ** InitialObject) ~> InitialObject
absorbL @(FS a) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS a) @(FS Z) ((Ob (FS (UN FS a) && FS Nat0) =>
  (a ** InitialObject) ~> InitialObject)
 -> (a ** InitialObject) ~> InitialObject)
-> (Ob (FS (UN FS a) && FS Nat0) =>
    (a ** InitialObject) ~> InitialObject)
-> (a ** InitialObject) ~> InitialObject
forall a b. (a -> b) -> a -> b
$ Vec (Mult (UN FS a) Nat0) (Fin Nat0)
-> FinSet (FS (Mult (UN FS a) Nat0)) (FS Nat0)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat @a @Z (Vec Nat0 (Fin Nat0) -> Vec (UN FS a) (Vec Nat0 (Fin Nat0))
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Vec Nat0 (Fin Nat0)
forall a. Vec Nat0 a
VNil))
  absorbR :: forall (a :: FINSET). Ob a => (InitialObject ** a) ~> InitialObject
absorbR = Vec Nat0 (Fin Nat0) -> FinSet (FS Nat0) (FS Nat0)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet Vec Nat0 (Fin Nat0)
forall a. Vec Nat0 a
VNil

-- >>> import Data.Type.Nat
-- >>> import Data.Fin
-- >>> mult @Nat5 @Nat4 fin4 fin2 -- 4*4+2
-- 18
-- >>> mult @Nat4 @Nat5 fin2 fin4 -- 5*2+4
-- 14
mult :: forall n m. (SNatI n, SNatI m) => Fin n -> Fin m -> Fin (Mult n m)
mult :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult Fin n
n Fin m
m = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> case Fin n
n of {}
  SS @n' -> case Fin n
n of
    Fin n
FZ -> Proxy (Mult n1 m) -> Fin m -> Fin (Plus m (Mult n1 m))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy m -> Fin n -> Fin (Plus n m)
weakenLeft (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @(Mult n' m)) Fin m
m
    FS Fin n1
n' -> Proxy m -> Fin (Mult n1 m) -> Fin (Plus m (Mult n1 m))
forall (n :: Nat) (m :: Nat).
SNatI n =>
Proxy n -> Fin m -> Fin (Plus n m)
weakenRight (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @m) (Fin n1 -> Fin m -> Fin (Mult n1 m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult Fin n1
n' Fin m
m)

unmult :: forall n m. (SNatI n, SNatI m) => Fin (Mult n m) -> (Fin n, Fin m)
unmult :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Mult n m) -> (Fin n, Fin m)
unmult Fin (Mult n m)
f = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> case Fin (Mult n m)
f of {}
  SS @n' -> case forall (n :: Nat) (m :: Nat).
SNatI n =>
Fin (Plus n m) -> Either (Fin n) (Fin m)
split @m @(Mult n' m) Fin (Mult n m)
Fin (Plus m (Mult n1 m))
f of
    P.Left Fin m
m -> (Fin n
Fin ('S n1)
forall (n1 :: Nat). Fin ('S n1)
FZ, Fin m
m)
    P.Right Fin (Mult n1 m)
f' -> let (Fin n1
n, Fin m
m) = forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Mult n m) -> (Fin n, Fin m)
unmult @n' @m Fin (Mult n1 m)
f' in (Fin n1 -> Fin ('S n1)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS Fin n1
n, Fin m
m)

instance MonoidalProfunctor FinSet where
  one :: FinSet Unit Unit
one = FinSet Unit Unit
FinSet (FS Nat1) (FS Nat1)
forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: FINSET). Ob a => FinSet a a
id
  ** :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET).
FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 ** y1) (x2 ** y2)
(**) = (x1 ~> x2) -> (y1 ~> y2) -> (x1 && y1) ~> (x2 && y2)
FinSet x1 x2 -> FinSet y1 y2 -> FinSet (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 :: FINSET) (b :: FINSET) (x :: FINSET) (y :: FINSET).
(a ~> x) -> (b ~> y) -> (a && b) ~> (x && y)
(***)

instance Monoidal FINSET where
  type a ** b = a && b
  type Unit = FS Nat1
  withOb2 :: forall (a :: FINSET) (b :: FINSET) 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 :: FINSET). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ** a) ~> a
(TerminalObject && FS (UN FS a)) ~> FS (UN FS a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(TerminalObject && a) ~> a
leftUnitorProd
  leftUnitorInv :: forall (a :: FINSET). Ob a => a ~> (Unit ** a)
leftUnitorInv = a ~> (Unit ** a)
FS (UN FS a) ~> (TerminalObject && FS (UN FS a))
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (TerminalObject && a)
leftUnitorProdInv
  rightUnitor :: forall (a :: FINSET). Ob a => (a ** Unit) ~> a
rightUnitor = (a ** Unit) ~> a
(FS (UN FS a) && TerminalObject) ~> FS (UN FS a)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
(a && TerminalObject) ~> a
rightUnitorProd
  rightUnitorInv :: forall (a :: FINSET). Ob a => a ~> (a ** Unit)
rightUnitorInv = a ~> (a ** Unit)
FS (UN FS a) ~> (FS (UN FS a) && TerminalObject)
forall {k} (a :: k).
(HasProducts k, Ob a) =>
a ~> (a && TerminalObject)
rightUnitorProdInv
  associator :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(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 :: FINSET) (b :: FINSET) (c :: FINSET).
(HasProducts FINSET, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
associatorProd @a @b @c
  associatorInv :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(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 :: FINSET) (b :: FINSET) (c :: FINSET).
(HasProducts FINSET, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
associatorProdInv @a @b @c

instance SymMonoidal FINSET where
  swap :: forall (a :: FINSET) (b :: FINSET).
(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 :: FINSET) (b :: FINSET).
(HasBinaryProducts FINSET, Ob a, Ob b) =>
(a && b) ~> (b && a)
swapProd @a @b

type family Exp (a :: Nat) (b :: Nat) :: Nat where
  Exp a Z = S Z
  Exp a (S n) = Mult a (Exp a n)

instance Closed FINSET where
  type FS a ~~> FS b = FS (Exp b a)
  withObExp :: forall (a :: FINSET) (b :: FINSET) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @(FS a) @b Ob (a ~~> b) => r
r = case forall (n :: Nat). SNatI n => SNat n
snat @a of
    SNat (UN FS a)
SZ -> r
Ob (a ~~> b) => r
r
    SS @a' -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(FS a') @b ((Ob (FS n1 ~~> b) => r) -> r) -> (Ob (FS n1 ~~> b) => r) -> r
forall a b. (a -> b) -> a -> b
$ forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @b @(FS (Exp (UN FS b) a')) r
Ob (b && FS (Exp (UN FS b) n1)) => r
Ob (a ~~> b) => r
r
  curry :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry @(FS a) @(FS b) (FinSet @_ @c Vec n (Fin m)
f) = forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(FS b) @(FS c) ((Ob (FS (UN FS b) ~~> FS m) => a ~> (b ~~> c)) -> a ~> (b ~~> c))
-> (Ob (FS (UN FS b) ~~> FS m) => a ~> (b ~~> c)) -> a ~> (b ~~> c)
forall a b. (a -> b) -> a -> b
$ Vec (UN FS a) (Fin (Exp m (UN FS b)))
-> FinSet (FS (UN FS a)) (FS (Exp m (UN FS b)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Vec (UN FS b) (Fin m) -> Fin (Exp m (UN FS b)))
-> Vec (UN FS a) (Vec (UN FS b) (Fin m))
-> Vec (UN FS a) (Fin (Exp m (UN FS b)))
forall a b. (a -> b) -> Vec (UN FS a) a -> Vec (UN FS a) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap Vec (UN FS b) (Fin m) -> Fin (Exp m (UN FS b))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> Fin (Exp m n)
exp (forall (n :: Nat) (m :: Nat) a.
(SNatI n, SNatI m) =>
Vec (Mult n m) a -> Vec n (Vec m a)
chunks @a @b Vec n (Fin m)
Vec (Mult (UN FS a) (UN FS b)) (Fin m)
f))
  apply :: forall (a :: FINSET) (b :: FINSET).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply @(FS a) @(FS b) =
    forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(FS a) @(FS b) ((Ob (FS (UN FS a) ~~> FS (UN FS b)) => ((a ~~> b) ** a) ~> b)
 -> ((a ~~> b) ** a) ~> b)
-> (Ob (FS (UN FS a) ~~> FS (UN FS b)) => ((a ~~> b) ** a) ~> b)
-> ((a ~~> b) ** a) ~> b
forall a b. (a -> b) -> a -> b
$
      forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS (Exp b a)) @(FS a) ((Ob (FS (Exp (UN FS b) (UN FS a)) && FS (UN FS a)) =>
  ((a ~~> b) ** a) ~> b)
 -> ((a ~~> b) ** a) ~> b)
-> (Ob (FS (Exp (UN FS b) (UN FS a)) && FS (UN FS a)) =>
    ((a ~~> b) ** a) ~> b)
-> ((a ~~> b) ** a) ~> b
forall a b. (a -> b) -> a -> b
$
        Vec (Mult (Exp (UN FS b) (UN FS a)) (UN FS a)) (Fin (UN FS b))
-> FinSet
     (FS (Mult (Exp (UN FS b) (UN FS a)) (UN FS a))) (FS (UN FS b))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (forall a (m :: Nat) b (n :: Nat).
(a -> Vec m b) -> Vec n a -> Vec (Mult n m) b
concatMap @_ @a @_ @(Exp b a) Fin (Exp (UN FS b) (UN FS a)) -> Vec (UN FS a) (Fin (UN FS b))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Exp m n) -> Vec n (Fin m)
unExp Vec (Exp (UN FS b) (UN FS a)) (Fin (Exp (UN FS b) (UN FS a)))
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe)

-- >>> import Data.Type.Nat
-- >>> import Data.Fin
-- >>> exp @_ @Nat2 (fin1 ::: fin0 ::: fin1 ::: fin1 ::: VNil)
-- 11
exp :: forall n m. (SNatI n, SNatI m) => Vec n (Fin m) -> Fin (Exp m n)
exp :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> Fin (Exp m n)
exp Vec n (Fin m)
VNil = Fin Nat1
Fin (Exp m n)
forall (n1 :: Nat). Fin ('S n1)
FZ
exp (Fin m
x ::: Vec n1 (Fin m)
xs) = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SS @n' -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(FS n') @(FS m) ((Ob (FS n1 ~~> FS m) => Fin (Exp m n)) -> Fin (Exp m n))
-> (Ob (FS n1 ~~> FS m) => Fin (Exp m n)) -> Fin (Exp m n)
forall a b. (a -> b) -> a -> b
$ Fin m -> Fin (Exp m n1) -> Fin (Mult m (Exp m n1))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult Fin m
x (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> Fin (Exp m n)
exp @n' @m Vec n1 (Fin m)
Vec n1 (Fin m)
xs)

-- >>> import Data.Type.Nat
-- >>> import Data.Fin
-- >>> unExp @Nat3 @Nat2 fin6
-- 1 ::: 1 ::: 0 ::: VNil
unExp :: forall n m. (SNatI n, SNatI m) => Fin (Exp m n) -> Vec n (Fin m)
unExp :: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Exp m n) -> Vec n (Fin m)
unExp Fin (Exp m n)
f = case forall (n :: Nat). SNatI n => SNat n
snat @n of
  SNat n
SZ -> Vec n (Fin m)
Vec Nat0 (Fin m)
forall a. Vec Nat0 a
VNil
  SS @n' -> forall k (a :: k) (b :: k) r.
(Closed k, Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp @_ @(FS n') @(FS m) ((Ob (FS n1 ~~> FS m) => Vec n (Fin m)) -> Vec n (Fin m))
-> (Ob (FS n1 ~~> FS m) => Vec n (Fin m)) -> Vec n (Fin m)
forall a b. (a -> b) -> a -> b
$ let (Fin m
x, Fin (Exp m n1)
xs) = forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Mult n m) -> (Fin n, Fin m)
unmult @m @(Exp m n') Fin (Mult m (Exp m n1))
Fin (Exp m n)
f in Fin m
x Fin m -> Vec n1 (Fin m) -> Vec ('S n1) (Fin m)
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Exp m n) -> Vec n (Fin m)
unExp @n' @m Fin (Exp m n1)
xs

-- >>> import Data.Type.Nat
-- >>> comult @(FS Nat4)
-- FinSet (0 ::: 5 ::: 10 ::: 15 ::: VNil)
instance (SNatI a) => Comonoid (FS a) where
  counit :: FS a ~> Unit
counit = FS a ~> Unit
FS a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: FINSET). Ob a => a ~> TerminalObject
terminate
  comult :: FS a ~> (FS a ** FS a)
comult = FS a ~> (FS a ** FS a)
FS a ~> (FS a && FS a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag
instance CopyDiscard FINSET

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

findIso :: (SNatI n) => [(Fin n, Fin n)] -> P.Maybe (Iso' (FS n) (FS n))
findIso :: forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (Iso' (FS n) (FS n))
findIso [(Fin n, Fin n)]
ps = (FS n ~> FS n) -> (FS n ~> FS n) -> Iso (FS n) (FS n) (FS n) (FS n)
FinSet (FS n) (FS n)
-> FinSet (FS n) (FS n) -> Iso (FS n) (FS n) (FS n) (FS n)
forall {j} {k} (s :: k) (t :: j) (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Iso s t a b
iso (FinSet (FS n) (FS n)
 -> FinSet (FS n) (FS n) -> Iso (FS n) (FS n) (FS n) (FS n))
-> Maybe (FinSet (FS n) (FS n))
-> Maybe (FinSet (FS n) (FS n) -> Iso (FS n) (FS n) (FS n) (FS n))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> [(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
findArr [(Fin n, Fin n)]
ps Maybe (FinSet (FS n) (FS n) -> Iso (FS n) (FS n) (FS n) (FS n))
-> Maybe (FinSet (FS n) (FS n))
-> Maybe (Iso (FS n) (FS n) (FS n) (FS n))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
P.<*> [(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
findArr (((Fin n, Fin n) -> (Fin n, Fin n))
-> [(Fin n, Fin n)] -> [(Fin n, Fin n)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Fin n ** Fin n) ~> (Fin n ** Fin n)
(Fin n, Fin n) -> (Fin n, Fin n)
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 [(Fin n, Fin n)]
ps)

findArr :: forall n. (SNatI n) => [(Fin n, Fin n)] -> P.Maybe (FS n ~> FS n)
findArr :: forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
findArr = Vec n (Maybe (Fin n)) -> [(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
go (Maybe (Fin n) -> Vec n (Maybe (Fin n))
forall (n :: Nat) x. SNatI n => x -> Vec n x
repeat Maybe (Fin n)
forall a. Maybe a
P.Nothing)
  where
    go :: Vec n (P.Maybe (Fin n)) -> [(Fin n, Fin n)] -> P.Maybe (FS n ~> FS n)
    go :: Vec n (Maybe (Fin n)) -> [(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
go Vec n (Maybe (Fin n))
v [] = (FS n ~> FS n) -> Maybe (FS n ~> FS n)
forall a. a -> Maybe a
P.Just ((FS n ~> FS n) -> Maybe (FS n ~> FS n))
-> (FS n ~> FS n) -> Maybe (FS n ~> FS n)
forall a b. (a -> b) -> a -> b
$ Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec n (Fin n) -> FinSet (FS n) (FS n))
-> Vec n (Fin n) -> FinSet (FS n) (FS n)
forall a b. (a -> b) -> a -> b
$ (Fin n -> Maybe (Fin n) -> Fin n)
-> Vec n (Fin n) -> Vec n (Maybe (Fin n)) -> Vec n (Fin n)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith Fin n -> Maybe (Fin n) -> Fin n
forall a. a -> Maybe a -> a
fromMaybe Vec n (Fin n)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe Vec n (Maybe (Fin n))
v
    go Vec n (Maybe (Fin n))
v ((Fin n
f1, Fin n
f2) : [(Fin n, Fin n)]
ps) = case Vec n (Maybe (Fin n))
v Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
f1 of
      P.Just Fin n
f | Fin n
f Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P./= Fin n
f2 -> Maybe (FS n ~> FS n)
Maybe (FinSet (FS n) (FS n))
forall a. Maybe a
P.Nothing
      Maybe (Fin n)
_ -> Vec n (Maybe (Fin n)) -> [(Fin n, Fin n)] -> Maybe (FS n ~> FS n)
go ((Fin n -> Maybe (Fin n)) -> Vec n (Maybe (Fin n))
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
i -> if Fin n
i Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin n
f1 then Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
P.Just Fin n
f2 else Vec n (Maybe (Fin n))
v Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
i)) [(Fin n, Fin n)]
ps

-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> let f :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin1 ::: fin0 ::: VNil
-- >>> let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
-- >>> let h :: FinSet (FS Nat3) (FS Nat4) = FinSet $ fin3 ::: fin2 ::: fin3 ::: VNil
-- >>> (case factorEqualizer f g h of p :.: q -> P.show (p, q, q . p)) :: P.String
-- "(FinSet {unFinSet = 1 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 2 ::: 3 ::: VNil},FinSet {unFinSet = 3 ::: 2 ::: 3 ::: VNil})"
instance HasEqualizers FINSET where
  factorEqualizer :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(a ~> b) -> (a ~> b) -> (c ~> a) -> (:.:) (~>) (~>) c a
factorEqualizer (FinSet Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) (FinSet Vec n (Fin m)
h) =
    let groups :: [Fin n]
groups = [Fin n
x | Fin n
x <- Vec n (Fin n) -> [Fin n]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n (Fin n)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe, Vec n (Fin m)
f Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
x Fin m -> Fin m -> Bool
forall a. Eq a => a -> a -> Bool
P.== Vec n (Fin m)
Vec n (Fin m)
g Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
Fin n
x]
    in [Fin n]
-> (forall (n :: Nat).
    SNatI n =>
    Vec n (Fin n) -> (:.:) FinSet FinSet (FS n) (FS n))
-> (:.:) FinSet FinSet (FS n) (FS n)
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [Fin n]
groups \Vec n (Fin n)
vec -> Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin n -> Fin n) -> Vec n (Fin n)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
c -> (Fin m -> Bool) -> Vec n (Fin m) -> Fin n
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex (Fin m -> Fin m -> Bool
forall a. Eq a => a -> a -> Bool
P.== (Vec n (Fin m)
h Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
c)) Vec n (Fin n)
Vec n (Fin m)
vec)) FinSet (FS n) (FS n)
-> FinSet (FS n) (FS n) -> (:.:) FinSet FinSet (FS n) (FS n)
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
:.: Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet Vec n (Fin n)
vec

-- Exercise 3.84 of Seven Sketches (A: 0=red, 1=blue, 2=black)
-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> let f :: FinSet (FS Nat6) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin0 ::: fin0 ::: fin2 ::: fin1 ::: VNil
-- >>> let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
-- >>> (case pullback f g of Cone (Leg (FinSet l) (Leg (FinSet r) Apex)) -> P.show (l, r)) :: P.String
-- "(0 ::: 0 ::: 1 ::: 2 ::: 2 ::: 3 ::: 3 ::: 4 ::: 5 ::: VNil,1 ::: 3 ::: 2 ::: 1 ::: 3 ::: 1 ::: 3 ::: 0 ::: 2 ::: VNil)"
instance HasPullbacks FINSET where
  pullback :: forall (o :: FINSET) (a :: FINSET) (b :: FINSET) r.
(a ~> o)
-> (b ~> o)
-> (forall (p :: FINSET). (p ~> a) -> (p ~> b) -> r)
-> r
pullback (FinSet Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) forall (p :: FINSET). (p ~> a) -> (p ~> b) -> r
k =
    let groups :: [(Fin n, Fin n)]
groups = [(Fin n
x, Fin n
y) | Fin n
x <- Vec n (Fin n) -> [Fin n]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n (Fin n)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe, Fin n
y <- Vec n (Fin n) -> [Fin n]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n (Fin n)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe, Vec n (Fin m)
f Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
x Fin m -> Fin m -> Bool
forall a. Eq a => a -> a -> Bool
P.== Vec n (Fin m)
Vec n (Fin m)
g Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
y]
    in [(Fin n, Fin n)]
-> (forall (n :: Nat). SNatI n => Vec n (Fin n, Fin n) -> r) -> r
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [(Fin n, Fin n)]
groups \Vec n (Fin n, Fin n)
vec -> (FS n ~> a) -> (FS n ~> b) -> r
forall (p :: FINSET). (p ~> a) -> (p ~> b) -> r
k (Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec n (Fin n) -> FinSet (FS n) (FS n))
-> Vec n (Fin n) -> FinSet (FS n) (FS n)
forall a b. (a -> b) -> a -> b
$ ((Fin n, Fin n) -> Fin n) -> Vec n (Fin n, Fin n) -> Vec n (Fin n)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Fin n && Fin n) ~> Fin n
(Fin n, Fin n) -> Fin n
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 Vec n (Fin n, Fin n)
vec) (Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec n (Fin n) -> FinSet (FS n) (FS n))
-> Vec n (Fin n) -> FinSet (FS n) (FS n)
forall a b. (a -> b) -> a -> b
$ ((Fin n, Fin n) -> Fin n) -> Vec n (Fin n, Fin n) -> Vec n (Fin n)
forall a b. (a -> b) -> Vec n a -> Vec n b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Fin n && Fin n) ~> Fin n
(Fin n, Fin n) -> Fin n
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 Vec n (Fin n, Fin n)
vec)

instance HasCoequalizers FINSET where
  factorCoequalizer :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(a ~> b) -> (a ~> b) -> (b ~> c) -> (:.:) (~>) (~>) b c
factorCoequalizer (FinSet @_ @a Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) (FinSet Vec n (Fin m)
h) =
    let
      find :: IntMap a -> a -> a
find IntMap a
m a
i = a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe a
i (IntMap a -> a -> a
find IntMap a
m) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IM.lookup (a -> Int
forall a. Enum a => a -> Int
P.fromEnum a
i) IntMap a
m
      union :: IntMap a -> (a, a) -> IntMap a
union IntMap a
m (a
i, a
j) = let ri :: a
ri = IntMap a -> a -> a
forall {a}. Enum a => IntMap a -> a -> a
find IntMap a
m a
i; rj :: a
rj = IntMap a -> a -> a
forall {a}. Enum a => IntMap a -> a -> a
find IntMap a
m a
j in if a
ri a -> a -> Bool
forall a. Eq a => a -> a -> Bool
P.== a
rj then IntMap a
m else Int -> a -> IntMap a -> IntMap a
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert (a -> Int
forall a. Enum a => a -> Int
P.fromEnum a
ri) a
rj IntMap a
m
      unionFind :: IntMap (Fin m)
unionFind = (IntMap (Fin m) -> (Fin m, Fin m) -> IntMap (Fin m))
-> IntMap (Fin m) -> Vec n (Fin m, Fin m) -> IntMap (Fin m)
forall b a. (b -> a -> b) -> b -> Vec n a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl IntMap (Fin m) -> (Fin m, Fin m) -> IntMap (Fin m)
forall {a}. (Enum a, Eq a) => IntMap a -> (a, a) -> IntMap a
union IntMap (Fin m)
forall a. IntMap a
IM.empty ((Fin m -> Fin m -> (Fin m, Fin m))
-> Vec n (Fin m) -> Vec n (Fin m) -> Vec n (Fin m, Fin m)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\Fin m
u Fin m
v -> (Fin m
u, Fin m
v)) Vec n (Fin m)
f Vec n (Fin m)
Vec n (Fin m)
g)
      step :: IntMap [Fin m] -> Fin m -> IntMap [Fin m]
step IntMap [Fin m]
m Fin m
x = ([Fin m] -> [Fin m] -> [Fin m])
-> Int -> [Fin m] -> IntMap [Fin m] -> IntMap [Fin m]
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith [Fin m] -> [Fin m] -> [Fin m]
forall a. [a] -> [a] -> [a]
(P.++) (Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum (Fin m -> Int) -> Fin m -> Int
forall a b. (a -> b) -> a -> b
$ IntMap (Fin m) -> Fin m -> Fin m
forall {a}. Enum a => IntMap a -> a -> a
find IntMap (Fin m)
unionFind Fin m
x) [Item [Fin m]
Fin m
x] IntMap [Fin m]
m
      groups :: [[Fin m]]
groups = IntMap [Fin m] -> [[Fin m]]
forall a. IntMap a -> [a]
IM.elems (IntMap [Fin m] -> [[Fin m]]) -> IntMap [Fin m] -> [[Fin m]]
forall a b. (a -> b) -> a -> b
$ (IntMap [Fin m] -> Fin m -> IntMap [Fin m])
-> IntMap [Fin m] -> Vec m (Fin m) -> IntMap [Fin m]
forall b a. (b -> a -> b) -> b -> Vec m a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl IntMap [Fin m] -> Fin m -> IntMap [Fin m]
step IntMap [Fin m]
forall a. IntMap a
IM.empty (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @a)
    in
      [[Fin m]]
-> (forall (n :: Nat).
    SNatI n =>
    Vec n [Fin m] -> (:.:) FinSet FinSet (FS m) (FS m))
-> (:.:) FinSet FinSet (FS m) (FS m)
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [[Fin m]]
groups \Vec n [Fin m]
vec ->
        Vec m (Fin n) -> FinSet (FS m) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin m -> Fin n) -> Vec m (Fin n)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin m
a -> ([Fin m] -> Bool) -> Vec n [Fin m] -> Fin n
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex (Fin m -> [Fin m] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem Fin m
a) Vec n [Fin m]
vec))
          FinSet (FS m) (FS n)
-> FinSet (FS n) (FS m) -> (:.:) FinSet FinSet (FS m) (FS m)
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
:.: Vec n (Fin m) -> FinSet (FS n) (FS m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin n -> Fin m) -> Vec n (Fin m)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
i -> Vec n (Fin m)
h Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! (Vec n [Fin m]
Vec n [Fin n]
vec Vec n [Fin n] -> Fin n -> [Fin n]
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
i [Fin n] -> Int -> Fin n
forall a. HasCallStack => [a] -> Int -> a
P.!! Int
0)))

-- Exercise 6.22 of Seven Sketches
-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> let l :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin0 ::: fin1 ::: fin2 ::: VNil
-- >>> let r :: FinSet (FS Nat4) (FS Nat5) = FinSet $ fin0 ::: fin2 ::: fin4 ::: fin4 ::: VNil
-- >>> (pushout l r \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
-- "(1 ::: 3 ::: 3 ::: VNil,1 ::: 0 ::: 1 ::: 2 ::: 3 ::: VNil)"
instance HasPushouts FINSET where
  pushout :: forall (o :: FINSET) (a :: FINSET) (b :: FINSET) r.
(o ~> a)
-> (o ~> b)
-> (forall (p :: FINSET). (a ~> p) -> (b ~> p) -> r)
-> r
pushout = (o ~> a)
-> (o ~> b)
-> (forall (p :: FINSET). (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

findIndex :: (a -> P.Bool) -> Vec n a -> Fin n
findIndex :: forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex a -> Bool
_ Vec n a
VNil = String -> Fin n
forall a. HasCallStack => String -> a
P.error String
"unexpected missing element"
findIndex a -> Bool
f (a
a ::: Vec n1 a
as)
  | a -> Bool
f a
a = Fin n
Fin ('S n1)
forall (n1 :: Nat). Fin ('S n1)
FZ
  | Bool
P.otherwise = Fin n1 -> Fin ('S n1)
forall (n1 :: Nat). Fin n1 -> Fin ('S n1)
FS (Fin n1 -> Fin ('S n1)) -> Fin n1 -> Fin ('S n1)
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> Vec n1 a -> Fin n1
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex a -> Bool
f Vec n1 a
as

-- >>> import Proarrow.Colimit.Pushout (isEpi)
-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> let f :: FinSet (FS Nat3) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: VNil
-- >>> (pushout f f \(FinSet g1) (FinSet g2) -> P.show (g1, g2)) :: P.String
-- "(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
-- >>> isEpi f
-- True
-- >>> import Proarrow.Limit.Pullback (isMono)
-- >>> (pullback f f \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
-- "(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
-- >>> isMono f
-- True
-- >>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
-- >>> (classifyImage f, classifyKernelPair f)
-- (FinSet {unFinSet = 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: VNil})
-- >>> [and, or, implies] :: [FinSet (FS Nat4) (FS Nat2)]
-- [FinSet {unFinSet = 0 ::: 0 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 0 ::: 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 1 ::: 0 ::: 1 ::: VNil}]
-- >>> false :: FinSet (FS Nat1) (FS Nat2)
-- FinSet {unFinSet = 0 ::: VNil}

instance HasSubobjectClassifier FINSET where
  type Omega = FS Nat2
  true :: TerminalObject ~> Omega
true = Vec Nat1 (Fin Nat2) -> FinSet (FS Nat1) (FS Nat2)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec Nat1 (Fin Nat2) -> FinSet (FS Nat1) (FS Nat2))
-> Vec Nat1 (Fin Nat2) -> FinSet (FS Nat1) (FS Nat2)
forall a b. (a -> b) -> a -> b
$ Fin Nat2
Fin (Plus Nat1 Nat1)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin Nat2 -> Vec Nat0 (Fin Nat2) -> Vec Nat1 (Fin Nat2)
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin Nat2)
forall a. Vec Nat0 a
VNil
  classifyGraph :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (a && b) ~> Omega
classifyGraph (FinSet @n @m Vec n (Fin m)
f) = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @_ @(FS n) @(FS m) ((Ob (FS n && FS m) => (a && b) ~> Omega) -> (a && b) ~> Omega)
-> (Ob (FS n && FS m) => (a && b) ~> Omega) -> (a && b) ~> Omega
forall a b. (a -> b) -> a -> b
$ Vec (Mult n m) (Fin Nat2) -> FinSet (FS (Mult n m)) (FS Nat2)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec (Mult n m) (Fin Nat2) -> FinSet (FS (Mult n m)) (FS Nat2))
-> Vec (Mult n m) (Fin Nat2) -> FinSet (FS (Mult n m)) (FS Nat2)
forall a b. (a -> b) -> a -> b
$ (Fin (Mult n m) -> Fin Nat2) -> Vec (Mult n m) (Fin Nat2)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate
    \(forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin (Mult n m) -> (Fin n, Fin m)
unmult @n @m -> (Fin n
n, Fin m
m)) -> if Vec n (Fin m)
f Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
n Fin m -> Fin m -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin m
m then Fin Nat2
Fin (Plus Nat1 Nat1)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 else Fin Nat2
Fin (Plus Nat0 Nat2)
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0

instance HasEpiMonoFactorization FINSET where
  factorize :: forall (a :: FINSET) (b :: FINSET). (a ~> b) -> (:.:) (~>) (~>) a b
factorize (FinSet Vec n (Fin m)
f) = [Fin m]
-> (forall (n :: Nat).
    SNatI n =>
    Vec n (Fin m) -> (:.:) FinSet FinSet (FS n) (FS m))
-> (:.:) FinSet FinSet (FS n) (FS m)
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList ([Fin m] -> [Fin m]
forall a. Ord a => [a] -> [a]
nubOrd (Vec n (Fin m) -> [Fin m]
forall (n :: Nat) a. Vec n a -> [a]
toList Vec n (Fin m)
f)) \Vec n (Fin m)
vec ->
    let revMap :: IntMap (Fin n)
revMap = [(Int, Fin n)] -> IntMap (Fin n)
forall a. [(Int, a)] -> IntMap a
IM.fromList (Vec n (Int, Fin n) -> [(Int, Fin n)]
forall (n :: Nat) a. Vec n a -> [a]
toList ((Fin m -> Fin n -> (Int, Fin n))
-> Vec n (Fin m) -> Vec n (Fin n) -> Vec n (Int, Fin n)
forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith (\Fin m
k Fin n
v -> (Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum Fin m
k, Fin n
v)) Vec n (Fin m)
vec Vec n (Fin n)
forall (n :: Nat). SNatI n => Vec n (Fin n)
universe))
    in Vec n (Fin n) -> FinSet (FS n) (FS n)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin n -> Fin n) -> Vec n (Fin n)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
a -> IntMap (Fin n)
revMap IntMap (Fin n) -> Int -> Fin n
forall a. IntMap a -> Int -> a
IM.! Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum (Vec n (Fin m)
f Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
a)))
         FinSet (FS n) (FS n)
-> FinSet (FS n) (FS m) -> (:.:) FinSet FinSet (FS n) (FS m)
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
:.: Vec n (Fin m) -> FinSet (FS n) (FS m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet Vec n (Fin m)
vec

instance ElementaryTopos FINSET