{-# LANGUAGE AllowAmbiguousTypes #-}

{- HLINT ignore "Use elemIndex" -}

-- | The skeleton of the category of __finite sets__: objects are natural numbers (@'FS' n@) and a
-- morphism @'FS' n '~>' 'FS' m@ is a function stored as its table, a length-@n@ vector of indices
-- below @m@. Distributive and cartesian closed (exponentials via the 'Exp' type family), with all
-- structure computed concretely.
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.List qualified as List
import Data.Maybe (fromJust, fromMaybe, isNothing)
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 (..))
import Proarrow.Category.Topos (ElementaryTopos, HasEpiMonoFactorization (..), HasSubobjectClassifier (..))
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..))
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 (CocommutativeComonoid, Comonoid (..), Monoid (..))
import Proarrow.Optic (iso)
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 :: CAT 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)

-- | The skeleton of the category of finite sets: objects are natural numbers and an arrow
-- @'FS' n '~>' 'FS' m@ is a function given by its table.
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 @(FS a) @(FS b) @(FS c) =
    forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @_ @(FS b) @(FS c) ((Ob (FS (UN FS b) || FS (UN FS c)) =>
  (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (Ob (FS (UN FS b) || FS (UN FS c)) =>
    (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
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 a) @(FS (Plus b c)) ((Ob (FS (UN FS a) && FS (Plus (UN FS b) (UN FS c))) =>
  (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (Ob (FS (UN FS a) && FS (Plus (UN FS b) (UN FS c))) =>
    (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
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 a) @(FS b) ((Ob (FS (UN FS a) && FS (UN FS b)) =>
  (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (Ob (FS (UN FS a) && FS (UN FS b)) =>
    (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
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 a) @(FS c) ((Ob (FS (UN FS a) && FS (UN FS c)) =>
  (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (Ob (FS (UN FS a) && FS (UN FS c)) =>
    (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
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 @_ @(FS (Mult a b)) @(FS (Mult a c)) ((Ob
    (FS (Mult (UN FS a) (UN FS b)) || FS (Mult (UN FS a) (UN FS c))) =>
  (a ** (b || c)) ~> ((a ** b) || (a ** c)))
 -> (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (Ob
      (FS (Mult (UN FS a) (UN FS b)) || FS (Mult (UN FS a) (UN FS c))) =>
    (a ** (b || c)) ~> ((a ** b) || (a ** c)))
-> (a ** (b || c)) ~> ((a ** b) || (a ** c))
forall a b. (a -> b) -> a -> b
$
              Vec
  (Mult (UN FS a) (Plus (UN FS b) (UN FS c)))
  (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> FinSet
     (FS (Mult (UN FS a) (Plus (UN FS b) (UN FS c))))
     (FS (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec
   (Mult (UN FS a) (Plus (UN FS b) (UN FS c)))
   (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
 -> FinSet
      (FS (Mult (UN FS a) (Plus (UN FS b) (UN FS c))))
      (FS (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
-> Vec
     (Mult (UN FS a) (Plus (UN FS b) (UN FS c)))
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> FinSet
     (FS (Mult (UN FS a) (Plus (UN FS b) (UN FS c))))
     (FS (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
forall a b. (a -> b) -> a -> b
$
                forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat @a @(Plus b c) (Vec
   (UN FS a)
   (Vec
      (Plus (UN FS b) (UN FS c))
      (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
 -> Vec
      (Mult (UN FS a) (Plus (UN FS b) (UN FS c)))
      (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
-> Vec
     (UN FS a)
     (Vec
        (Plus (UN FS b) (UN FS c))
        (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
-> Vec
     (Mult (UN FS a) (Plus (UN FS b) (UN FS c)))
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
forall a b. (a -> b) -> a -> b
$
                  (Fin (UN FS a)
 -> Vec
      (Plus (UN FS b) (UN FS c))
      (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
-> Vec (UN FS a) (Fin (UN FS a))
-> Vec
     (UN FS a)
     (Vec
        (Plus (UN FS b) (UN FS c))
        (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))))
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)
i ->
                        (Fin (UN FS b)
 -> Fin
      (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> Vec (UN FS b) (Fin (UN FS b))
-> Vec
     (UN FS b)
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
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 (\Fin (UN FS b)
j -> Proxy (Mult (UN FS a) (UN FS c))
-> Fin (Mult (UN FS a) (UN FS b))
-> Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))
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 a c)) (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult @a @b Fin (UN FS a)
i Fin (UN FS b)
j)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @b)
                          Vec
  (UN FS b)
  (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> Vec
     (UN FS c)
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> Vec
     (Plus (UN FS b) (UN FS c))
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ (Fin (UN FS c)
 -> Fin
      (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
-> Vec (UN FS c) (Fin (UN FS c))
-> Vec
     (UN FS c)
     (Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c))))
forall a b. (a -> b) -> Vec (UN FS c) a -> Vec (UN FS c) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\Fin (UN FS c)
j -> Proxy (Mult (UN FS a) (UN FS b))
-> Fin (Mult (UN FS a) (UN FS c))
-> Fin (Plus (Mult (UN FS a) (UN FS b)) (Mult (UN FS a) (UN FS c)))
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 @(Mult a b)) (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult @a @c Fin (UN FS a)
i Fin (UN FS c)
j)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @c)
                    )
                    (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @a)
  distR :: forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(FS a) @(FS b) @(FS c) =
    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 || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (FS (UN FS a) || FS (UN FS b)) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
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 (Plus a b)) @(FS c) ((Ob (FS (Plus (UN FS a) (UN FS b)) && FS (UN FS c)) =>
  ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (FS (Plus (UN FS a) (UN FS b)) && FS (UN FS c)) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
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 a) @(FS c) ((Ob (FS (UN FS a) && FS (UN FS c)) =>
  ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (FS (UN FS a) && FS (UN FS c)) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
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 b) @(FS c) ((Ob (FS (UN FS b) && FS (UN FS c)) =>
  ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob (FS (UN FS b) && FS (UN FS c)) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
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 @_ @(FS (Mult a c)) @(FS (Mult b c)) ((Ob
    (FS (Mult (UN FS a) (UN FS c)) || FS (Mult (UN FS b) (UN FS c))) =>
  ((a || b) ** c) ~> ((a ** c) || (b ** c)))
 -> ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> (Ob
      (FS (Mult (UN FS a) (UN FS c)) || FS (Mult (UN FS b) (UN FS c))) =>
    ((a || b) ** c) ~> ((a ** c) || (b ** c)))
-> ((a || b) ** c) ~> ((a ** c) || (b ** c))
forall a b. (a -> b) -> a -> b
$
              Vec
  (Mult (Plus (UN FS a) (UN FS b)) (UN FS c))
  (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
-> FinSet
     (FS (Mult (Plus (UN FS a) (UN FS b)) (UN FS c)))
     (FS (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec
   (Mult (Plus (UN FS a) (UN FS b)) (UN FS c))
   (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
 -> FinSet
      (FS (Mult (Plus (UN FS a) (UN FS b)) (UN FS c)))
      (FS (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec
     (Mult (Plus (UN FS a) (UN FS b)) (UN FS c))
     (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
-> FinSet
     (FS (Mult (Plus (UN FS a) (UN FS b)) (UN FS c)))
     (FS (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
forall a b. (a -> b) -> a -> b
$
                forall (n :: Nat) (m :: Nat) a. Vec n (Vec m a) -> Vec (Mult n m) a
concat @(Plus a b) @c (Vec
   (Plus (UN FS a) (UN FS b))
   (Vec
      (UN FS c)
      (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
 -> Vec
      (Mult (Plus (UN FS a) (UN FS b)) (UN FS c))
      (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec
     (Plus (UN FS a) (UN FS b))
     (Vec
        (UN FS c)
        (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec
     (Mult (Plus (UN FS a) (UN FS b)) (UN FS c))
     (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
forall a b. (a -> b) -> a -> b
$
                  (Fin (UN FS a)
 -> Vec
      (UN FS c)
      (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec (UN FS a) (Fin (UN FS a))
-> Vec
     (UN FS a)
     (Vec
        (UN FS c)
        (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
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)
i -> (Fin (UN FS c)
 -> Fin
      (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
-> Vec (UN FS c) (Fin (UN FS c))
-> Vec
     (UN FS c)
     (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
forall a b. (a -> b) -> Vec (UN FS c) a -> Vec (UN FS c) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\Fin (UN FS c)
j -> Proxy (Mult (UN FS b) (UN FS c))
-> Fin (Mult (UN FS a) (UN FS c))
-> Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))
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 b c)) (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult @a @c Fin (UN FS a)
i Fin (UN FS c)
j)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @c)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @a)
                    Vec
  (UN FS a)
  (Vec
     (UN FS c)
     (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec
     (UN FS b)
     (Vec
        (UN FS c)
        (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec
     (Plus (UN FS a) (UN FS b))
     (Vec
        (UN FS c)
        (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
forall (n :: Nat) a (m :: Nat).
Vec n a -> Vec m a -> Vec (Plus n m) a
++ (Fin (UN FS b)
 -> Vec
      (UN FS c)
      (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
-> Vec (UN FS b) (Fin (UN FS b))
-> Vec
     (UN FS b)
     (Vec
        (UN FS c)
        (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))))
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 (\Fin (UN FS b)
i -> (Fin (UN FS c)
 -> Fin
      (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
-> Vec (UN FS c) (Fin (UN FS c))
-> Vec
     (UN FS c)
     (Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c))))
forall a b. (a -> b) -> Vec (UN FS c) a -> Vec (UN FS c) b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (\Fin (UN FS c)
j -> Proxy (Mult (UN FS a) (UN FS c))
-> Fin (Mult (UN FS b) (UN FS c))
-> Fin (Plus (Mult (UN FS a) (UN FS c)) (Mult (UN FS b) (UN FS c)))
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 @(Mult a c)) (forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Fin n -> Fin m -> Fin (Mult n m)
mult @b @c Fin (UN FS b)
i Fin (UN FS c)
j)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @c)) (forall (n :: Nat). SNatI n => Vec n (Fin n)
universe @b)
  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 :: CAT 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).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
((a && b) && c) ~> (a && (b && c))
forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(HasBinaryProducts 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).
(HasBinaryProducts k, Ob a, Ob b, Ob c) =>
(a && (b && c)) ~> ((a && b) && c)
forall (a :: FINSET) (b :: FINSET) (c :: FINSET).
(HasBinaryProducts 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 {unFinSet = 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 (SNatI a) => CocommutativeComonoid (FS a)

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

-- | Finds an isomorphism between 'FS n' and itself that's consistent with the given (source, target)
-- pairs, if one exists.
findIso :: forall n. (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 = Vec n (Fin n) -> Iso' (FS n) (FS n)
mkIso (Vec n (Fin n) -> Iso' (FS n) (FS n))
-> Maybe (Vec n (Fin n)) -> Maybe (Iso' (FS n) (FS n))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> [(Fin n, Fin n)] -> Maybe (Vec n (Fin n))
forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (Vec n (Fin n))
findBijection [(Fin n, Fin n)]
ps
  where
    mkIso :: Vec n (Fin n) -> Iso' (FS n) (FS n)
    mkIso :: Vec n (Fin n) -> Iso' (FS n) (FS n)
mkIso Vec n (Fin n)
fwd = (FS n ~> FS n) -> (FS n ~> FS n) -> Iso' (FS n) (FS n)
forall {j} {k} (c :: (j +-> k) -> Constraint) (s :: k) (t :: j)
       (a :: k) (b :: j).
(CategoryOf j, CategoryOf k) =>
(s ~> a) -> (b ~> t) -> Optic c s t a b
iso (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)
fwd) (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
j -> (Fin n -> Bool) -> Vec n (Fin n) -> Fin n
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex (Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin n
j) Vec n (Fin n)
fwd)))

-- | Extends the given (source, target) pairs to a full bijection on @Fin n@, if they're consistent
-- with being a partial injection (checked in both directions as they're added, so two different
-- sources claiming the same target is rejected just as readily as one source getting conflicting
-- targets). Unconstrained sources are matched up with whatever targets are left over, in order.
findBijection :: forall n. (SNatI n) => [(Fin n, Fin n)] -> P.Maybe (Vec n (Fin n))
findBijection :: forall (n :: Nat).
SNatI n =>
[(Fin n, Fin n)] -> Maybe (Vec n (Fin n))
findBijection [(Fin n, Fin n)]
ps = do
  (fwd, bwd) <- Vec n (Maybe (Fin n))
-> Vec n (Maybe (Fin n))
-> [(Fin n, Fin n)]
-> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin 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) (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) [(Fin n, Fin n)]
ps
  let freeSrcs = (Fin n -> Bool) -> [Fin n] -> [Fin n]
forall a. (a -> Bool) -> [a] -> [a]
P.filter (\Fin n
i -> Maybe (Fin n) -> Bool
forall a. Maybe a -> Bool
isNothing (Vec n (Maybe (Fin n))
fwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
i)) (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)
      freeTgts = (Fin n -> Bool) -> [Fin n] -> [Fin n]
forall a. (a -> Bool) -> [a] -> [a]
P.filter (\Fin n
j -> Maybe (Fin n) -> Bool
forall a. Maybe a -> Bool
isNothing (Vec n (Maybe (Fin n))
bwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
j)) (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)
      completion = [Fin n] -> [Fin n] -> [(Fin n, Fin n)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Fin n]
freeSrcs [Fin n]
freeTgts
  P.pure (tabulate (\Fin n
i -> Fin n -> Maybe (Fin n) -> Fin n
forall a. a -> Maybe a -> a
fromMaybe (Maybe (Fin n) -> Fin n
forall a. HasCallStack => Maybe a -> a
fromJust (Fin n -> [(Fin n, Fin n)] -> Maybe (Fin n)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup Fin n
i [(Fin n, Fin n)]
completion)) (Vec n (Maybe (Fin n))
fwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
i)))
  where
    go
      :: Vec n (P.Maybe (Fin n))
      -> Vec n (P.Maybe (Fin n))
      -> [(Fin n, Fin n)]
      -> P.Maybe (Vec n (P.Maybe (Fin n)), Vec n (P.Maybe (Fin n)))
    go :: Vec n (Maybe (Fin n))
-> Vec n (Maybe (Fin n))
-> [(Fin n, Fin n)]
-> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin n)))
go Vec n (Maybe (Fin n))
fwd Vec n (Maybe (Fin n))
bwd [] = (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin n)))
-> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin n)))
forall a. a -> Maybe a
P.Just (Vec n (Maybe (Fin n))
fwd, Vec n (Maybe (Fin n))
bwd)
    go Vec n (Maybe (Fin n))
fwd Vec n (Maybe (Fin n))
bwd ((Fin n
s, Fin n
t) : [(Fin n, Fin n)]
rest) = case (Vec n (Maybe (Fin n))
fwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
s, Vec n (Maybe (Fin n))
bwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
t) of
      (P.Just Fin n
t', Maybe (Fin n)
_) | Fin n
t' Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P./= Fin n
t -> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin n)))
forall a. Maybe a
P.Nothing
      (Maybe (Fin n)
_, P.Just Fin n
s') | Fin n
s' Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P./= Fin n
s -> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin n)))
forall a. Maybe a
P.Nothing
      (Maybe (Fin n), Maybe (Fin n))
_ ->
        Vec n (Maybe (Fin n))
-> Vec n (Maybe (Fin n))
-> [(Fin n, Fin n)]
-> Maybe (Vec n (Maybe (Fin n)), Vec n (Maybe (Fin 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
s then Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
P.Just Fin n
t else Vec n (Maybe (Fin n))
fwd 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 -> Maybe (Fin n)) -> Vec n (Maybe (Fin n))
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin n
j -> if Fin n
j Fin n -> Fin n -> Bool
forall a. Eq a => a -> a -> Bool
P.== Fin n
t then Fin n -> Maybe (Fin n)
forall a. a -> Maybe a
P.Just Fin n
s else Vec n (Maybe (Fin n))
bwd Vec n (Maybe (Fin n)) -> Fin n -> Maybe (Fin n)
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
j))
          [(Fin n, Fin n)]
rest

-- | >>> 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
-- >>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
-- "(FinSet {unFinSet = 2 ::: 3 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 3 ::: 2 ::: 3 ::: VNil})"
instance HasEqualizers FINSET where
  equalize :: forall (a :: FINSET) (b :: FINSET) r.
(a ~> b) -> (a ~> b) -> (forall (e :: FINSET). (e ~> a) -> r) -> r
equalize (FinSet Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) forall (e :: FINSET). (e ~> a) -> r
k =
    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) -> r) -> r
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [Fin n]
groups \Vec n (Fin n)
vec -> (FS n ~> a) -> r
forall (e :: FINSET). (e ~> a) -> 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)
vec)
  factorEqualizer :: forall (e :: FINSET) (x :: FINSET) (e' :: FINSET).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (FinSet Vec n (Fin m)
incl) (FinSet Vec n (Fin m)
h) = 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 m)
Vec n (Fin m)
incl))

-- Example 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
-- >>> (pullback f g \(FinSet l) (FinSet r) -> 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
      gByValue :: IntMap [Fin n]
gByValue = ([Fin n] -> [Fin n] -> [Fin n])
-> [(Int, [Fin n])] -> IntMap [Fin n]
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith (([Fin n] -> [Fin n] -> [Fin n]) -> [Fin n] -> [Fin n] -> [Fin n]
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip [Fin n] -> [Fin n] -> [Fin n]
forall a. [a] -> [a] -> [a]
(P.++)) [(Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum (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), [Item [Fin n]
Fin n
y]) | 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]
      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 <- [Fin n] -> Maybe [Fin n] -> [Fin n]
forall a. a -> Maybe a -> a
fromMaybe [] (Int -> IntMap [Fin n] -> Maybe [Fin n]
forall a. Int -> IntMap a -> Maybe a
IM.lookup (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
x)) IntMap [Fin n]
gByValue)]
    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
  coequalize :: forall (a :: FINSET) (b :: FINSET) r.
(a ~> b) -> (a ~> b) -> (forall (c :: FINSET). (b ~> c) -> r) -> r
coequalize (FinSet @_ @a Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) forall (c :: FINSET). (b ~> c) -> r
k =
    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 (,) 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] -> r) -> r
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [[Fin m]]
groups \Vec n [Fin m]
vec -> (b ~> FS n) -> r
forall (c :: FINSET). (b ~> c) -> r
k (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)))
  factorCoequalizer :: forall (c :: FINSET) (x :: FINSET) (c' :: FINSET).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (FinSet Vec n (Fin m)
q) (FinSet Vec n (Fin m)
h) =
    let reps :: IntMap (Fin n)
reps = (Fin n -> Fin n -> Fin n) -> [(Int, Fin n)] -> IntMap (Fin n)
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith (\Fin n
_ Fin n
old -> Fin n
old) [(Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum (Vec n (Fin m)
q Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! Fin n
b), Fin n
b) | Fin n
b <- 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]
    in Vec m (Fin m) -> FinSet (FS m) (FS m)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet ((Fin m -> Fin m) -> Vec m (Fin m)
forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate (\Fin m
i -> Vec n (Fin m)
h Vec n (Fin m) -> Fin n -> Fin m
forall (n :: Nat) a. Vec n a -> Fin n -> a
! (IntMap (Fin n)
IntMap (Fin n)
reps IntMap (Fin n) -> Int -> Fin n
forall a. IntMap a -> Int -> a
IM.! Fin m -> Int
forall a. Enum a => a -> Int
P.fromEnum Fin m
i)))

-- 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

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