{-# LANGUAGE AllowAmbiguousTypes #-}
-- Orphans throughout, and unavoidably: every instance here is on either 'SUBCAT' 'Finitary' (the
-- kind synonym 'FINITARY' expands to it, and both halves of that come from other modules) or on a
-- profunctor defined elsewhere. Both the class and the category it carves out have to sit below the
-- enrichment machinery; everything computed in that category needs things sitting above it.
{-# OPTIONS_GHC -Wno-orphans #-}

-- | __The topos of finitary profunctors.__ Everything built on the numbering in
-- "Proarrow.Category.Enriched.Finitary": a hom-set is an initial segment of the naturals, so a
-- subobject or a quotient of one is a table of indices, and a computation can produce such a table
-- and reify it into a fresh object. That is 'Reindex', and it gives equalizers, coequalizers,
-- pullbacks, pushouts and epi-mono factorization.
--
-- The internal hom and the subobject classifier are the same construction one level up: both are
-- ends, enumerated by choosing a value at every point of a domain and keeping the choices that
-- commute with the action. Neither count is a formula in the sizes it is built from -- they depend
-- on how the arrows of @j@ and @k@ compose -- which is exactly why the numbering is a value.
--
-- The punchline is @'ElementaryTopos' ('PROD' ('FINITARY' j k))@ at the end. 'PROD' is what makes
-- the tensor the product rather than Day convolution, as it does for @j '+->' k@ itself.
module Proarrow.Category.Enriched.Finitary.Topos where

import Data.IntMap.Strict qualified as IM
import Data.Kind (Constraint)
import Data.List (elemIndex, findIndex, genericIndex, genericLength, genericReplicate, partition, sort)
import Data.Map.Strict qualified as M
import Data.Proxy (Proxy (..))
import Data.Type.Equality ((:~:) (..))
import Data.Type.Nat (Nat (..), SNatI, reify, snat)
import Data.Type.Nat qualified as N
import Numeric.Natural (Natural)
import Prelude (Maybe (..), ($), (==), (||))
import Prelude qualified as P

import Proarrow.Category.Enriched.Finitary
import Proarrow.Category.Enriched.Thin
  ( Entry
  , Enumerable (..)
  , Finite (..)
  , Indexed (..)
  , IndexedList (..)
  , KnownList (..)
  )
import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Topos
  ( ElementaryTopos
  , HasEpiMonoFactorization (..)
  , HasSubobjectClassifier (..)
  )
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts)
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Hom
  , Profunctor (..)
  , Promonad (..)
  , UN
  , lmap
  , rmap
  , (//)
  , type (+->)
  , type (:~>)
  )
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), PROD (..), Prod (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks)
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Instance.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Instance.Exponential ((:~>:) (..))
import Proarrow.Profunctor.Instance.Initial (InitialProfunctor)
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Instance.Sieve (Sieve (..), maximalSieve)
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Instance.Yoneda (Yo (..))

-- | The subcategory of finitary profunctors, as "Proarrow.Category.Instance.Rep" does for
-- representable ones.
type FINITARY j k = SUBCAT (Finitary :: (j +-> k) -> Constraint)

type FIN (p :: j +-> k) = SUB p :: FINITARY j k

instance (CategoryOf j, CategoryOf k) => HasTerminalObject (FINITARY j k) where
  type TerminalObject = FIN TerminalProfunctor
  terminate :: forall (a :: FINITARY j k). Ob a => a ~> TerminalObject
terminate = Prof (UN SUB a) TerminalProfunctor
-> Sub Prof (SUB (UN SUB a)) (FIN TerminalProfunctor)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub UN SUB a ~> TerminalObject
Prof (UN SUB a) TerminalProfunctor
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
forall (a :: k -> j -> Type). Ob a => a ~> TerminalObject
terminate

instance (CategoryOf j, CategoryOf k) => HasBinaryProducts (FINITARY j k) where
  type a && b = SUB (UN SUB a :*: UN SUB b)
  withObProd :: forall (a :: FINITARY j k) (b :: FINITARY j k) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd Ob (a && b) => r
r = r
Ob (a && b) => r
r
  fst :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(SUB p) @(SUB q) = Prof (UN SUB a :*: UN SUB b) (UN SUB a)
-> Sub Prof (SUB (UN SUB a :*: UN SUB b)) (SUB (UN SUB a))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @(j +-> k) @p @q)
  snd :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(SUB p) @(SUB q) = Prof (UN SUB a :*: UN SUB b) (UN SUB b)
-> Sub Prof (SUB (UN SUB a :*: UN SUB b)) (SUB (UN SUB b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @(j +-> k) @p @q)
  Sub Prof a1 b1
l &&& :: forall (a :: FINITARY j k) (x :: FINITARY j k) (y :: FINITARY j k).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Sub Prof a1 b1
r = Prof a1 (b1 :*: b1) -> Sub Prof (SUB a1) (SUB (b1 :*: b1))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (a1 ~> b1
Prof a1 b1
l (a1 ~> b1) -> (a1 ~> b1) -> a1 ~> (b1 && b1)
forall k (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
(a ~> x) -> (a ~> y) -> a ~> (x && y)
forall (a :: k -> j -> Type) (x :: k -> j -> Type)
       (y :: k -> j -> Type).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& a1 ~> b1
Prof a1 b1
r)

instance (CategoryOf j, CategoryOf k) => HasInitialObject (FINITARY j k) where
  type InitialObject = FIN InitialProfunctor
  initiate :: forall (a :: FINITARY j k). Ob a => InitialObject ~> a
initiate = Prof InitialProfunctor (UN SUB a)
-> Sub Prof (FIN InitialProfunctor) (SUB (UN SUB a))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub InitialObject ~> UN SUB a
Prof InitialProfunctor (UN SUB a)
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
forall (a :: k -> j -> Type). Ob a => InitialObject ~> a
initiate

instance (CategoryOf j, CategoryOf k) => HasBinaryCoproducts (FINITARY j k) where
  type a || b = SUB (UN SUB a :+: UN SUB b)
  withObCoprod :: forall (a :: FINITARY j k) (b :: FINITARY j k) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod Ob (a || b) => r
r = r
Ob (a || b) => r
r
  lft :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(SUB p) @(SUB q) = Prof (UN SUB a) (UN SUB a :+: UN SUB b)
-> Sub Prof (SUB (UN SUB a)) (SUB (UN SUB a :+: UN SUB b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @(j +-> k) @p @q)
  rgt :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(SUB p) @(SUB q) = Prof (UN SUB b) (UN SUB a :+: UN SUB b)
-> Sub Prof (SUB (UN SUB b)) (SUB (UN SUB a :+: UN SUB b))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @(j +-> k) @p @q)
  Sub Prof a1 b1
l ||| :: forall (x :: FINITARY j k) (a :: FINITARY j k) (y :: FINITARY j k).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Sub Prof a1 b1
r = Prof (a1 :+: a1) b1 -> Sub Prof (SUB (a1 :+: a1)) (SUB b1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (a1 ~> b1
Prof a1 b1
l (a1 ~> b1) -> (a1 ~> b1) -> (a1 || a1) ~> b1
forall k (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
(x ~> a) -> (y ~> a) -> (x || y) ~> a
forall (x :: k -> j -> Type) (a :: k -> j -> Type)
       (y :: k -> j -> Type).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| a1 ~> b1
Prof a1 b1
r)

-- * Tables of fibres

-- | A type-level list of naturals, reflected.
class KnownNats (ns :: [Nat]) where
  natsVal :: [Natural]

instance KnownNats '[] where
  natsVal :: [Natural]
natsVal = []

instance (SNatI n, KnownNats ns) => KnownNats (n ': ns) where
  natsVal :: [Natural]
natsVal = SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
N.snatToNatural (forall (n :: Nat). SNatI n => SNat n
snat @n) Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: forall (ns :: [Nat]). KnownNats ns => [Natural]
natsVal @ns

-- | A type-level list of lists of naturals, reflected: the fibres of a partial surjection out of
-- one hom-set.
class KnownFibres (fs :: [[Nat]]) where
  fibresVal :: [[Natural]]

instance KnownFibres '[] where
  fibresVal :: [[Natural]]
fibresVal = []

instance (KnownNats f, KnownFibres fs) => KnownFibres (f ': fs) where
  fibresVal :: [[Natural]]
fibresVal = forall (ns :: [Nat]). KnownNats ns => [Natural]
natsVal @f [Natural] -> [[Natural]] -> [[Natural]]
forall a. a -> [a] -> [a]
: forall (fs :: [[Nat]]). KnownFibres fs => [[Natural]]
fibresVal @fs

-- | Reify a list of lists of naturals.
fibres :: forall r. [[Natural]] -> (forall fs. (KnownFibres fs) => r) -> r
fibres :: forall r.
[[Natural]] -> (forall (fs :: [[Nat]]). KnownFibres fs => r) -> r
fibres [] forall (fs :: [[Nat]]). KnownFibres fs => r
k = forall (fs :: [[Nat]]). KnownFibres fs => r
k @'[]
fibres ([Natural]
f : [[Natural]]
fs) forall (fs :: [[Nat]]). KnownFibres fs => r
k = [Natural] -> (forall (ns :: [Nat]). KnownNats ns => r) -> r
forall r'.
[Natural] -> (forall (ns :: [Nat]). KnownNats ns => r') -> r'
nats [Natural]
f \ @f' -> [[Natural]] -> (forall (fs :: [[Nat]]). KnownFibres fs => r) -> r
forall r.
[[Natural]] -> (forall (fs :: [[Nat]]). KnownFibres fs => r) -> r
fibres [[Natural]]
fs \ @fs' -> forall (fs :: [[Nat]]). KnownFibres fs => r
k @(f' ': fs')
  where
    nats :: forall r'. [Natural] -> (forall ns. (KnownNats ns) => r') -> r'
    nats :: forall r'.
[Natural] -> (forall (ns :: [Nat]). KnownNats ns => r') -> r'
nats [] forall (ns :: [Nat]). KnownNats ns => r'
k' = forall (ns :: [Nat]). KnownNats ns => r'
k' @'[]
    nats (Natural
n : [Natural]
ns) forall (ns :: [Nat]). KnownNats ns => r'
k' = 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
n) \(Proxy n
_ :: Proxy n) -> [Natural] -> (forall (ns :: [Nat]). KnownNats ns => r') -> r'
forall r'.
[Natural] -> (forall (ns :: [Nat]). KnownNats ns => r') -> r'
nats [Natural]
ns \ @ns' -> forall (ns :: [Nat]). KnownNats ns => r'
k' @(n ': ns')

-- | A table: a row for each object of @k@, and in each row the fibres at each object of @j@.
type KnownTable bs as t = KnownList (KnownList KnownFibres bs) as t

-- | Build a table by visiting every pair of objects, reifying each cell.
buildTable
  :: forall j k r
   . (Enumerable j, Enumerable k)
  => (forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]])
  -> (forall (t :: [[[[Nat]]]]). (KnownTable (Objects j) (Objects k) t) => r)
  -> r
buildTable :: forall j k r.
(Enumerable j, Enumerable k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]])
-> (forall (t :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) t =>
    r)
-> r
buildTable forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]]
cell = IndexedList (Objects k)
-> (forall (t :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) t =>
    r)
-> r
forall (as :: [k]) r'.
IndexedList as
-> (forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r')
-> r'
rows (forall k. Finite k => IndexedList (Objects k)
finite @k)
  where
    rows :: forall (as :: [k]) r'. IndexedList as -> (forall t. (KnownTable (Objects j) as t) => r') -> r'
    rows :: forall (as :: [k]) r'.
IndexedList as
-> (forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r')
-> r'
rows IndexedList as
FNil forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r'
k' = forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r'
k' @'[]
    rows (FCons @a IndexedList as1
as) forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r'
k' = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @k @a (forall (a :: k) (bs :: [j]) r'.
Ob a =>
IndexedList bs
-> (forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r')
-> r'
row @a (forall k. Finite k => IndexedList (Objects k)
finite @j) \ @r0 -> IndexedList as1
-> (forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as1 t => r')
-> r'
forall (as :: [k]) r'.
IndexedList as
-> (forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r')
-> r'
rows IndexedList as1
as \ @t -> forall (t :: [[[[Nat]]]]). KnownTable (Objects j) as t => r'
k' @(r0 ': t))
    row
      :: forall (a :: k) (bs :: [j]) r'. (Ob a) => IndexedList bs -> (forall r0. (KnownList KnownFibres bs r0) => r') -> r'
    row :: forall (a :: k) (bs :: [j]) r'.
Ob a =>
IndexedList bs
-> (forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r')
-> r'
row IndexedList bs
FNil forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r'
k' = forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r'
k' @'[]
    row (FCons @b IndexedList as1
bs) forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r'
k' = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @j @b ([[Natural]] -> (forall (fs :: [[Nat]]). KnownFibres fs => r') -> r'
forall r.
[[Natural]] -> (forall (fs :: [[Nat]]). KnownFibres fs => r) -> r
fibres (forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]]
cell @a @b) \ @fs -> forall (a :: k) (bs :: [j]) r'.
Ob a =>
IndexedList bs
-> (forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r')
-> r'
row @a IndexedList as1
bs \ @r0 -> forall (r0 :: [[[Nat]]]). KnownList KnownFibres bs r0 => r'
k' @(fs ': r0))

-- * Reindexing along a table of fibres

-- | @p@ relabelled, at each pair of objects, along a partial surjection onto an initial segment of
-- the naturals, given by its fibres: index @i@ of the new hom-set stands for the elements of @p@ in
-- the @i@-th fibre. Singleton fibres cut out a subobject, a partition is a quotient. Well behaved
-- exactly when the fibres are respected by @p@'s 'dimap', which is the case for the tables
-- 'equalize' and 'coequalize' build; 'dimap' delegates to @p@ and relies on it.
newtype Reindex (p :: j +-> k) (fs :: [[[[Nat]]]]) (a :: k) (b :: j) = Reindex (p a b)

type Cell fs (a :: k) (b :: j) = Entry (Entry fs (Index a)) (Index b)

instance (Profunctor p) => Profunctor (Reindex p fs) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Reindex p fs a b -> Reindex p fs c d
dimap c ~> a
l b ~> d
r (Reindex p a b
x) = p c d -> Reindex p fs c d
forall j k (p :: j +-> k) (fs :: [[[[Nat]]]]) (a :: k) (b :: j).
p a b -> Reindex p fs a b
Reindex ((c ~> a) -> (b ~> d) -> p a b -> p c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
l b ~> d
r p a b
x)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Reindex p fs a b -> r
\\ Reindex p a b
x = r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
x

-- | The fibres at a pair of objects, found by walking the table to the objects' positions.
withCell
  :: forall {j} {k} fs (a :: k) (b :: j) r
   . (Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs, Ob a, Ob b)
  => ((KnownFibres (Cell fs a b)) => r) -> r
withCell :: forall {j} {k} (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
withCell KnownFibres (Cell fs a b) => r
r =
  forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @a ((KnownIndex a => r) -> r) -> (KnownIndex a => r) -> r
forall a b. (a -> b) -> a -> b
$
    forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @j @b ((KnownIndex b => r) -> r) -> (KnownIndex b => r) -> r
forall a b. (a -> b) -> a -> b
$
      forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @k (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)) (((Lookup (Objects k) (Index a) ~ At k (Index a)) => r) -> r)
-> ((Lookup (Objects k) (Index a) ~ At k (Index a)) => r) -> r
forall a b. (a -> b) -> a -> b
$
        forall k (i :: Nat) r.
Finite k =>
SNat i -> ((Lookup (Objects k) i ~ At k i) => r) -> r
withAtLookup @j (forall (n :: Nat). SNatI n => SNat n
snat @(Index b)) (((Lookup (Objects j) (Index b) ~ At j (Index b)) => r) -> r)
-> ((Lookup (Objects j) (Index b) ~ At j (Index b)) => r) -> r
forall a b. (a -> b) -> a -> b
$
          forall {x} {y} (c :: x -> Constraint) (shape :: [y]) (xs :: [x])
       (s :: y) (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
forall (c :: [[[Nat]]] -> Constraint) (shape :: [k])
       (xs :: [[[[Nat]]]]) (s :: k) (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
withEntry @(KnownList KnownFibres (Objects j)) @(Objects k) @fs (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)) 'Just a :~: 'Just a
Lookup (Objects k) (Index a) :~: 'Just a
forall {k} (a :: k). a :~: a
Refl ((KnownList KnownFibres (Objects j) (Entry fs (Index a)) => r)
 -> r)
-> (KnownList KnownFibres (Objects j) (Entry fs (Index a)) => r)
-> r
forall a b. (a -> b) -> a -> b
$
            forall {x} {y} (c :: x -> Constraint) (shape :: [y]) (xs :: [x])
       (s :: y) (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
forall (c :: [[Nat]] -> Constraint) (shape :: [j])
       (xs :: [[[Nat]]]) (s :: j) (i :: Nat) r.
KnownList c shape xs =>
SNat i
-> (Lookup shape i :~: 'Just s) -> (c (Entry xs i) => r) -> r
withEntry @KnownFibres @(Objects j) @(Entry fs (Index a)) (forall (n :: Nat). SNatI n => SNat n
snat @(Index b)) 'Just b :~: 'Just b
Lookup (Objects j) (Index b) :~: 'Just b
forall {k} (a :: k). a :~: a
Refl r
KnownFibres (Cell fs a b) => r
r

instance
  (Finitary p, Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs)
  => Finitary (Reindex (p :: j +-> k) fs)
  where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = forall (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
forall {j} {k} (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
withCell @fs @a @b ([[Natural]] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall (fs :: [[Nat]]). KnownFibres fs => [[Natural]]
fibresVal @(Cell fs a b)))
  toIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Reindex p fs a b -> Natural
toIndex @a @b (Reindex p a b
x) =
    forall (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
forall {j} {k} (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
withCell @fs @a @b
      ( case ([Natural] -> Bool) -> [[Natural]] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex (Natural -> [Natural] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem (p a b -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex p a b
x)) (forall (fs :: [[Nat]]). KnownFibres fs => [[Natural]]
fibresVal @(Cell fs a b)) of
          Just Int
pos -> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral Int
pos
          Maybe Int
Nothing -> [Char] -> Natural
forall a. HasCallStack => [Char] -> a
P.error [Char]
"Reindex: element outside every fibre"
      )
      ((Ob a, Ob b) => Natural) -> p a b -> Natural
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
x
  fromIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Natural -> Reindex p fs a b
fromIndex @a @b Natural
i =
    forall (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
forall {j} {k} (fs :: [[[[Nat]]]]) (a :: k) (b :: j) r.
(Enumerable j, Enumerable k, KnownTable (Objects j) (Objects k) fs,
 Ob a, Ob b) =>
(KnownFibres (Cell fs a b) => r) -> r
withCell @fs @a @b ((KnownFibres (Cell fs a b) => Reindex p fs a b)
 -> Reindex p fs a b)
-> (KnownFibres (Cell fs a b) => Reindex p fs a b)
-> Reindex p fs a b
forall a b. (a -> b) -> a -> b
$
      case [[Natural]] -> Natural -> [Natural]
forall i a. Integral i => [a] -> i -> a
genericIndex (forall (fs :: [[Nat]]). KnownFibres fs => [[Natural]]
fibresVal @(Cell fs a b)) Natural
i of
        Natural
rep : [Natural]
_ -> p a b -> Reindex p fs a b
forall j k (p :: j +-> k) (fs :: [[[[Nat]]]]) (a :: k) (b :: j).
p a b -> Reindex p fs a b
Reindex (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @p Natural
rep)
        [] -> [Char] -> Reindex p fs a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"Reindex: empty fibre"

-- | Whether a predicate on @p@\'s elements picks out a /subprofunctor/: the elements it keeps must
-- be closed under the action, since @'Reindex'@ inherits its 'dimap' from @p@ and so can only carve
-- out a set that is.
--
-- @'dimap' l r@ is @'lmap' l . 'rmap' r@, so closure under the two whiskerings separately is closure
-- under the action: two walks over three objects rather than one over four.
closedUnder
  :: forall {j} {k} (p :: j +-> k)
   . (Finitary p, FiniteCat j, FiniteCat k)
  => (forall a b. (Ob a, Ob b) => p a b -> P.Bool)
  -> P.Bool
closedUnder :: forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool) -> Bool
closedUnder forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep =
  [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and
    ( forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @a -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @b ->
        let kept :: [p a a]
kept = [p a a
z | p a a
z <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b, p a a -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep p a a
z]
        in forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k @P.Bool (\ @c -> [p a a -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep ((a ~> a) -> p a a -> p a a
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> a
g p a a
z) | a ~> a
g <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom k) @c @a, p a a
z <- [p a a]
kept])
             [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
P.++ forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j @P.Bool (\ @d -> [p a a -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep ((a ~> a) -> p a a -> p a a
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> a
h p a a
z) | a ~> a
h <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> j) (a :: j) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom j) @b @d, p a a
z <- [p a a]
kept])
    )

-- | Carve a subprofunctor out of @p@, the caller choosing which elements to keep, and receiving the
-- new object\'s inclusion. This is what 'equalize' does with the elements two transformations agree
-- on, exposed so that a caller can pick out a subobject of its own: it is how a value -- a graph read
-- off a file, say -- becomes an object of @'FINITARY' j k@, as a subobject of a big enough ambient
-- one. The failure continuation is taken when the kept set is not 'closedUnder' the action, and so
-- is no subobject.
withSubobject
  :: forall {j} {k} (p :: j +-> k) r
   . (Finitary p, FiniteCat j, FiniteCat k)
  => (forall a b. (Ob a, Ob b) => p a b -> P.Bool)
  -> (forall q. (Finitary q) => FIN q ~> FIN p -> r)
  -> r
  -> r
withSubobject :: forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool)
-> (forall (q :: j +-> k). Finitary q => (FIN q ~> FIN p) -> r)
-> r
-> r
withSubobject forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep forall (q :: j +-> k). Finitary q => (FIN q ~> FIN p) -> r
ok r
notClosed =
  if forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool) -> Bool
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool) -> Bool
closedUnder @p p a b -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep
    then forall j k r.
(Enumerable j, Enumerable k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]])
-> (forall (t :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) t =>
    r)
-> r
buildTable @j @k (\ @a @b -> [[p a b -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex p a b
x] | p a b
x <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b, p a b -> Bool
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Bool
keep p a b
x]) \ @fs ->
      forall (q :: j +-> k). Finitary q => (FIN q ~> FIN p) -> r
ok @(Reindex p fs) (Prof (Reindex p t) p -> Sub Prof (FIN (Reindex p t)) (FIN p)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((Reindex p t :~> p) -> Prof (Reindex p t) p
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Reindex p a b
x) -> p a b
x))
    else r
notClosed

-- * Equalizers and coequalizers

-- | The element of @p@ that @f@ sends to a given element of @q@, when @f@ is injective and the
-- element is in its image -- which is what both factorizations below need, in opposite directions.
preimage
  :: forall {j} {k} (p :: j +-> k) q (a :: k) (b :: j)
   . (Finitary p, Finitary q, Ob a, Ob b)
  => P.String -> (p a b -> q a b) -> q a b -> p a b
preimage :: forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, Ob a, Ob b) =>
[Char] -> (p a b -> q a b) -> q a b -> p a b
preimage [Char]
msg p a b -> q a b
f q a b
y =
  let toIndexQ :: q a b -> Natural
toIndexQ = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @q @a @b
  in case [p a b
x | p a b
x <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b, q a b -> Natural
toIndexQ (p a b -> q a b
f p a b
x) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== q a b -> Natural
toIndexQ q a b
y] of
       p a b
x : [p a b]
_ -> p a b
x
       [] -> [Char] -> p a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
msg

-- | Partition a list of indices into the equivalence classes generated by a list of pairs. Both
-- levels are sorted, so the classes come out ordered by their least member and the table is canonical.
classes :: [(Natural, Natural)] -> [Natural] -> [[Natural]]
classes :: [(Natural, Natural)] -> [Natural] -> [[Natural]]
classes [(Natural, Natural)]
pairs [Natural]
is = [[Natural]] -> [[Natural]]
forall a. Ord a => [a] -> [a]
sort (([Natural] -> [Natural]) -> [[Natural]] -> [[Natural]]
forall a b. (a -> b) -> [a] -> [b]
P.map [Natural] -> [Natural]
forall a. Ord a => [a] -> [a]
sort (((Natural, Natural) -> [[Natural]] -> [[Natural]])
-> [[Natural]] -> [(Natural, Natural)] -> [[Natural]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr (Natural, Natural) -> [[Natural]] -> [[Natural]]
forall {a}. Eq a => (a, a) -> [[a]] -> [[a]]
merge ((Natural -> [Natural]) -> [Natural] -> [[Natural]]
forall a b. (a -> b) -> [a] -> [b]
P.map (Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: []) [Natural]
is) [(Natural, Natural)]
pairs))
  where
    merge :: (a, a) -> [[a]] -> [[a]]
merge (a
i, a
j) [[a]]
cs = case ([a] -> Bool) -> [[a]] -> ([[a]], [[a]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\[a]
c -> a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem a
i [a]
c Bool -> Bool -> Bool
|| a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
P.elem a
j [a]
c) [[a]]
cs of
      ([], [[a]]
_) -> [Char] -> [[a]]
forall a. HasCallStack => [Char] -> a
P.error [Char]
"classes: an index outside the set being partitioned"
      ([[a]]
hit, [[a]]
miss) -> [[a]] -> [a]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
P.concat [[a]]
hit [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
miss

-- | Equalizers of finitary profunctors between finite categories: at each pair of objects, keep the
-- indices on which the two natural transformations agree, and reify the table.
instance (Enumerable j, Enumerable k) => HasEqualizers (FINITARY j k) where
  equalize :: forall (a :: FINITARY j k) (b :: FINITARY j k) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: FINITARY j k). (e ~> a) -> r) -> r
equalize (Sub (Prof @p @q a1 :~> b1
f)) (Sub (Prof a1 :~> b1
g)) forall (e :: FINITARY j k). (e ~> a) -> r
k =
    forall j k r.
(Enumerable j, Enumerable k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]])
-> (forall (t :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) t =>
    r)
-> r
buildTable @j @k
      ( \ @a @b ->
          let toIndexP :: a1 a b -> Natural
toIndexP = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @p @a @b; toIndexQ :: b1 a b -> Natural
toIndexQ = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @q @a @b
          in [[a1 a b -> Natural
toIndexP a1 a b
x] | a1 a b
x <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b, b1 a b -> Natural
toIndexQ (a1 a b -> b1 a b
a1 :~> b1
f a1 a b
x) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== b1 a b -> Natural
toIndexQ (a1 a b -> b1 a b
a1 :~> b1
g a1 a b
x)]
      )
      \ @fs -> (SUB (Reindex a1 t) ~> a) -> r
forall (e :: FINITARY j k). (e ~> a) -> r
k (Prof (Reindex a1 t) a1 -> Sub Prof (SUB (Reindex a1 t)) (SUB a1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof @(Reindex p fs) \(Reindex a1 a b
x) -> a1 a b
x))
  factorEqualizer :: forall (e :: FINITARY j k) (x :: FINITARY j k)
       (e' :: FINITARY j k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (Sub (Prof @e a1 :~> b1
incl)) (Sub (Prof @e' a1 :~> b1
h)) =
    Prof a1 a1 -> Sub Prof (SUB a1) (SUB a1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof @e' @e \a1 a b
y -> [Char] -> (a1 a b -> b1 a b) -> b1 a b -> a1 a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, Ob a, Ob b) =>
[Char] -> (p a b -> q a b) -> q a b -> p a b
preimage [Char]
"factorEqualizer: h's image must lie within incl's image" a1 a b -> b1 a b
a1 :~> b1
incl (a1 a b -> b1 a b
a1 :~> b1
h a1 a b
y) ((Ob a, Ob b) => a1 a b) -> a1 a b -> a1 a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> a1 a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a1 a b
y)

-- | Coequalizers: at each pair of objects, partition the indices by the equivalence relation the two
-- natural transformations generate, and reify the table. Naturality makes the partition a
-- congruence, so the quotient is again a profunctor.
instance (Enumerable j, Enumerable k) => HasCoequalizers (FINITARY j k) where
  coequalize :: forall (a :: FINITARY j k) (b :: FINITARY j k) r.
(a ~> b)
-> (a ~> b) -> (forall (c :: FINITARY j k). (b ~> c) -> r) -> r
coequalize (Sub (Prof @p @q a1 :~> b1
f)) (Sub (Prof a1 :~> b1
g)) forall (c :: FINITARY j k). (b ~> c) -> r
k =
    forall j k r.
(Enumerable j, Enumerable k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => [[Natural]])
-> (forall (t :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) t =>
    r)
-> r
buildTable @j @k
      ( \ @a @b ->
          let toIndexQ :: b1 a b -> Natural
toIndexQ = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @q @a @b
          in [(Natural, Natural)] -> [Natural] -> [[Natural]]
classes [(b1 a b -> Natural
toIndexQ (a1 a b -> b1 a b
a1 :~> b1
f a1 a b
x), b1 a b -> Natural
toIndexQ (a1 a b -> b1 a b
a1 :~> b1
g a1 a b
x)) | a1 a b
x <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b] ((b1 a b -> Natural) -> [b1 a b] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
P.map b1 a b -> Natural
toIndexQ (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @q @a @b))
      )
      \ @fs -> (b ~> SUB (Reindex b1 t)) -> r
forall (c :: FINITARY j k). (b ~> c) -> r
k (Prof b1 (Reindex b1 t) -> Sub Prof (SUB b1) (SUB (Reindex b1 t))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof @q @(Reindex q fs) b1 a b -> Reindex b1 t a b
b1 :~> Reindex b1 t
forall j k (p :: j +-> k) (fs :: [[[[Nat]]]]) (a :: k) (b :: j).
p a b -> Reindex p fs a b
Reindex))
  factorCoequalizer :: forall (c :: FINITARY j k) (x :: FINITARY j k)
       (c' :: FINITARY j k).
(x ~> c) -> (x ~> c') -> c ~> c'
factorCoequalizer (Sub (Prof @_ @c a1 :~> b1
proj)) (Sub (Prof @_ @c' a1 :~> b1
h)) =
    Prof b1 b1 -> Sub Prof (SUB b1) (SUB b1)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof @c @c' \b1 a b
y -> a1 a b -> b1 a b
a1 :~> b1
h ([Char] -> (a1 a b -> b1 a b) -> b1 a b -> a1 a b
forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, Ob a, Ob b) =>
[Char] -> (p a b -> q a b) -> q a b -> p a b
preimage [Char]
"factorCoequalizer: proj must be onto" a1 a b -> b1 a b
a1 :~> b1
proj b1 a b
y) ((Ob a, Ob b) => b1 a b) -> b1 a b -> b1 a b
forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> b1 a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ b1 a b
y)

-- * Pullbacks, pushouts and images

-- | Pullbacks are equalizers of products, and pushouts coequalizers of coproducts, all of which
-- finitary profunctors have.
instance (Enumerable j, Enumerable k) => HasPullbacks (FINITARY j k)

instance (Enumerable j, Enumerable k) => HasPushouts (FINITARY j k)

-- | The image of a natural transformation is the equalizer of its cokernel pair.
instance (Enumerable j, Enumerable k) => HasEpiMonoFactorization (FINITARY j k)

-- * Natural transformations, enumerated

-- | Enumerate a set of families by brute force: every way of choosing a value at each point of the
-- domain, kept when it satisfies every condition. A condition is checked as soon as both of its
-- points have been chosen, so a violation prunes the whole subtree of completions rather than
-- rejecting each of them in turn -- which is what keeps the candidate space from being the full
-- product. Families come out in the same order as @'P.sequence' choices@ would give them: the
-- earliest point varies slowest.
familiesSatisfying :: [[v]] -> [(P.Int, P.Int, v -> v -> P.Bool)] -> [[v]]
familiesSatisfying :: forall v. [[v]] -> [(Int, Int, v -> v -> Bool)] -> [[v]]
familiesSatisfying [[v]]
choices [(Int, Int, v -> v -> Bool)]
laws = Int -> [v] -> [[v]] -> [[v]]
go Int
0 [] [[v]]
choices
  where
    -- a condition can first be tested at the later of its two points
    byDepth :: IntMap [(Int, Int, v -> v -> Bool)]
byDepth = ([(Int, Int, v -> v -> Bool)]
 -> [(Int, Int, v -> v -> Bool)] -> [(Int, Int, v -> v -> Bool)])
-> [(Int, [(Int, Int, v -> v -> Bool)])]
-> IntMap [(Int, Int, v -> v -> Bool)]
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IM.fromListWith [(Int, Int, v -> v -> Bool)]
-> [(Int, Int, v -> v -> Bool)] -> [(Int, Int, v -> v -> Bool)]
forall a. [a] -> [a] -> [a]
(P.++) [(Int -> Int -> Int
forall a. Ord a => a -> a -> a
P.max Int
src Int
tgt, [(Int
src, Int
tgt, v -> v -> Bool
rel)]) | (Int
src, Int
tgt, v -> v -> Bool
rel) <- [(Int, Int, v -> v -> Bool)]
laws]
    go :: Int -> [v] -> [[v]] -> [[v]]
go Int
_ [v]
chosen [] = [[v] -> [v]
forall a. [a] -> [a]
P.reverse [v]
chosen]
    go Int
i [v]
chosen ([v]
cs : [[v]]
rest) =
      [ [v]
row
      | v
v <- [v]
cs
      , let chosen' :: [v]
chosen' = v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
chosen
      , let at :: Int -> v
at Int
n = [v]
chosen' [v] -> Int -> v
forall a. HasCallStack => [a] -> Int -> a
P.!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
P.- Int
n) -- @chosen'@ holds points @0..i@ in reverse
      , ((Int, Int, v -> v -> Bool) -> Bool)
-> [(Int, Int, v -> v -> Bool)] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
P.all (\(Int
src, Int
tgt, v -> v -> Bool
rel) -> v -> v -> Bool
rel (Int -> v
at Int
src) (Int -> v
at Int
tgt)) ([(Int, Int, v -> v -> Bool)]
-> Int
-> IntMap [(Int, Int, v -> v -> Bool)]
-> [(Int, Int, v -> v -> Bool)]
forall a. a -> Int -> IntMap a -> a
IM.findWithDefault [] Int
i IntMap [(Int, Int, v -> v -> Bool)]
byDepth)
      , [v]
row <- Int -> [v] -> [[v]] -> [[v]]
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
P.+ Int
1) [v]
chosen' [[v]]
rest
      ]

-- | Which of the enumerated families a tabulated one is.
familyIndex :: (P.Eq v) => P.String -> [[v]] -> [v] -> Natural
familyIndex :: forall v. Eq v => [Char] -> [[v]] -> [v] -> Natural
familyIndex [Char]
msg [[v]]
fams [v]
row = case [v] -> [[v]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [v]
row [[v]]
fams of
  Just Int
i -> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral Int
i
  Maybe Int
Nothing -> [Char] -> Natural
forall a. HasCallStack => [Char] -> a
P.error [Char]
msg

-- | One point of the domain of the end @∫ Set(p c d, q c d)@ whose elements are the natural
-- transformations @p -> q@: an object pair and an element of @p@ there. Every end below is one of
-- these: the internal hom only changes the weight @p@, and the subobject classifier also changes
-- what the conditions are read as. So this is the single enumeration the topos is built on.
type NatKey = (Natural, Natural, Natural)

-- | Visit every point of that domain, in one fixed order.
natDomain
  :: forall {j} {k} (p :: j +-> k) r
   . (Finitary p, FiniteCat j, FiniteCat k)
  => (forall a b. (Ob a, Ob b) => p a b -> r)
  -> [r]
natDomain :: forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r
f = forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @a -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @b -> (p a a -> r) -> [p a a] -> [r]
forall a b. (a -> b) -> [a] -> [b]
P.map p a a -> r
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r
f (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b)

natKey
  :: forall {j} {k} (a :: k) (b :: j) (p :: j +-> k). (FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) => p a b -> NatKey
natKey :: forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey p a b
x = (forall (a :: k). (Enumerable k, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @a, forall (a :: j). (Enumerable j, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @b, p a b -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex p a b
x)

-- | Where each point of the domain sits in a tabulated family. This is the same for every family
-- over a given weight, so bind it once outside a loop over them.
natPositions
  :: forall {j} {k} (p :: j +-> k). (Finitary p, FiniteCat j, FiniteCat k) => M.Map NatKey P.Int
natPositions :: forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions = [(NatKey, Int)] -> Map NatKey Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([NatKey] -> [Int] -> [(NatKey, Int)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip (forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain @p @NatKey p a b -> NatKey
forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey) [Int
Item [Int]
0 ..])

-- | Read a tabulated family back as a function on the points, given those positions.
atNatKey :: M.Map NatKey P.Int -> [v] -> NatKey -> v
atNatKey :: forall v. Map NatKey Int -> [v] -> NatKey -> v
atNatKey Map NatKey Int
pos [v]
row NatKey
k = [v]
row [v] -> Int -> v
forall a. HasCallStack => [a] -> Int -> a
P.!! (Map NatKey Int
pos Map NatKey Int -> NatKey -> Int
forall k a. Ord k => Map k a -> k -> a
M.! NatKey
k)

-- | Every natural transformation @p -> q@, as its list of @q@-indices in 'natDomain' order.
-- Naturality is the only condition: the value at @x@ and the value at @'dimap' g h x@ must agree
-- after transport.
natElements
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => [[Natural]]
natElements :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements =
  [[Natural]]
-> [(Int, Int, Natural -> Natural -> Bool)] -> [[Natural]]
forall v. [[v]] -> [(Int, Int, v -> v -> Bool)] -> [[v]]
familiesSatisfying
    -- the same choice list at every point over one object pair, so @q@\'s size is asked once per pair
    (forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @a -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @b -> Natural -> [Natural] -> [[Natural]]
forall i a. Integral i => i -> a -> [a]
genericReplicate (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
size @p @a @b) (Natural -> [Natural]
indices (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural
size @q @a @b)))
    (forall {j} {k} (p :: j +-> k) (q :: j +-> k) v.
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
([Natural] -> v -> v -> Bool) -> [(Int, Int, v -> v -> Bool)]
forall (p :: j +-> k) (q :: j +-> k) v.
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
([Natural] -> v -> v -> Bool) -> [(Int, Int, v -> v -> Bool)]
natConditions @p @q \[Natural]
tr Natural
i Natural
j -> Natural
j Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== [Natural] -> Natural -> Natural
forall i a. Integral i => [a] -> i -> a
genericIndex [Natural]
tr Natural
i)

-- | The conditions as positions in a tabulated family, with @q@\'s transport handed to the
-- relation. Only the internal hom reads that transport; the sieves below ignore it, and pass
-- 'TerminalProfunctor' for @q@ so that computing it costs nothing.
natConditions
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k) v
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => ([Natural] -> v -> v -> P.Bool)
  -> [(P.Int, P.Int, v -> v -> P.Bool)]
natConditions :: forall {j} {k} (p :: j +-> k) (q :: j +-> k) v.
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
([Natural] -> v -> v -> Bool) -> [(Int, Int, v -> v -> Bool)]
natConditions [Natural] -> v -> v -> Bool
rel = [(NatKey -> Int
at NatKey
src, NatKey -> Int
at NatKey
tgt, [Natural] -> v -> v -> Bool
rel [Natural]
tr) | (NatKey
src, NatKey
tgt, [Natural]
tr) <- forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[(NatKey, NatKey, [Natural])]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[(NatKey, NatKey, [Natural])]
natLaws @p @q]
  where
    at :: NatKey -> Int
at = (forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @p Map NatKey Int -> NatKey -> Int
forall k a. Ord k => Map k a -> k -> a
M.!)

-- | The naturality conditions on a transformation. As in 'closedUnder', @'dimap' g h@ is
-- @'lmap' g . 'rmap' h@, so commuting with the two whiskerings separately is commuting with the
-- action: two walks over three objects rather than one over four, and the transport table depends
-- on the arrow alone rather than on each element.
natLaws
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => [(NatKey, NatKey, [Natural])]
natLaws :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[(NatKey, NatKey, [Natural])]
natLaws =
  forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @a -> forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @b ->
    let xs :: [p a a]
xs = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @p @a @b; qs :: [q a a]
qs = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @q @a @b
    in forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k @(NatKey, NatKey, [Natural])
         ( \ @c -> [(p a a -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey p a a
x, p a a -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey ((a ~> a) -> p a a -> p a a
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> a
g p a a
x), [Natural]
tr) | a ~> a
g <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: k +-> k) (a :: k) (b :: k).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom k) @c @a, let tr :: [Natural]
tr = (q a a -> Natural) -> [q a a] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
P.map (q a a -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => q a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex (q a a -> Natural) -> (q a a -> q a a) -> q a a -> Natural
forall b c a. (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
. (a ~> a) -> q a a -> q a a
forall (c :: k) (a :: k) (b :: j). (c ~> a) -> q a b -> q c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> a
g) [q a a]
qs, p a a
x <- [p a a]
xs]
         )
         [(NatKey, NatKey, [Natural])]
-> [(NatKey, NatKey, [Natural])] -> [(NatKey, NatKey, [Natural])]
forall a. [a] -> [a] -> [a]
P.++ forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j @(NatKey, NatKey, [Natural])
           ( \ @d -> [(p a a -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey p a a
x, p a a -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey ((a ~> a) -> p a a -> p a a
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> a
h p a a
x), [Natural]
tr) | a ~> a
h <- forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
forall (p :: j +-> j) (a :: j) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @(Hom j) @b @d, let tr :: [Natural]
tr = (q a a -> Natural) -> [q a a] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
P.map (q a a -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => q a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex (q a a -> Natural) -> (q a a -> q a a) -> q a a -> Natural
forall b c a. (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
. (a ~> a) -> q a a -> q a a
forall (b :: j) (d :: j) (a :: k). (b ~> d) -> q a b -> q a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> a
h) [q a a]
qs, p a a
x <- [p a a]
xs]
           )

-- | A natural transformation as its table of @q@-indices, in 'natDomain' order. That is everything
-- there is to see of one, so it serves for both comparing and showing.
natTable
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => (p :~> q)
  -> [Natural]
natTable :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
natTable p :~> q
f = forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain @p (q a b -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => q a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex (q a b -> Natural) -> (p a b -> q a b) -> p a b -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. p a b -> q a b
p :~> q
f)

-- | Every natural transformation @p -> q@, as an arrow of @'FINITARY' j k@. This is what makes the
-- category of finitary profunctors testable: its hom-sets are enumerable, so a generator can pick
-- from them, where in general a natural transformation is not something one can generate.
natTransformations
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => [FIN p ~> FIN q]
natTransformations :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[FIN p ~> FIN q]
natTransformations = let pos :: Map NatKey Int
pos = forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: k -> j -> Type).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @p in ([Natural] -> Sub Prof (SUB p) (SUB q))
-> [[Natural]] -> [Sub Prof (SUB p) (SUB q)]
forall a b. (a -> b) -> [a] -> [b]
P.map (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
Map NatKey Int -> [Natural] -> FIN p ~> FIN q
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
Map NatKey Int -> [Natural] -> FIN p ~> FIN q
natAt @p @q Map NatKey Int
pos) (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: k -> j -> Type) (q :: k -> j -> Type).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @p @q)

-- | A tabulated transformation as an arrow.
natAt
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k)
  => M.Map NatKey P.Int
  -> [Natural]
  -> FIN p ~> FIN q
natAt :: forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
Map NatKey Int -> [Natural] -> FIN p ~> FIN q
natAt Map NatKey Int
pos [Natural]
row = Prof p q -> Sub Prof (SUB p) (SUB q)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((p :~> q) -> Prof p q
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \p a b
x -> p a b
x p a b -> ((Ob a, Ob b) => q a b) -> q a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @q (Map NatKey Int -> [Natural] -> NatKey -> Natural
forall v. Map NatKey Int -> [v] -> NatKey -> v
atNatKey Map NatKey Int
pos [Natural]
row (p a b -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey p a b
x)))

-- | @'FINITARY' j k@ is locally finite: its own hom-profunctor is finitary, by 'natTransformations'.
-- So the numbering above is not just a testing device, it is the skeleton of each hom-set, and the
-- 'Finitary' laws apply to it like to any other. (It is not a 'FiniteCat' -- there are unboundedly
-- many finitary profunctors -- which is exactly the difference between finite and locally finite.)
instance (FiniteCat j, FiniteCat k) => Finitary (Sub Prof :: CAT (FINITARY j k)) where
  size :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
Natural
size @f @g = [[Natural]] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(UN SUB f) @(UN SUB g))
  toIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
Sub Prof a b -> Natural
toIndex @f @g (Sub (Prof a1 :~> b1
n)) =
    [Char] -> [[Natural]] -> [Natural] -> Natural
forall v. Eq v => [Char] -> [[v]] -> [v] -> Natural
familyIndex
      [Char]
"toIndex: the transformation is not natural"
      (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(UN SUB f) @(UN SUB g))
      (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
natTable @(UN SUB f) @(UN SUB g) a1 a b -> b1 a b
UN SUB a a b -> UN SUB b a b
a1 :~> b1
UN SUB a :~> UN SUB b
n)
  fromIndex :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
Natural -> Sub Prof a b
fromIndex @f @g Natural
i =
    forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
Map NatKey Int -> [Natural] -> FIN p ~> FIN q
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
Map NatKey Int -> [Natural] -> FIN p ~> FIN q
natAt @(UN SUB f) @(UN SUB g) (forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @(UN SUB f)) ([[Natural]] -> Natural -> [Natural]
forall i a. Integral i => [a] -> i -> a
genericIndex (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(UN SUB f) @(UN SUB g)) Natural
i)
  elements :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(Ob a, Ob b) =>
[Sub Prof a b]
elements @f @g = forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[FIN p ~> FIN q]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[FIN p ~> FIN q]
natTransformations @(UN SUB f) @(UN SUB g)

-- | What the internal hom at @a@\/@b@ is a set of natural transformations /out of/. An element of
-- it over @c@\/@d@ is an arrow into @a@, an arrow out of @b@ and an element of @p@ -- exactly the
-- three arguments an 'Exp' takes.
type ExpWeight :: forall {j} {k}. (j +-> k) -> k -> j -> j +-> k
type ExpWeight p a b = Yo a (OP b) :*: p

-- | The internal hom of finitary profunctors is finitary: its elements are the natural
-- transformations out of 'ExpWeight', enumerated. Nothing here is a formula in the sizes of @p@ and
-- @q@ -- the count depends on how the arrows of @j@ and @k@ compose -- which is why 'size' is a
-- value and not a type family.
instance (Finitary p, Finitary q, FiniteCat j, FiniteCat k) => Finitary (p :~>: q :: j +-> k) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = [[Natural]] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(ExpWeight p a b) @q)

  -- the search is bound outside the argument lambda, so a caller can share it across a hom-set
  toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => (:~>:) p q a b -> Natural
toIndex @a @b = \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f) ->
    [Char] -> [[Natural]] -> [Natural] -> Natural
forall v. Eq v => [Char] -> [[v]] -> [v] -> Natural
familyIndex [Char]
"toIndex: the family is not natural" [[Natural]]
es (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
natTable @(ExpWeight p a b) @q \(Yo a ~> a
ca b1 ~> b
bd :*: p a b
x) -> (a ~> a) -> (b ~> b) -> p a b -> q a b
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f a ~> a
ca b ~> b
b1 ~> b
bd p a b
x)
    where
      es :: [[Natural]]
es = forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(ExpWeight p a b) @q
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> (:~>:) p q a b
fromIndex @a @b Natural
i = forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Natural] -> (:~>:) p q a b
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Natural] -> (:~>:) p q a b
expAt @p @q (forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @(ExpWeight p a b)) ([[Natural]] -> Natural -> [Natural]
forall i a. Integral i => [a] -> i -> a
genericIndex (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(ExpWeight p a b) @q) Natural
i)
  elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [(:~>:) p q a b]
elements @a @b =
    let pos :: Map NatKey Int
pos = forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @(ExpWeight p a b) in ([Natural] -> (:~>:) p q a b) -> [[Natural]] -> [(:~>:) p q a b]
forall a b. (a -> b) -> [a] -> [b]
P.map (forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Natural] -> (:~>:) p q a b
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Natural] -> (:~>:) p q a b
expAt @p @q Map NatKey Int
pos) (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @(ExpWeight p a b) @q)

-- | A tabulated family as an element of the internal hom.
expAt
  :: forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j)
   . (Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => M.Map NatKey P.Int
  -> [Natural]
  -> (p :~>: q) a b
expAt :: forall {j} {k} (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Natural] -> (:~>:) p q a b
expAt Map NatKey Int
pos [Natural]
row = (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd p c d
x -> c ~> a
ca (c ~> a) -> ((Ob c, Ob a) => q c d) -> q c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
bd (b ~> d) -> ((Ob b, Ob d) => q c d) -> q c d
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex @q (Map NatKey Int -> [Natural] -> NatKey -> Natural
forall v. Map NatKey Int -> [v] -> NatKey -> v
atNatKey Map NatKey Int
pos [Natural]
row ((:*:) (Yo a (OP b)) p c d -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey ((c ~> a) -> (b ~> d) -> Yo a (OP b) c d
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a (OP b1) c d
Yo c ~> a
ca b ~> d
bd Yo a (OP b) c d -> p c d -> (:*:) (Yo a (OP b)) p c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: p c d
x)))

-- | Finitary profunctors are cartesian closed. The 'PROD' wrapper is what makes the tensor the
-- product rather than Day convolution, exactly as it does for @j '+->' k@ itself.
instance (FiniteCat j, FiniteCat k) => Closed (PROD (FINITARY j k)) where
  type p ~~> q = PR (SUB (UN SUB (UN PR p) :~>: UN SUB (UN PR q)))
  withObExp :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k))
       (c :: PROD (FINITARY j k)).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Prod (Sub (Prof (UN SUB (UN PR a) :*: UN SUB (UN PR b)) :~> b1
n))) = Sub Prof (SUB (UN SUB (UN PR a))) (SUB (UN SUB (UN PR b) :~>: b1))
-> Prod
     (Sub Prof)
     (PR (SUB (UN SUB (UN PR a))))
     (PR (SUB (UN SUB (UN PR b) :~>: b1)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof (UN SUB (UN PR a)) (UN SUB (UN PR b) :~>: b1)
-> Sub
     Prof (SUB (UN SUB (UN PR a))) (SUB (UN SUB (UN PR b) :~>: b1))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((UN SUB (UN PR a) :~> (UN SUB (UN PR b) :~>: b1))
-> Prof (UN SUB (UN PR a)) (UN SUB (UN PR b) :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \UN SUB (UN PR a) a b
p -> UN SUB (UN PR a) a b
p UN SUB (UN PR a) a b
-> ((Ob a, Ob b) => (:~>:) (UN SUB (UN PR b)) b1 a b)
-> (:~>:) (UN SUB (UN PR b)) b1 a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> UN SUB (UN PR b) c d -> b1 c d)
-> (:~>:) (UN SUB (UN PR b)) b1 a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd UN SUB (UN PR b) c d
q -> (:*:) (UN SUB (UN PR a)) (UN SUB (UN PR b)) c d -> b1 c d
(UN SUB (UN PR a) :*: UN SUB (UN PR b)) :~> b1
n ((c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) a b -> UN SUB (UN PR a) c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) a b -> UN SUB (UN PR a) c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
ca b ~> d
bd UN SUB (UN PR a) a b
p UN SUB (UN PR a) c d
-> UN SUB (UN PR b) c d
-> (:*:) (UN SUB (UN PR a)) (UN SUB (UN PR b)) c d
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: UN SUB (UN PR b) c d
q)))
  apply :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = Sub
  Prof
  (SUB
     ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a)))
  (SUB (UN SUB (UN PR b)))
-> Prod
     (Sub Prof)
     (PR
        (SUB
           ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))))
     (PR (SUB (UN SUB (UN PR b))))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof
  ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
  (UN SUB (UN PR b))
-> Sub
     Prof
     (SUB
        ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a)))
     (SUB (UN SUB (UN PR b)))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
 :~> UN SUB (UN PR b))
-> Prof
     ((UN SUB (UN PR a) :~>: UN SUB (UN PR b)) :*: UN SUB (UN PR a))
     (UN SUB (UN PR b))
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) c d -> UN SUB (UN PR b) c d
f :*: UN SUB (UN PR a) a b
q) -> (a ~> a)
-> (b ~> b) -> UN SUB (UN PR a) a b -> UN SUB (UN PR b) a b
forall (c :: k) (d :: j).
(c ~> a)
-> (b ~> d) -> UN SUB (UN PR a) c d -> UN SUB (UN PR b) c d
f a ~> a
forall (a :: k). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id UN SUB (UN PR a) a b
q ((Ob a, Ob b) => UN SUB (UN PR b) a b)
-> UN SUB (UN PR a) a b -> UN SUB (UN PR b) a b
forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> UN SUB (UN PR a) a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ UN SUB (UN PR a) a b
q))
  Prod (Sub (Prof a1 :~> b1
m)) ^^^ :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k))
       (x :: PROD (FINITARY j k)) (y :: PROD (FINITARY j k)).
(b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y)
^^^ Prod (Sub (Prof a1 :~> b1
n)) = Sub Prof (SUB (b1 :~>: a1)) (SUB (a1 :~>: b1))
-> Prod (Sub Prof) (PR (SUB (b1 :~>: a1))) (PR (SUB (a1 :~>: b1)))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof (b1 :~>: a1) (a1 :~>: b1)
-> Sub Prof (SUB (b1 :~>: a1)) (SUB (a1 :~>: b1))
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (((b1 :~>: a1) :~> (a1 :~>: b1)) -> Prof (b1 :~>: a1) (a1 :~>: b1)
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(Exp forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f) -> (forall (c :: k) (d :: j).
 (c ~> a) -> (b ~> d) -> a1 c d -> b1 c d)
-> (:~>:) a1 b1 a b
forall {k} {k1} (a :: k) (b :: k1) (p :: k -> k1 -> Type)
       (q :: k -> k1 -> Type).
(Ob a, Ob b) =>
(forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> p c d -> q c d)
-> (:~>:) p q a b
Exp \c ~> a
ca b ~> d
bd a1 c d
p -> a1 c d -> b1 c d
a1 :~> b1
m ((c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> b1 c d -> a1 c d
f c ~> a
ca b ~> d
bd (a1 c d -> b1 c d
a1 :~> b1
n a1 c d
p))))

-- * The subobject classifier

-- | Every sieve at @a@\/@b@, as the points of @'Yo' a ('OP' b)@ it contains, in 'natDomain' order:
-- all subsets, kept when closed. This is the same end again, at the weight @'Yo' a ('OP' b)@ and
-- valued in booleans, with the naturality conditions read as implications rather than equations.
sieveElements :: forall {j} {k} (a :: k) (b :: j). (FiniteCat j, FiniteCat k, Ob a, Ob b) => [[P.Bool]]
sieveElements :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
sieveElements =
  [[Bool]] -> [(Int, Int, Bool -> Bool -> Bool)] -> [[Bool]]
forall v. [[v]] -> [(Int, Int, v -> v -> Bool)] -> [[v]]
familiesSatisfying
    (forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain @(Yo a (OP b)) ([Bool] -> Yo a (OP b) a b -> [Bool]
forall a b. a -> b -> a
P.const [Bool
Item [Bool]
P.False, Bool
Item [Bool]
P.True]))
    (forall {j} {k} (p :: j +-> k) (q :: j +-> k) v.
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
([Natural] -> v -> v -> Bool) -> [(Int, Int, v -> v -> Bool)]
forall (p :: j +-> k) (q :: j +-> k) v.
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
([Natural] -> v -> v -> Bool) -> [(Int, Int, v -> v -> Bool)]
natConditions @(Yo a (OP b)) @TerminalProfunctor \[Natural]
_ Bool
s Bool
t -> Bool -> Bool
P.not Bool
s Bool -> Bool -> Bool
P.|| Bool
t)

-- | A sieve as the tabulation of its membership, in 'natDomain' order -- the inverse of 'sieveAt'.
sieveTable :: forall {j} {k} (a :: k) (b :: j). (FiniteCat j, FiniteCat k) => Sieve a b -> [P.Bool]
sieveTable :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> [Bool]
sieveTable (Sieve forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s) = forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain @(Yo a (OP b)) \(Yo a ~> a
ca b1 ~> b
bd) -> (a ~> a) -> (b ~> b) -> Bool
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s a ~> a
ca b ~> b
b1 ~> b
bd

instance (FiniteCat j, FiniteCat k) => Finitary (Sieve :: j +-> k) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = [[Bool]] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
sieveElements @a @b)
  toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Sieve a b -> Natural
toIndex @a @b = [Char] -> [[Bool]] -> [Bool] -> Natural
forall v. Eq v => [Char] -> [[v]] -> [v] -> Natural
familyIndex [Char]
"toIndex: not a sieve" (forall (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
sieveElements @a @b) ([Bool] -> Natural)
-> (Sieve a b -> [Bool]) -> Sieve a b -> Natural
forall b c a. (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
. Sieve a b -> [Bool]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> [Bool]
sieveTable
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> Sieve a b
fromIndex @a @b Natural
i = Map NatKey Int -> [Bool] -> Sieve a b
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Bool] -> Sieve a b
sieveAt (forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @(Yo a (OP b))) ([[Bool]] -> Natural -> [Bool]
forall i a. Integral i => [a] -> i -> a
genericIndex (forall (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
sieveElements @a @b) Natural
i)
  elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [Sieve a b]
elements @a @b = let pos :: Map NatKey Int
pos = forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
Map NatKey Int
natPositions @(Yo a (OP b)) in ([Bool] -> Sieve a b) -> [[Bool]] -> [Sieve a b]
forall a b. (a -> b) -> [a] -> [b]
P.map (Map NatKey Int -> [Bool] -> Sieve a b
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Bool] -> Sieve a b
sieveAt Map NatKey Int
pos) (forall (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Bool]]
sieveElements @a @b)

-- | A tabulated sieve as a sieve.
sieveAt
  :: forall {j} {k} (a :: k) (b :: j)
   . (FiniteCat j, FiniteCat k, Ob a, Ob b)
  => M.Map NatKey P.Int
  -> [P.Bool]
  -> Sieve a b
sieveAt :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map NatKey Int -> [Bool] -> Sieve a b
sieveAt Map NatKey Int
pos [Bool]
row = (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool)
-> Sieve a b
forall {k} {j} (a :: k) (b :: j).
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool)
-> Sieve a b
Sieve \c ~> a
ca b ~> d
bd -> c ~> a
ca (c ~> a) -> ((Ob c, Ob a) => Bool) -> Bool
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
bd (b ~> d) -> ((Ob b, Ob d) => Bool) -> Bool
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// Map NatKey Int -> [Bool] -> NatKey -> Bool
forall v. Map NatKey Int -> [v] -> NatKey -> v
atNatKey Map NatKey Int
pos [Bool]
row (Yo a (OP b) c d -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey ((c ~> a) -> (b ~> d) -> Yo a (OP b) c d
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a (OP b1) c d
Yo c ~> a
ca b ~> d
bd))

-- | The subobject classifier is the profunctor of sieves, and an arrow classifies its graph: the
-- sieve of all the ways an element of @p@ and one of @q@ can be carried to a matching pair.
instance (FiniteCat j, FiniteCat k) => HasSubobjectClassifier (PROD (FINITARY j k)) where
  type Omega = PR (SUB Sieve)
  true :: TerminalObject ~> Omega
true = Sub Prof (SUB TerminalProfunctor) (SUB Sieve)
-> Prod (Sub Prof) (PR (SUB TerminalProfunctor)) (PR (SUB Sieve))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof TerminalProfunctor Sieve
-> Sub Prof (SUB TerminalProfunctor) (SUB Sieve)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub ((TerminalProfunctor :~> Sieve) -> Prof TerminalProfunctor Sieve
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \TerminalProfunctor a b
TerminalProfunctor -> Sieve a b
forall {j} {k} (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
Sieve a b
maximalSieve))
  classifyGraph :: forall (a :: PROD (FINITARY j k)) (b :: PROD (FINITARY j k)).
(a ~> b) -> (a && b) ~> Omega
classifyGraph (Prod (Sub (Prof @_ @q a1 :~> b1
f))) =
    Sub Prof (SUB (a1 :*: b1)) (SUB Sieve)
-> Prod (Sub Prof) (PR (SUB (a1 :*: b1))) (PR (SUB Sieve))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof (a1 :*: b1) Sieve -> Sub Prof (SUB (a1 :*: b1)) (SUB Sieve)
forall {k} (ob :: OB k) (a1 :: k) (b1 :: k) (p :: CAT k).
(ob a1, ob b1) =>
p a1 b1 -> Sub p (SUB a1) (SUB b1)
Sub (((a1 :*: b1) :~> Sieve) -> Prof (a1 :*: b1) Sieve
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \(a1 a b
x :*: b1 a b
y) -> a1 a b
x a1 a b -> ((Ob a, Ob b) => Sieve a b) -> Sieve a b
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool)
-> Sieve a b
forall {k} {j} (a :: k) (b :: j).
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool)
-> Sieve a b
Sieve \c ~> a
g b ~> d
h -> c ~> a
g (c ~> a) -> ((Ob c, Ob a) => Bool) -> Bool
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// b ~> d
h (b ~> d) -> ((Ob b, Ob d) => Bool) -> Bool
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
forall (p :: k -> j -> Type) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex @q (a1 c d -> b1 c d
a1 :~> b1
f ((c ~> a) -> (b ~> d) -> a1 a b -> a1 c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> a1 a b -> a1 c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
g b ~> d
h a1 a b
x)) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== b1 c d -> Natural
forall (a :: k) (b :: j). (Ob a, Ob b) => b1 a b -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex ((c ~> a) -> (b ~> d) -> b1 a b -> b1 c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> b1 a b -> b1 c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap c ~> a
g b ~> d
h b1 a b
y)))

-- | Finitary profunctors between finite categories form an elementary topos: finite limits and
-- colimits, cartesian closed, a subobject classifier, and image factorization.
instance (FiniteCat j, FiniteCat k) => ElementaryTopos (PROD (FINITARY j k))