{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Instance.FinSet where

import Data.Fin (Fin (..), fin0, fin1, fin2, split, weakenLeft, weakenRight)
import Data.Maybe (fromMaybe)
import Data.Type.Nat (Mult, Nat (..), Nat0, Nat1, Nat2, Nat3, Plus, SNat (..), SNatI, snat, snatToNatural)
import Data.Vec.Lazy
  ( Vec (..)
  , chunks
  , concat
  , concatMap
  , reifyList
  , repeat
  , tabulate
  , toList
  , universe
  , zipWith
  , (!)
  , (++)
  )
import Prelude (Either (..), Num (..), fromIntegral, ($))
import Prelude qualified as P

import Data.Data (Proxy (..))
import Data.IntMap qualified as IM
import Proarrow.Category.Instance.Bool (BOOL)
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.Distributive (Distributive (..), distLProd, distRProd)
import Proarrow.Core (CAT, CategoryOf (..), Is, Profunctor (..), Promonad (..), UN, dimapDefault)
import Proarrow.Monoid (Comonoid (..), Monoid (..))
import Proarrow.Object.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Object.BinaryProduct
  ( HasBinaryProducts (..)
  , associatorProd
  , associatorProdInv
  , diag
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Object.Exponential (Closed (..))
import Proarrow.Object.Initial (HasInitialObject (..))
import Proarrow.Object.Pullback (Cone (..), Cosink (..), HasPullbacks (..), InternalIn (..))
import Proarrow.Object.Pushout (Cocone (..), HasPushouts (..), Sink (..))
import Proarrow.Object.Terminal (HasTerminalObject (..))
import Proarrow.Optic (Iso', iso)

type data FINSET = FS Nat
type instance UN FS (FS n) = n

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 a && b = FS (Mult (UN FS a) (UN FS 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
  distL0 :: forall (a :: FINSET). Ob a => (a ** InitialObject) ~> InitialObject
distL0 @(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))
  distR0 :: forall (a :: FINSET). Ob a => (InitialObject ** a) ~> InitialObject
distR0 = 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
  par0 :: FinSet Unit Unit
par0 = 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
  par :: forall (x1 :: FINSET) (x2 :: FINSET) (y1 :: FINSET) (y2 :: FINSET).
FinSet x1 x2 -> FinSet y1 y2 -> FinSet (x1 ** y1) (x2 ** y2)
par = (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

-- 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).
(a ~> o) -> (b ~> o) -> Cosink '[a, b]
pullback (FinSet Vec n (Fin m)
f) (FinSet Vec n (Fin m)
g) =
    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) -> Cosink '[a, b])
-> Cosink '[a, b]
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 -> Cone ('PR (FS n)) (L '[a, b]) -> Cosink '[a, b]
forall {k} (a :: k) (as :: [k]). Cone ('PR a) (L as) -> Cosink as
Cone (Cone ('PR (FS n)) (L '[a, b]) -> Cosink '[a, b])
-> Cone ('PR (FS n)) (L '[a, b]) -> Cosink '[a, b]
forall a b. (a -> b) -> a -> b
$ (FS n ~> a)
-> Cone ('PR (FS n)) (L '[b]) -> Cone ('PR (FS n)) (L '[a, b])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (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) (Cone ('PR (FS n)) (L '[b]) -> Cone ('PR (FS n)) (L '[a, b]))
-> Cone ('PR (FS n)) (L '[b]) -> Cone ('PR (FS n)) (L '[a, b])
forall a b. (a -> b) -> a -> b
$ (FS n ~> b)
-> Cone ('PR (FS n)) (L '[]) -> Cone ('PR (FS n)) (L '[b])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (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) Cone ('PR (FS n)) (L '[])
forall {k} (a1 :: k). Ob a1 => Cone ('PR a1) (L '[])
Apex

-- >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> import Proarrow.Object.Pullback (equalizer)
-- >>> 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
-- >>> (case equalizer f g of Cone (Leg (FinSet f) Apex) -> P.show f) :: P.String
-- "2 ::: 3 ::: VNil"

-- 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
-- >>> (case pushout l r of Cospan (FinSet l) (FinSet r) -> (P.show l, P.show r)) :: (P.String, P.String)
-- ("1 ::: 3 ::: 3 ::: VNil","1 ::: 0 ::: 1 ::: 2 ::: 3 ::: VNil")
instance HasPushouts FINSET where
  pushout :: forall (o :: FINSET) (a :: FINSET) (b :: FINSET).
(o ~> a) -> (o ~> b) -> Sink '[a, b]
pushout (FinSet @_ @a Vec n (Fin m)
f) (FinSet @_ @b Vec n (Fin m)
g) =
    let
      sizeA :: Int
sizeA = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat m -> Natural
forall (n :: Nat). SNat n -> Natural
snatToNatural (forall (n :: Nat). SNatI n => SNat n
snat @a))
      sizeB :: Int
sizeB = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat m -> Natural
forall (n :: Nat). SNat n -> Natural
snatToNatural (forall (n :: Nat). SNatI n => SNat n
snat @b))
      toI :: Either (Fin m) (Fin m) -> Int
toI (Left Fin m
a) = Fin m -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Fin m
a
      toI (Right Fin m
b) = Int
sizeA Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Fin m -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Fin m
b
      find :: IntMap Int -> Int -> Int
find IntMap Int
m Int
i = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe Int
i (IntMap Int -> Int -> Int
find IntMap Int
m) (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Int -> IntMap Int -> Maybe Int
forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap Int
m
      union :: IntMap Int -> (Int, Int) -> IntMap Int
union IntMap Int
m (Int
i, Int
j) = let ri :: Int
ri = IntMap Int -> Int -> Int
find IntMap Int
m Int
i; rj :: Int
rj = IntMap Int -> Int -> Int
find IntMap Int
m Int
j in if Int
ri Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
P.== Int
rj then IntMap Int
m else Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
ri Int
rj IntMap Int
m
      unionFind :: IntMap Int
unionFind = (IntMap Int -> (Int, Int) -> IntMap Int)
-> IntMap Int -> Vec n (Int, Int) -> IntMap Int
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 Int -> (Int, Int) -> IntMap Int
union IntMap Int
forall a. IntMap a
IM.empty ((Fin m -> Fin m -> (Int, Int))
-> Vec n (Fin m) -> Vec n (Fin m) -> Vec n (Int, Int)
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 -> (Either (Fin m) (Fin m) -> Int
toI (Fin m -> Either (Fin m) (Fin m)
forall a b. a -> Either a b
Left Fin m
u), Either (Fin m) (Fin m) -> Int
toI (Fin m -> Either (Fin m) (Fin m)
forall a b. b -> Either a b
Right Fin m
v))) Vec n (Fin m)
f Vec n (Fin m)
Vec n (Fin m)
g)
      groups :: [[Int]]
groups = IntMap [Int] -> [[Int]]
forall a. IntMap a -> [a]
IM.elems (IntMap [Int] -> [[Int]]) -> IntMap [Int] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
P.foldl @[] (\IntMap [Int]
m Int
x -> ([Int] -> [Int] -> [Int])
-> Int -> [Int] -> IntMap [Int] -> IntMap [Int]
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IM.insertWith [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
(P.++) (IntMap Int -> Int -> Int
find IntMap Int
unionFind Int
x) [Int
Item [Int]
x] IntMap [Int]
m) IntMap [Int]
forall a. IntMap a
IM.empty [Int
Item [Int]
0 .. Int
sizeA Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
sizeB Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
    in
      [[Int]]
-> (forall (n :: Nat). SNatI n => Vec n [Int] -> Sink '[a, b])
-> Sink '[a, b]
forall a r.
[a] -> (forall (n :: Nat). SNatI n => Vec n a -> r) -> r
reifyList [[Int]]
groups \Vec n [Int]
vec ->
        let mapA :: Vec m (Fin n)
mapA = forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate @a (\Fin m
a -> ([Int] -> Bool) -> Vec n [Int] -> Fin n
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem (Either (Fin m) (Fin m) -> Int
toI (Either (Fin m) (Fin m) -> Int) -> Either (Fin m) (Fin m) -> Int
forall a b. (a -> b) -> a -> b
$ Fin m -> Either (Fin m) (Fin m)
forall a b. a -> Either a b
Left Fin m
a)) Vec n [Int]
vec)
            mapB :: Vec m (Fin n)
mapB = forall (n :: Nat) a. SNatI n => (Fin n -> a) -> Vec n a
tabulate @b (\Fin m
b -> ([Int] -> Bool) -> Vec n [Int] -> Fin n
forall a (n :: Nat). (a -> Bool) -> Vec n a -> Fin n
findIndex (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem (Either (Fin m) (Fin m) -> Int
toI (Either (Fin m) (Fin m) -> Int) -> Either (Fin m) (Fin m) -> Int
forall a b. (a -> b) -> a -> b
$ Fin m -> Either (Fin m) (Fin m)
forall a b. b -> Either a b
Right Fin m
b)) Vec n [Int]
vec)
        in Cocone (L '[a, b]) ('COPR (FS n)) -> Sink '[a, b]
forall {k} (as :: [k]) (a :: k). Cocone (L as) ('COPR a) -> Sink as
Cocone (Cocone (L '[a, b]) ('COPR (FS n)) -> Sink '[a, b])
-> Cocone (L '[a, b]) ('COPR (FS n)) -> Sink '[a, b]
forall a b. (a -> b) -> a -> b
$ (a ~> FS n)
-> Cocone (L '[b]) ('COPR (FS n))
-> Cocone (L '[a, b]) ('COPR (FS n))
forall {k} (b :: k) (a1 :: k) (bs1 :: [k]).
(b ~> a1)
-> Cocone (L bs1) ('COPR a1) -> Cocone (L (b : bs1)) ('COPR a1)
Coleg (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 Vec m (Fin n)
mapA) (Cocone (L '[b]) ('COPR (FS n))
 -> Cocone (L '[a, b]) ('COPR (FS n)))
-> Cocone (L '[b]) ('COPR (FS n))
-> Cocone (L '[a, b]) ('COPR (FS n))
forall a b. (a -> b) -> a -> b
$ (b ~> FS n)
-> Cocone (L '[]) ('COPR (FS n)) -> Cocone (L '[b]) ('COPR (FS n))
forall {k} (b :: k) (a1 :: k) (bs1 :: [k]).
(b ~> a1)
-> Cocone (L bs1) ('COPR a1) -> Cocone (L (b : bs1)) ('COPR a1)
Coleg (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 Vec m (Fin n)
mapB) Cocone (L '[]) ('COPR (FS n))
forall {k} (a1 :: k). Ob a1 => Cocone (L '[]) ('COPR a1)
Coapex

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 Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> (case pullback (source @BOOL @FINSET) (target @BOOL @FINSET) of Cone (Leg (FinSet l) (Leg (FinSet r) Apex)) -> P.show (l, r)) :: P.String
-- "(0 ::: 1 ::: 2 ::: 2 ::: VNil,0 ::: 0 ::: 1 ::: 2 ::: VNil)"
instance BOOL `InternalIn` FINSET where
  type C0 BOOL = FS Nat2 -- Fin0 = FLS, Fin1 = TRU
  type C1 BOOL = FS Nat3 -- Fin0 = Fls, Fin1 = F2T, Fin2 = Tru
  source :: C1 BOOL ~> C0 BOOL
source = Vec ('S ('S Nat1)) (Fin ('S Nat1))
-> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S Nat1)) (Fin ('S Nat1))
 -> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1)))
-> Vec ('S ('S Nat1)) (Fin ('S Nat1))
-> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1))
forall a b. (a -> b) -> a -> b
$ Fin ('S Nat1)
Fin (Plus Nat0 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S Nat1)
-> Vec ('S Nat1) (Fin ('S Nat1))
-> Vec ('S ('S Nat1)) (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S Nat1)
Fin (Plus Nat0 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S Nat1)
-> Vec Nat1 (Fin ('S Nat1)) -> Vec ('S Nat1) (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S Nat1)
Fin (Plus Nat1 Nat1)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S Nat1)
-> Vec Nat0 (Fin ('S Nat1)) -> Vec Nat1 (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S Nat1))
forall a. Vec Nat0 a
VNil
  target :: C1 BOOL ~> C0 BOOL
target = Vec ('S ('S Nat1)) (Fin ('S Nat1))
-> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S Nat1)) (Fin ('S Nat1))
 -> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1)))
-> Vec ('S ('S Nat1)) (Fin ('S Nat1))
-> FinSet (FS ('S ('S Nat1))) (FS ('S Nat1))
forall a b. (a -> b) -> a -> b
$ Fin ('S Nat1)
Fin (Plus Nat0 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S Nat1)
-> Vec ('S Nat1) (Fin ('S Nat1))
-> Vec ('S ('S Nat1)) (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S Nat1)
Fin (Plus Nat1 Nat1)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S Nat1)
-> Vec Nat1 (Fin ('S Nat1)) -> Vec ('S Nat1) (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S Nat1)
Fin (Plus Nat1 Nat1)
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S Nat1)
-> Vec Nat0 (Fin ('S Nat1)) -> Vec Nat1 (Fin ('S Nat1))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S Nat1))
forall a. Vec Nat0 a
VNil
  identity :: C0 BOOL ~> C1 BOOL
identity = Vec ('S Nat1) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S Nat1)) (FS ('S ('S Nat1)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S Nat1) (Fin ('S ('S Nat1)))
 -> FinSet (FS ('S Nat1)) (FS ('S ('S Nat1))))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S Nat1)) (FS ('S ('S Nat1)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S Nat1))
Fin (Plus Nat0 ('S ('S Nat1)))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S ('S Nat1))
-> Vec Nat1 (Fin ('S ('S Nat1)))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus ('S Nat1) Nat1)
forall (n :: Nat). Fin (Plus ('S Nat1) ('S n))
fin2 Fin ('S ('S Nat1))
-> Vec Nat0 (Fin ('S ('S Nat1))) -> Vec Nat1 (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S ('S Nat1)))
forall a. Vec Nat0 a
VNil

  -- 4 different ways to compose, read vertically.
  compose :: Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
compose =
    Cone
  ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
forall {k} (a :: k) (as :: [k]). Cone ('PR a) (L as) -> Cosink as
Cone (Cone
   ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
 -> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
-> Cosink '[C1 BOOL, C1 BOOL, C1 BOOL]
forall a b. (a -> b) -> a -> b
$
      (FS ('S ('S ('S Nat1))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
 -> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1))))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S Nat1))
Fin (Plus Nat0 ('S ('S Nat1)))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S ('S Nat1))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus Nat1 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S ('S Nat1))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus ('S Nat1) Nat1)
forall (n :: Nat). Fin (Plus ('S Nat1) ('S n))
fin2 Fin ('S ('S Nat1))
-> Vec Nat1 (Fin ('S ('S Nat1)))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus ('S Nat1) Nat1)
forall (n :: Nat). Fin (Plus ('S Nat1) ('S n))
fin2 Fin ('S ('S Nat1))
-> Vec Nat0 (Fin ('S ('S Nat1))) -> Vec Nat1 (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S ('S Nat1)))
forall a. Vec Nat0 a
VNil) (Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL])
 -> Cone
      ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL]))
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL])
-> Cone
     ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL, C1 BOOL])
forall a b. (a -> b) -> a -> b
$
        (FS ('S ('S ('S Nat1))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL])
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
 -> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1))))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S Nat1))
Fin (Plus Nat0 ('S ('S Nat1)))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S ('S Nat1))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus Nat0 ('S ('S Nat1)))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S ('S Nat1))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus Nat1 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S ('S Nat1))
-> Vec Nat1 (Fin ('S ('S Nat1)))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus ('S Nat1) Nat1)
forall (n :: Nat). Fin (Plus ('S Nat1) ('S n))
fin2 Fin ('S ('S Nat1))
-> Vec Nat0 (Fin ('S ('S Nat1))) -> Vec Nat1 (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S ('S Nat1)))
forall a. Vec Nat0 a
VNil) (Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL])
 -> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL]))
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL])
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL, C1 BOOL])
forall a b. (a -> b) -> a -> b
$
          (FS ('S ('S ('S Nat1))) ~> C1 BOOL)
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[])
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone ('PR a1) (L bs1) -> Cone ('PR a1) (L (b : bs1))
Leg (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
 -> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1))))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
-> FinSet (FS ('S ('S ('S Nat1)))) (FS ('S ('S Nat1)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S Nat1))
Fin (Plus Nat0 ('S ('S Nat1)))
forall (n :: Nat). Fin (Plus Nat0 ('S n))
fin0 Fin ('S ('S Nat1))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
-> Vec ('S ('S ('S Nat1))) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus Nat1 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S ('S Nat1))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
-> Vec ('S ('S Nat1)) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus Nat1 ('S Nat1))
forall (n :: Nat). Fin (Plus Nat1 ('S n))
fin1 Fin ('S ('S Nat1))
-> Vec Nat1 (Fin ('S ('S Nat1)))
-> Vec ('S Nat1) (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S Nat1))
Fin (Plus ('S Nat1) Nat1)
forall (n :: Nat). Fin (Plus ('S Nat1) ('S n))
fin2 Fin ('S ('S Nat1))
-> Vec Nat0 (Fin ('S ('S Nat1))) -> Vec Nat1 (Fin ('S ('S Nat1)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec Nat0 (Fin ('S ('S Nat1)))
forall a. Vec Nat0 a
VNil) (Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[])
 -> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL]))
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[])
-> Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[C1 BOOL])
forall a b. (a -> b) -> a -> b
$
            Cone ('PR (FS ('S ('S ('S Nat1))))) (L '[])
forall {k} (a1 :: k). Ob a1 => Cone ('PR a1) (L '[])
Apex

type Finite k = k `InternalIn` FINSET