{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Internal categories: @ik \`InternalIn\` k@ is a category internal to @k@, given by an object of
-- objects @'C0' ik@, an object of arrows @'C1' ik@, and source\/target\/identity\/composition
-- structure maps.
--
-- Internal to finite sets these are the finite categories, and each direction needs a different
-- presentation of finite sets. A 'FiniteCat' counts its arrows only at the value level, so it is
-- internal to 'Proarrow.Category.Instance.FinHask.FINHASK'. Going back,
-- 'Proarrow.Category.Enriched.Thin.Enumerable' wants the object list as a type, which only the
-- skeleton 'Proarrow.Category.Instance.FinSet.FINSET' supplies, so 'INTERNAL' is built from an
-- internal category in @FINSET@.
module Proarrow.Category.Internal where

import Prelude (($))
import Prelude qualified as P

import Data.Fin (fin0, fin1, fin2, toNatural)
import Data.Kind (Type)
import Data.List (elemIndex, genericIndex, genericLength)
import Data.Proxy (Proxy (..))
import Data.Type.Nat (Nat2, Nat3, SNatI, reify, snat)
import Data.Type.Nat qualified as N
import Data.Universe.Class qualified as U
import Data.Vec.Lazy (Vec (..))
import Data.Vec.Lazy qualified as Vec
import Numeric.Natural (Natural)
import Proarrow.Category.Enriched.Finitary (Finitary (..), FiniteCat, indices)
import Proarrow.Category.Enriched.Thin
  ( At
  , AtOb (..)
  , Enumerable (..)
  , Finite (..)
  , FmapWrap
  , Index
  , Indexed (..)
  , IndexedList (..)
  , MapWrap
  , Objects
  , finite
  , withWrapAtLookup
  , wrapFinite
  )
import Proarrow.Category.Instance.Bool (BOOL)
import Proarrow.Category.Instance.FinHask (FINHASK (..), arr)
import Proarrow.Category.Instance.FinSet (FINSET (..), FinSet (..))
import Proarrow.Category.Instance.Ordinal (IsOrdinal, ORDINAL)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Is, Kind, Profunctor (..), Promonad (..), UN, dimapDefault, (\\))
import Proarrow.Profunctor.Instance.Cone (Cone (..), Cosink (..))

-- | An internal category in a category @k@.
class ik `InternalIn` k where
  type C0 ik :: k
  type C1 ik :: k
  source :: C1 ik ~> (C0 ik :: k)
  target :: C1 ik ~> (C0 ik :: k)
  identity :: C0 ik ~> (C1 ik :: k)
  compose :: Cosink [C1 ik, C1 ik, C1 ik :: k] -- first arrow projection, second arrow projection, composite

-- | >>> import Data.Fin
-- >>> import Data.Type.Nat
-- >>> import Data.Vec.Lazy
-- >>> import Proarrow.Limit.Pullback
-- >>> import Prelude qualified as P
-- >>> (pullback (source @BOOL @FINSET) (target @BOOL @FINSET) \(FinSet l) (FinSet r) -> 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 ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
 -> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S 'Z) (Fin ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec 'Z (Fin ('S ('S 'Z))) -> Vec ('S 'Z) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S 'Z)))
forall a. Vec 'Z a
VNil
  target :: C1 BOOL ~> C0 BOOL
target = Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
 -> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z))))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
-> FinSet (FS ('S ('S ('S 'Z)))) (FS ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S 'Z))
Fin (Plus 'Z ('S ('S 'Z)))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S 'Z))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
-> Vec ('S ('S ('S 'Z))) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec ('S 'Z) (Fin ('S ('S 'Z)))
-> Vec ('S ('S 'Z)) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S 'Z))
Fin (Plus ('S 'Z) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S 'Z) ('S n))
fin1 Fin ('S ('S 'Z))
-> Vec 'Z (Fin ('S ('S 'Z))) -> Vec ('S 'Z) (Fin ('S ('S 'Z)))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S 'Z)))
forall a. Vec 'Z a
VNil
  identity :: C0 BOOL ~> C1 BOOL
identity = Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z))))
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Vec n (Fin m) -> FinSet (FS n) (FS m)
FinSet (Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
 -> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z)))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
-> FinSet (FS ('S ('S 'Z))) (FS ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Fin ('S ('S ('S 'Z)))
Fin (Plus 'Z ('S ('S ('S 'Z))))
forall (n :: Nat). Fin (Plus 'Z ('S n))
fin0 Fin ('S ('S ('S 'Z)))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
-> Vec ('S ('S 'Z)) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Fin ('S ('S ('S 'Z)))
Fin (Plus ('S ('S 'Z)) ('S 'Z))
forall (n :: Nat). Fin (Plus ('S ('S 'Z)) ('S n))
fin2 Fin ('S ('S ('S 'Z)))
-> Vec 'Z (Fin ('S ('S ('S 'Z))))
-> Vec ('S 'Z) (Fin ('S ('S ('S 'Z))))
forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('S n1) a
::: Vec 'Z (Fin ('S ('S ('S 'Z))))
forall a. Vec 'Z a
VNil

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

-- * Finite categories are the ones internal to @FINHASK@

-- | An object of @k@ as an inhabitant of a finite Haskell type: its index in
-- @'Proarrow.Category.Enriched.Thin.Objects' k@.
type ObIx :: Kind -> Type
newtype ObIx k = ObIx Natural
  deriving newtype (ObIx k -> ObIx k -> Bool
(ObIx k -> ObIx k -> Bool)
-> (ObIx k -> ObIx k -> Bool) -> Eq (ObIx k)
forall k. ObIx k -> ObIx k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall k. ObIx k -> ObIx k -> Bool
== :: ObIx k -> ObIx k -> Bool
$c/= :: forall k. ObIx k -> ObIx k -> Bool
/= :: ObIx k -> ObIx k -> Bool
P.Eq, Eq (ObIx k)
Eq (ObIx k) =>
(ObIx k -> ObIx k -> Ordering)
-> (ObIx k -> ObIx k -> Bool)
-> (ObIx k -> ObIx k -> Bool)
-> (ObIx k -> ObIx k -> Bool)
-> (ObIx k -> ObIx k -> Bool)
-> (ObIx k -> ObIx k -> ObIx k)
-> (ObIx k -> ObIx k -> ObIx k)
-> Ord (ObIx k)
ObIx k -> ObIx k -> Bool
ObIx k -> ObIx k -> Ordering
ObIx k -> ObIx k -> ObIx k
forall k. Eq (ObIx k)
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. ObIx k -> ObIx k -> Bool
forall k. ObIx k -> ObIx k -> Ordering
forall k. ObIx k -> ObIx k -> ObIx k
$ccompare :: forall k. ObIx k -> ObIx k -> Ordering
compare :: ObIx k -> ObIx k -> Ordering
$c< :: forall k. ObIx k -> ObIx k -> Bool
< :: ObIx k -> ObIx k -> Bool
$c<= :: forall k. ObIx k -> ObIx k -> Bool
<= :: ObIx k -> ObIx k -> Bool
$c> :: forall k. ObIx k -> ObIx k -> Bool
> :: ObIx k -> ObIx k -> Bool
$c>= :: forall k. ObIx k -> ObIx k -> Bool
>= :: ObIx k -> ObIx k -> Bool
$cmax :: forall k. ObIx k -> ObIx k -> ObIx k
max :: ObIx k -> ObIx k -> ObIx k
$cmin :: forall k. ObIx k -> ObIx k -> ObIx k
min :: ObIx k -> ObIx k -> ObIx k
P.Ord, Int -> ObIx k -> ShowS
[ObIx k] -> ShowS
ObIx k -> String
(Int -> ObIx k -> ShowS)
-> (ObIx k -> String) -> ([ObIx k] -> ShowS) -> Show (ObIx k)
forall k. Int -> ObIx k -> ShowS
forall k. [ObIx k] -> ShowS
forall k. ObIx k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall k. Int -> ObIx k -> ShowS
showsPrec :: Int -> ObIx k -> ShowS
$cshow :: forall k. ObIx k -> String
show :: ObIx k -> String
$cshowList :: forall k. [ObIx k] -> ShowS
showList :: [ObIx k] -> ShowS
P.Show)

-- | An arrow of @k@ as an inhabitant of a finite Haskell type: the indices of its source and target
-- objects, and its own position in that hom-set.
type ArrIx :: Kind -> Type
data ArrIx k = ArrIx {forall k. ArrIx k -> Natural
arrSrc :: Natural, forall k. ArrIx k -> Natural
arrTgt :: Natural, forall k. ArrIx k -> Natural
arrPos :: Natural}
  deriving (ArrIx k -> ArrIx k -> Bool
(ArrIx k -> ArrIx k -> Bool)
-> (ArrIx k -> ArrIx k -> Bool) -> Eq (ArrIx k)
forall k. ArrIx k -> ArrIx k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall k. ArrIx k -> ArrIx k -> Bool
== :: ArrIx k -> ArrIx k -> Bool
$c/= :: forall k. ArrIx k -> ArrIx k -> Bool
/= :: ArrIx k -> ArrIx k -> Bool
P.Eq, Eq (ArrIx k)
Eq (ArrIx k) =>
(ArrIx k -> ArrIx k -> Ordering)
-> (ArrIx k -> ArrIx k -> Bool)
-> (ArrIx k -> ArrIx k -> Bool)
-> (ArrIx k -> ArrIx k -> Bool)
-> (ArrIx k -> ArrIx k -> Bool)
-> (ArrIx k -> ArrIx k -> ArrIx k)
-> (ArrIx k -> ArrIx k -> ArrIx k)
-> Ord (ArrIx k)
ArrIx k -> ArrIx k -> Bool
ArrIx k -> ArrIx k -> Ordering
ArrIx k -> ArrIx k -> ArrIx k
forall k. Eq (ArrIx k)
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. ArrIx k -> ArrIx k -> Bool
forall k. ArrIx k -> ArrIx k -> Ordering
forall k. ArrIx k -> ArrIx k -> ArrIx k
$ccompare :: forall k. ArrIx k -> ArrIx k -> Ordering
compare :: ArrIx k -> ArrIx k -> Ordering
$c< :: forall k. ArrIx k -> ArrIx k -> Bool
< :: ArrIx k -> ArrIx k -> Bool
$c<= :: forall k. ArrIx k -> ArrIx k -> Bool
<= :: ArrIx k -> ArrIx k -> Bool
$c> :: forall k. ArrIx k -> ArrIx k -> Bool
> :: ArrIx k -> ArrIx k -> Bool
$c>= :: forall k. ArrIx k -> ArrIx k -> Bool
>= :: ArrIx k -> ArrIx k -> Bool
$cmax :: forall k. ArrIx k -> ArrIx k -> ArrIx k
max :: ArrIx k -> ArrIx k -> ArrIx k
$cmin :: forall k. ArrIx k -> ArrIx k -> ArrIx k
min :: ArrIx k -> ArrIx k -> ArrIx k
P.Ord, Int -> ArrIx k -> ShowS
[ArrIx k] -> ShowS
ArrIx k -> String
(Int -> ArrIx k -> ShowS)
-> (ArrIx k -> String) -> ([ArrIx k] -> ShowS) -> Show (ArrIx k)
forall k. Int -> ArrIx k -> ShowS
forall k. [ArrIx k] -> ShowS
forall k. ArrIx k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall k. Int -> ArrIx k -> ShowS
showsPrec :: Int -> ArrIx k -> ShowS
$cshow :: forall k. ArrIx k -> String
show :: ArrIx k -> String
$cshowList :: forall k. [ArrIx k] -> ShowS
showList :: [ArrIx k] -> ShowS
P.Show)

-- | A composable pair, and the apex of 'compose': the pullback of 'source' along 'target'. The
-- arrows are given outer first, so that the legs of 'compose' come out in the order that instance
-- wants them: the first leg composed after the second.
type CompIx :: Kind -> Type
data CompIx k = CompIx (ArrIx k) (ArrIx k)
  deriving (CompIx k -> CompIx k -> Bool
(CompIx k -> CompIx k -> Bool)
-> (CompIx k -> CompIx k -> Bool) -> Eq (CompIx k)
forall k. CompIx k -> CompIx k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall k. CompIx k -> CompIx k -> Bool
== :: CompIx k -> CompIx k -> Bool
$c/= :: forall k. CompIx k -> CompIx k -> Bool
/= :: CompIx k -> CompIx k -> Bool
P.Eq, Eq (CompIx k)
Eq (CompIx k) =>
(CompIx k -> CompIx k -> Ordering)
-> (CompIx k -> CompIx k -> Bool)
-> (CompIx k -> CompIx k -> Bool)
-> (CompIx k -> CompIx k -> Bool)
-> (CompIx k -> CompIx k -> Bool)
-> (CompIx k -> CompIx k -> CompIx k)
-> (CompIx k -> CompIx k -> CompIx k)
-> Ord (CompIx k)
CompIx k -> CompIx k -> Bool
CompIx k -> CompIx k -> Ordering
CompIx k -> CompIx k -> CompIx k
forall k. Eq (CompIx k)
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k. CompIx k -> CompIx k -> Bool
forall k. CompIx k -> CompIx k -> Ordering
forall k. CompIx k -> CompIx k -> CompIx k
$ccompare :: forall k. CompIx k -> CompIx k -> Ordering
compare :: CompIx k -> CompIx k -> Ordering
$c< :: forall k. CompIx k -> CompIx k -> Bool
< :: CompIx k -> CompIx k -> Bool
$c<= :: forall k. CompIx k -> CompIx k -> Bool
<= :: CompIx k -> CompIx k -> Bool
$c> :: forall k. CompIx k -> CompIx k -> Bool
> :: CompIx k -> CompIx k -> Bool
$c>= :: forall k. CompIx k -> CompIx k -> Bool
>= :: CompIx k -> CompIx k -> Bool
$cmax :: forall k. CompIx k -> CompIx k -> CompIx k
max :: CompIx k -> CompIx k -> CompIx k
$cmin :: forall k. CompIx k -> CompIx k -> CompIx k
min :: CompIx k -> CompIx k -> CompIx k
P.Ord, Int -> CompIx k -> ShowS
[CompIx k] -> ShowS
CompIx k -> String
(Int -> CompIx k -> ShowS)
-> (CompIx k -> String) -> ([CompIx k] -> ShowS) -> Show (CompIx k)
forall k. Int -> CompIx k -> ShowS
forall k. [CompIx k] -> ShowS
forall k. CompIx k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall k. Int -> CompIx k -> ShowS
showsPrec :: Int -> CompIx k -> ShowS
$cshow :: forall k. CompIx k -> String
show :: CompIx k -> String
$cshowList :: forall k. [CompIx k] -> ShowS
showList :: [CompIx k] -> ShowS
P.Show)

-- | How many objects @k@ has, by walking its object list.
obCount :: forall k. (Enumerable k) => Natural
obCount :: forall k. Enumerable k => Natural
obCount = IndexedList (Objects k) -> Natural
forall (xs :: [k]). IndexedList xs -> Natural
go (forall k. Finite k => IndexedList (Objects k)
finite @k)
  where
    go :: IndexedList (xs :: [k]) -> Natural
    go :: forall (xs :: [k]). IndexedList xs -> Natural
go IndexedList xs
FNil = Natural
0
    go (FCons IndexedList as1
xs) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.+ IndexedList as1 -> Natural
forall (xs :: [k]). IndexedList xs -> Natural
go IndexedList as1
xs

-- | Recover the object sitting at an index, together with the 'Ob' evidence that lets the
-- 'Finitary' methods be called at it. The index must be below 'obCount'; every index the
-- enumerations below produce is.
withObIx :: forall k r. (Enumerable k) => Natural -> (forall (a :: k). (Ob a) => Proxy a -> r) -> r
withObIx :: forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx Natural
i forall (a :: k). Ob a => Proxy a -> r
f = Nat -> (forall (n :: Nat). SNatI n => Proxy n -> r) -> r
forall r. Nat -> (forall (n :: Nat). SNatI n => Proxy n -> r) -> r
reify (Natural -> Nat
N.fromNatural Natural
i) \(Proxy n
_ :: Proxy n) -> case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @k (forall (n :: Nat). SNatI n => SNat n
snat @n) of
  AtJust @_ @a -> Proxy a -> r
forall (a :: k). Ob a => Proxy a -> r
f (forall (t :: k). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
  AtOb k (At k n)
AtNothing -> String -> r
forall a. HasCallStack => String -> a
P.error String
"withObIx: no object at this index"

-- | The size of a hom-set, named by the indices of its endpoints.
homSize :: forall k. (FiniteCat k) => Natural -> Natural -> Natural
homSize :: forall k. FiniteCat k => Natural -> Natural -> Natural
homSize Natural
i Natural
j =
  forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
i \(Proxy a
_ :: Proxy a) ->
    forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
j \(Proxy a
_ :: Proxy b) ->
      forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
Natural
size @(Hom k) @a @b

instance (Enumerable k) => U.Universe (ObIx k) where
  universe :: [ObIx k]
universe = Natural -> ObIx k
forall k. Natural -> ObIx k
ObIx (Natural -> ObIx k) -> [Natural] -> [ObIx k]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.<$> Natural -> [Natural]
indices (forall k. Enumerable k => Natural
obCount @k)
instance (Enumerable k) => U.Finite (ObIx k)

instance (FiniteCat k) => U.Universe (ArrIx k) where
  universe :: [ArrIx k]
universe =
    [ Natural -> Natural -> Natural -> ArrIx k
forall k. Natural -> Natural -> Natural -> ArrIx k
ArrIx Natural
i Natural
j Natural
h
    | Natural
i <- Natural -> [Natural]
indices (forall k. Enumerable k => Natural
obCount @k)
    , Natural
j <- Natural -> [Natural]
indices (forall k. Enumerable k => Natural
obCount @k)
    , Natural
h <- Natural -> [Natural]
indices (forall k. FiniteCat k => Natural -> Natural -> Natural
homSize @k Natural
i Natural
j)
    ]
instance (FiniteCat k) => U.Finite (ArrIx k)

instance (FiniteCat k) => U.Universe (CompIx k) where
  universe :: [CompIx k]
universe = [ArrIx k -> ArrIx k -> CompIx k
forall k. ArrIx k -> ArrIx k -> CompIx k
CompIx ArrIx k
g ArrIx k
f | ArrIx k
g <- [ArrIx k]
forall a. Finite a => [a]
U.universeF, ArrIx k
f <- [ArrIx k]
forall a. Finite a => [a]
U.universeF, ArrIx k -> Natural
forall k. ArrIx k -> Natural
arrSrc ArrIx k
g Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== ArrIx k -> Natural
forall k. ArrIx k -> Natural
arrTgt ArrIx k
f]
instance (FiniteCat k) => U.Finite (CompIx k)

-- | Every finite category is a category internal to 'FINHASK': objects and arrows are carried by
-- their indices, and the structure maps are the lookup tables that read those indices back.
--
-- At 'BOOL' every table agrees with the hand-written @FINSET@ presentation above, with the arrows
-- coming out in the order @Fls@, @F2T@, @Tru@.
--
-- >>> import Data.List (elemIndex)
-- >>> import Proarrow.Category.Instance.FinHask (toList)
-- >>> let ix a = P.maybe (-1) P.id (elemIndex a (U.universeF :: [ArrIx BOOL])) :: P.Int
-- >>> P.map P.snd (toList (source @BOOL @FINHASK))
-- [0,0,1]
-- >>> P.map P.snd (toList (target @BOOL @FINHASK))
-- [0,1,1]
-- >>> P.map (ix P.. P.snd) (toList (identity @BOOL @FINHASK))
-- [0,2]
-- >>> :{
-- (case compose @BOOL @FINHASK of
--    Cone (Leg l1 (Leg l2 (Leg l3 Apex))) ->
--      let g l = P.map (ix P.. P.snd) (toList l) in (g l1, g l2, g l3))
--   :: ([P.Int], [P.Int], [P.Int])
-- :}
-- ([0,1,2,2],[0,0,1,2],[0,1,1,2])
instance (FiniteCat k) => k `InternalIn` FINHASK where
  type C0 k = FH (ObIx k)
  type C1 k = FH (ArrIx k)
  source :: C1 k ~> C0 k
source = (ArrIx k -> ObIx k) -> FinHask (FH (ArrIx k)) (FH (ObIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(ArrIx Natural
i Natural
_ Natural
_) -> Natural -> ObIx k
forall k. Natural -> ObIx k
ObIx Natural
i
  target :: C1 k ~> C0 k
target = (ArrIx k -> ObIx k) -> FinHask (FH (ArrIx k)) (FH (ObIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(ArrIx Natural
_ Natural
j Natural
_) -> Natural -> ObIx k
forall k. Natural -> ObIx k
ObIx Natural
j
  identity :: C0 k ~> C1 k
identity = (ObIx k -> ArrIx k) -> FinHask (FH (ObIx k)) (FH (ArrIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(ObIx Natural
i) -> forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
i \(Proxy a
_ :: Proxy a) -> Natural -> Natural -> Natural -> ArrIx k
forall k. Natural -> Natural -> Natural -> ArrIx k
ArrIx Natural
i Natural
i (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @(Hom k) @a @a Hom k a a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
  compose :: Cosink '[C1 k, C1 k, C1 k]
compose =
    Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k])
-> Cosink '[C1 k, C1 k, C1 k]
forall {k} (a :: k) (as :: [k]). Cone (PR a) (L as) -> Cosink as
Cone (Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k])
 -> Cosink '[C1 k, C1 k, C1 k])
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k])
-> Cosink '[C1 k, C1 k, C1 k]
forall a b. (a -> b) -> a -> b
$
      (FH (CompIx k) ~> C1 k)
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k])
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone (PR a1) (L bs1) -> Cone (PR a1) (L (b : bs1))
Leg ((CompIx k -> ArrIx k) -> FinHask (FH (CompIx k)) (FH (ArrIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(CompIx ArrIx k
f ArrIx k
_) -> ArrIx k
f) (Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k])
 -> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k]))
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k])
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k, C1 k])
forall a b. (a -> b) -> a -> b
$
        (FH (CompIx k) ~> C1 k)
-> Cone (PR (FH (CompIx k))) (L '[C1 k])
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone (PR a1) (L bs1) -> Cone (PR a1) (L (b : bs1))
Leg ((CompIx k -> ArrIx k) -> FinHask (FH (CompIx k)) (FH (ArrIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr \(CompIx ArrIx k
_ ArrIx k
g) -> ArrIx k
g) (Cone (PR (FH (CompIx k))) (L '[C1 k])
 -> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k]))
-> Cone (PR (FH (CompIx k))) (L '[C1 k])
-> Cone (PR (FH (CompIx k))) (L '[C1 k, C1 k])
forall a b. (a -> b) -> a -> b
$
          (FH (CompIx k) ~> C1 k)
-> Cone (PR (FH (CompIx k))) (L '[])
-> Cone (PR (FH (CompIx k))) (L '[C1 k])
forall {k} (a1 :: k) (b :: k) (bs1 :: [k]).
(a1 ~> b) -> Cone (PR a1) (L bs1) -> Cone (PR a1) (L (b : bs1))
Leg ((CompIx k -> ArrIx k) -> FinHask (FH (CompIx k)) (FH (ArrIx k))
forall a b.
(Ob (FH a), Ob (FH b)) =>
(a -> b) -> FinHask (FH a) (FH b)
arr CompIx k -> ArrIx k
composite) Cone (PR (FH (CompIx k))) (L '[])
forall {k} (a1 :: k). Ob a1 => Cone (PR a1) (L '[])
Apex
    where
      composite :: CompIx k -> ArrIx k
composite (CompIx (ArrIx Natural
j Natural
l Natural
g) (ArrIx Natural
i Natural
_ Natural
f)) =
        forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
i \(Proxy a
_ :: Proxy a) ->
          forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
j \(Proxy a
_ :: Proxy b) ->
            forall k r.
Enumerable k =>
Natural -> (forall (a :: k). Ob a => Proxy a -> r) -> r
withObIx @k Natural
l \(Proxy a
_ :: Proxy c) ->
              Natural -> Natural -> Natural -> ArrIx k
forall k. Natural -> Natural -> Natural -> ArrIx k
ArrIx Natural
i Natural
l (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @(Hom k) @a @c (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @(Hom k) @b @c Natural
g (a ~> a) -> (a ~> a) -> Hom k a a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @(Hom k) @a @b Natural
f))

-- * The converse: an internal category in @FINSET@ is a finite category

-- | How many objects and how many arrows an internal category in @FINSET@ has. These are types.
-- That is what @FINSET@ has over 'Proarrow.Category.Instance.FinHask.FINHASK', and the converse
-- needs it, because 'Enumerable' asks for its object list at the type level.
type NumObs ik = UN FS (C0 ik :: FINSET)

type NumArrs ik = UN FS (C1 ik :: FINSET)

-- | The category an internal category in @FINSET@ presents, as a kind: its objects are the elements
-- of @'C0' ik@, numbered by 'ORDINAL'.
type data INTERNAL ik = IN (ORDINAL (NumObs ik))

-- | An arrow of the presented category: an element of @'C1' ik@. That its 'source' and 'target' are
-- the objects claimed is a runtime invariant, as the table invariants of 'FinSet' are.
type Internal :: forall {ik}. CAT (INTERNAL ik)
data Internal a b where
  Internal :: (Ob a, Ob b) => Natural -> Internal (a :: INTERNAL ik) b

-- | A structure map as a list of indices into its codomain.
tableOf :: FinSet a b -> [Natural]
tableOf :: forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf (FinSet Vec n (Fin m)
v) = (Fin m -> Natural) -> [Fin m] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
P.map Fin m -> Natural
forall (n :: Nat). Fin n -> Natural
toNatural (Vec n (Fin m) -> [Fin m]
forall (n :: Nat) a. Vec n a -> [a]
Vec.toList Vec n (Fin m)
v)

-- | The composition table: for each composable pair, the outer arrow, the inner arrow, and their
-- composite, as indices into @'C1' ik@.
compTable :: forall ik. (ik `InternalIn` FINSET) => [(Natural, Natural, Natural)]
compTable :: forall {k} (ik :: k).
InternalIn ik FINSET =>
[(Natural, Natural, Natural)]
compTable = case forall (ik :: k) k.
InternalIn ik k =>
Cosink '[C1 ik, C1 ik, C1 ik]
forall {k} (ik :: k) k.
InternalIn ik k =>
Cosink '[C1 ik, C1 ik, C1 ik]
compose @ik @FINSET of
  Cone (Leg a1 ~> b
l1 (Leg a1 ~> b
l2 (Leg a1 ~> b
l3 Cone (PR a1) (L bs1)
Apex))) -> [Natural]
-> [Natural] -> [Natural] -> [(Natural, Natural, Natural)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
P.zip3 (FinSet (FS (UN FS a)) b -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf a1 ~> b
FinSet (FS (UN FS a)) b
l1) (FinSet (FS (UN FS a)) b -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf a1 ~> b
FinSet (FS (UN FS a)) b
l2) (FinSet (FS (UN FS a)) b -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf a1 ~> b
FinSet (FS (UN FS a)) b
l3)

-- | Which element of @'C0' ik@ an object names.
obNum :: forall {ik} (a :: INTERNAL ik). (Enumerable (INTERNAL ik), Ob a) => Natural
obNum :: forall {k} {ik :: k} (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
obNum = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @(INTERNAL ik) @a (Proxy (OrdIndex (UN IN a)) -> Natural
forall (n :: Nat) m (proxy :: Nat -> Type).
(SNatI n, Num m) =>
proxy n -> m
N.reflectToNum (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @(Index a)))

instance (ik `InternalIn` FINSET) => Indexed (INTERNAL ik) where
  type Index (a :: INTERNAL ik) = Index (UN IN a)
  type At (INTERNAL ik) i = FmapWrap IN (At (ORDINAL (NumObs ik)) i)

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => Finite (INTERNAL ik) where
  type Objects (INTERNAL ik) = MapWrap IN (Objects (ORDINAL (NumObs ik)))
  finite :: IndexedList (Objects (INTERNAL ik))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: ORDINAL (NumObs ik) -> INTERNAL ik).
(Finite (ORDINAL (NumObs ik)),
 forall (a :: ORDINAL (NumObs ik)).
 KnownIndex a =>
 KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects (ORDINAL (NumObs ik))))
wrapFinite @IN
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (INTERNAL ik)) i ~ At (INTERNAL ik) i) => r)
-> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: ORDINAL (NumObs ik) -> INTERNAL ik) (i :: Nat) r.
Finite (ORDINAL (NumObs ik)) =>
SNat i
-> ((Lookup (MapWrap w (Objects (ORDINAL (NumObs ik)))) i
     ~ FmapWrap w (At (ORDINAL (NumObs ik)) i)) =>
    r)
-> r
withWrapAtLookup @IN

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => Enumerable (INTERNAL ik) where
  withIndex :: forall (a :: INTERNAL ik) r. Ob a => (KnownIndex a => r) -> r
withIndex @a KnownIndex a => r
r = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @(ORDINAL (NumObs ik)) @(UN IN a) r
KnownIndex (UN IN a) => r
KnownIndex a => r
r
  atOb :: forall (i :: Nat).
SNat i -> AtOb (INTERNAL ik) (At (INTERNAL ik) i)
atOb SNat i
i = case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
atOb @(ORDINAL (NumObs ik)) SNat i
i of
    AtOb (ORDINAL (NumObs ik)) (At (ORDINAL (NumObs ik)) i)
AtJust -> AtOb (INTERNAL ik) ('Just (IN a))
AtOb (INTERNAL ik) (At (INTERNAL ik) i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
AtJust
    AtOb (ORDINAL (NumObs ik)) (At (ORDINAL (NumObs ik)) i)
AtNothing -> AtOb (INTERNAL ik) 'Nothing
AtOb (INTERNAL ik) (At (INTERNAL ik) i)
forall k. AtOb k 'Nothing
AtNothing

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => Profunctor (Internal :: CAT (INTERNAL ik)) where
  dimap :: forall (c :: INTERNAL ik) (a :: INTERNAL ik) (b :: INTERNAL ik)
       (d :: INTERNAL ik).
(c ~> a) -> (b ~> d) -> Internal a b -> Internal c d
dimap = (c ~> a) -> (b ~> d) -> Internal a b -> Internal c d
Internal c a -> Internal b d -> Internal a b -> Internal 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 :: INTERNAL ik) (b :: INTERNAL ik) r.
((Ob a, Ob b) => r) -> Internal a b -> r
\\ Internal{} = r
(Ob a, Ob b) => r
r

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => Promonad (Internal :: CAT (INTERNAL ik)) where
  id :: forall (a :: INTERNAL ik). Ob a => Internal a a
id @a = Natural -> Internal a a
forall {k} (ik :: k) (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Natural -> Internal a b
Internal ([Natural] -> Natural -> Natural
forall i a. Integral i => [a] -> i -> a
genericIndex (FinSet (C0 ik) (C1 ik) -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf (forall (ik :: k) k. InternalIn ik k => C0 ik ~> C1 ik
forall {k} (ik :: k) k. InternalIn ik k => C0 ik ~> C1 ik
identity @ik @FINSET)) (forall {k} {ik :: k} (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
forall (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
obNum @a))
  Internal Natural
g . :: forall (b :: INTERNAL ik) (c :: INTERNAL ik) (a :: INTERNAL ik).
Internal b c -> Internal a b -> Internal a c
. Internal Natural
f = case [Natural
c | (Natural
o, Natural
i, Natural
c) <- forall (ik :: k).
InternalIn ik FINSET =>
[(Natural, Natural, Natural)]
forall {k} (ik :: k).
InternalIn ik FINSET =>
[(Natural, Natural, Natural)]
compTable @ik, Natural
o Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
g, Natural
i Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== Natural
f] of
    Natural
c : [Natural]
_ -> Natural -> Internal a c
forall {k} (ik :: k) (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Natural -> Internal a b
Internal Natural
c
    [] -> String -> Internal a c
forall a. HasCallStack => String -> a
P.error String
"Internal.(.): the arrows do not compose"

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => CategoryOf (INTERNAL ik) where
  type (~>) = Internal
  type Ob a = (Is IN a, IsOrdinal (UN IN a))

instance (ik `InternalIn` FINSET, SNatI (NumObs ik)) => Finitary (Internal :: CAT (INTERNAL ik)) where
  elements :: forall (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
[Internal a b]
elements @a @b =
    [ Natural -> Internal a b
forall {k} (ik :: k) (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Natural -> Internal a b
Internal Natural
e
    | (Natural
e, Natural
s, Natural
t) <- [Natural]
-> [Natural] -> [Natural] -> [(Natural, Natural, Natural)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
P.zip3 [Natural
Item [Natural]
0 ..] (FinSet (C1 ik) (C0 ik) -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf (forall (ik :: k) k. InternalIn ik k => C1 ik ~> C0 ik
forall {k} (ik :: k) k. InternalIn ik k => C1 ik ~> C0 ik
source @ik @FINSET)) (FinSet (C1 ik) (C0 ik) -> [Natural]
forall (a :: FINSET) (b :: FINSET). FinSet a b -> [Natural]
tableOf (forall (ik :: k) k. InternalIn ik k => C1 ik ~> C0 ik
forall {k} (ik :: k) k. InternalIn ik k => C1 ik ~> C0 ik
target @ik @FINSET))
    , Natural
s Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== forall {k} {ik :: k} (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
forall (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
obNum @a
    , Natural
t Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== forall {k} {ik :: k} (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
forall (a :: INTERNAL ik).
(Enumerable (INTERNAL ik), Ob a) =>
Natural
obNum @b
    ]
  size :: forall (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Natural
size @a @b = [Internal a b] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: INTERNAL ik +-> INTERNAL ik) (a :: INTERNAL ik)
       (b :: INTERNAL ik).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Internal :: CAT (INTERNAL ik)) @a @b)
  toIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Internal a b -> Natural
toIndex @a @b (Internal Natural
e) =
    case Natural -> [Natural] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Natural
e [Natural
n | Internal Natural
n <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: INTERNAL ik +-> INTERNAL ik) (a :: INTERNAL ik)
       (b :: INTERNAL ik).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Internal :: CAT (INTERNAL ik)) @a @b] of
      P.Just Int
i -> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral Int
i
      Maybe Int
P.Nothing -> String -> Natural
forall a. HasCallStack => String -> a
P.error String
"Internal.toIndex: not an arrow of this hom-set"
  fromIndex :: forall (a :: INTERNAL ik) (b :: INTERNAL ik).
(Ob a, Ob b) =>
Natural -> Internal a b
fromIndex @a @b Natural
i = [Internal a b] -> Natural -> Internal a b
forall i a. Integral i => [a] -> i -> a
genericIndex (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: INTERNAL ik +-> INTERNAL ik) (a :: INTERNAL ik)
       (b :: INTERNAL ik).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Internal :: CAT (INTERNAL ik)) @a @b) Natural
i

-- | The converse, as a statement: an internal category in @FINSET@ presents a 'FiniteCat'.
--
-- At 'BOOL' the presented category has the hom-sets of 'BOOL' back: one arrow each way except from
-- @TRU@ to @FLS@, where there is none.
--
-- >>> import Proarrow.Category.Instance.Ordinal (ORDINAL (..))
-- >>> :{
-- [ size @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN OZ)
-- , size @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ))
-- , size @(Hom (INTERNAL BOOL)) @(IN (OS OZ)) @(IN OZ)
-- , size @(Hom (INTERNAL BOOL)) @(IN (OS OZ)) @(IN (OS OZ))
-- ] :: [Natural]
-- :}
-- [1,1,0,1]
--
-- >>> let f = fromIndex @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ)) 0
-- >>> toIndex @(Hom (INTERNAL BOOL)) @(IN OZ) @(IN (OS OZ)) (id @_ @(IN (OS OZ)) . f)
-- 0
internalIsFinite
  :: forall ik r. (ik `InternalIn` FINSET, SNatI (NumObs ik)) => ((FiniteCat (INTERNAL ik)) => r) -> r
internalIsFinite :: forall {k} (ik :: k) r.
(InternalIn ik FINSET, SNatI (NumObs ik)) =>
(FiniteCat (INTERNAL ik) => r) -> r
internalIsFinite FiniteCat (INTERNAL ik) => r
r = r
FiniteCat (INTERNAL ik) => r
r