{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Profunctors whose hom-sets are finite and numbered: @p a b@ is in bijection with an initial
-- segment of the naturals. This is the profunctor form of the skeleton of the category of finite
-- sets, and it is what makes limits and colimits computable. An element is an index, so a subset or
-- a quotient of a hom-set is a table of indices, which a computation can produce and reify into a
-- fresh object; an arbitrary profunctor offers no handle on its hom-set other than the type itself.
--
-- The numbering is deliberately a /value/, as in "Proarrow.Category.Instance.FinHask": a size that
-- had to be a type family could only ever be a formula in the sizes it is built from, which rules
-- out every construction whose count depends on how arrows compose -- the exponential and the
-- subobject classifier among them. As values, those are enumerations like any other.
--
-- This is the sibling of "Proarrow.Category.Enriched.Thin", which it builds on: a
-- 'Proarrow.Category.Enriched.Thin.DecidableProfunctor' is the special case where every size is zero
-- or one, its 'Proarrow.Category.Enriched.Thin.Decision' being the pair 'toIndex'\/'fromIndex', and
-- 'decidableSize' and 'decidableFromIndex' build such an instance. As there, the class, the kind
-- wrapper 'FINITARY' and the instances for the basic profunctors all live together here.
module Proarrow.Category.Enriched.Finitary where

import Data.Kind (Constraint)
import Data.List (elemIndex, findIndex, genericIndex, genericLength, genericTake, 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 Data.Universe.Class qualified as U
import Data.Universe.Helpers qualified as U
import Numeric.Natural (Natural)
import Prelude (Maybe (..), compare, show, ($), (+), (-), (<), (==), (||))
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin
  ( DecidableProfunctor (..)
  , Decision (..)
  , Entry
  , Enumerable (..)
  , Finite (..)
  , Indexed (..)
  , IndexedList (..)
  , KnownList (..)
  )
import Proarrow.Category.Instance.Bool (Booleans)
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Topos
  ( ElementaryTopos
  , HasEpiMonoFactorization (..)
  , HasSubobjectClassifier (..)
  , defaultFactorize
  )
import Proarrow.Colimit.BinaryCoproduct (HasBinaryCoproducts (..))
import Proarrow.Colimit.Coequalizer (HasCoequalizers (..))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Colimit.Pushout (HasPushouts)
import Proarrow.Core (CategoryOf (..), Hom, Profunctor (..), Promonad (..), UN, lmap, rmap, (//), 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 (..))
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))

-- | A profunctor with finite, numbered hom-sets. 'toIndex' and 'fromIndex' are inverse for indices
-- below 'size'; @fromIndex@ of anything else is an error, as is 'toIndex' of an element that is not
-- one the instance can produce (which only an unlawfully built value can be).
--
-- An instance whose elements are found by searching should define 'elements' and read 'size' off
-- it, rather than let the default call 'fromIndex' once per element and repeat the search each time.
type Finitary :: forall {j} {k}. j +-> k -> Constraint
class (Profunctor p) => Finitary (p :: j +-> k) where
  -- | How many elements the hom-set has.
  size :: (Ob (a :: k), Ob (b :: j)) => Natural

  -- | Where an element sits in 'elements'. Takes its objects like the others do, so that an
  -- instance that has to search can bind the search outside the argument lambda and a caller can
  -- share it with @let toIndexP = 'toIndex' \@p \@a \@b@.
  toIndex :: (Ob (a :: k), Ob (b :: j)) => p a b -> Natural

  -- | The element at a position.
  fromIndex :: (Ob (a :: k), Ob (b :: j)) => Natural -> p a b

  -- | All elements of a hom-set, in index order.
  elements :: (Ob (a :: k), Ob (b :: j)) => [p a b]
  elements @a @b = (Natural -> p a b) -> [Natural] -> [p a b]
forall a b. (a -> b) -> [a] -> [b]
P.map (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 -> [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 @p @a @b))

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

-- | @[0 .. n-1]@, which @n@ being a 'Natural' rules out writing directly.
indices :: Natural -> [Natural]
indices :: Natural -> [Natural]
indices Natural
n = Natural -> [Natural] -> [Natural]
forall i a. Integral i => i -> [a] -> [a]
genericTake Natural
n [Natural
Item [Natural]
0 ..]

-- | The position of an object in its kind's object list.
objIndex :: forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex :: forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
withIndex @k @a (SNat (Index a) -> Natural
forall (n :: Nat). SNat n -> Natural
N.snatToNatural (forall (n :: Nat). SNatI n => SNat n
snat @(Index a)))

-- | Everything an enumeration of a kind's objects can do at each of them, concatenated.
foreachOb :: forall k r. (Enumerable k) => (forall (a :: k). (Ob a) => [r]) -> [r]
foreachOb :: forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb forall (a :: k). Ob a => [r]
f = IndexedList (Objects k) -> [r]
forall (as :: [k]). IndexedList as -> [r]
go (forall k. Finite k => IndexedList (Objects k)
finite @k)
  where
    go :: forall (as :: [k]). IndexedList as -> [r]
    go :: forall (as :: [k]). IndexedList as -> [r]
go IndexedList as
FNil = []
    go (FCons @a IndexedList as1
as) = forall k (a :: k) r.
(Enumerable k, KnownIndex a) =>
(Ob a => r) -> r
withOb @k @a (forall (a :: k). Ob a => [r]
f @a) [r] -> [r] -> [r]
forall a. [a] -> [a] -> [a]
P.++ IndexedList as1 -> [r]
forall (as :: [k]). IndexedList as -> [r]
go IndexedList as1
as

-- * Thin profunctors

-- | A decidable profunctor has one element where it holds and none where it does not. These cannot
-- be @default@ method bodies: 'size' and 'fromIndex' do not mention their objects except in a
-- constraint, so GHC cannot tie a default body's objects to the instance's.
decidableSize :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (DecidableProfunctor p, Ob a, Ob b) => Natural
decidableSize :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural
decidableSize = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b of
  Yes p a b
_ -> Natural
1
  Decision p a b (Holds p a b)
No -> Natural
0

decidableFromIndex
  :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (DecidableProfunctor p, Ob a, Ob b) => Natural -> p a b
decidableFromIndex :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural -> p a b
decidableFromIndex Natural
_ = case forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b of
  Yes p a b
x -> p a b
x
  Decision p a b (Holds p a b)
No -> [Char] -> p a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"fromIndex: the profunctor does not hold here"

-- * Hom-sets as finite sets

-- | An element of a hom-set of @p@, viewed as an element of a /finite set/: every instance the
-- @universe@ package asks for is supplied by the numbering, with 'toIndex' standing in for equality
-- and ordering. This is what makes a finitary profunctor a profunctor enriched in
-- 'Proarrow.Category.Instance.FinHask.FINHASK' -- see its
-- @'Proarrow.Category.Enriched.EnrichedProfunctor' FINHASK@
-- instance -- exactly as a decided profunctor is one enriched in
-- 'Proarrow.Category.Instance.Bool.BOOL'.
newtype Elt (p :: j +-> k) (a :: k) (b :: j) = Elt {forall j k (p :: j +-> k) (a :: k) (b :: j). Elt p a b -> p a b
unElt :: p a b}

instance (Finitary p, Ob a, Ob b) => U.Universe (Elt (p :: j +-> k) a b) where
  universe :: [Elt p a b]
universe = (p a b -> Elt p a b) -> [p a b] -> [Elt p a b]
forall a b. (a -> b) -> [a] -> [b]
P.map p a b -> Elt p a b
forall j k (p :: j +-> k) (a :: k) (b :: j). p a b -> Elt p a b
Elt (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)

instance (Finitary p, Ob a, Ob b) => U.Finite (Elt (p :: j +-> k) a b) where
  cardinality :: Tagged (Elt p a b) Natural
cardinality = Natural -> Tagged (Elt p a b) Natural
forall {k} (s :: k) b. b -> Tagged s b
U.Tagged (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)

instance (Finitary p) => P.Eq (Elt (p :: j +-> k) a b) where
  Elt p a b
x == :: Elt p a b -> Elt p a b -> Bool
== Elt p a b
y = (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 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 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
y) ((Ob a, Ob b) => Bool) -> p a b -> Bool
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

instance (Finitary p) => P.Ord (Elt (p :: j +-> k) a b) where
  compare :: Elt p a b -> Elt p a b -> Ordering
compare (Elt p a b
x) (Elt p a b
y) = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare (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 -> 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
y) ((Ob a, Ob b) => Ordering) -> p a b -> Ordering
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

-- | Its 'P.Eq' and 'P.Ord' cost whatever 'toIndex' costs, so an instance intended for enrichment
-- should compute 'toIndex' directly rather than by searching 'elements' -- 'finiteToIndex' searches,
-- which is fine for small hom-sets and not for large ones.

-- | The index, there being nothing else to show: a hom-set of a finitary profunctor is known only up
-- to its numbering.
instance (Finitary p) => P.Show (Elt (p :: j +-> k) a b) where
  show :: Elt p a b -> [Char]
show (Elt p a b
x) = Natural -> [Char]
forall a. Show a => a -> [Char]
P.show (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) ((Ob a, Ob b) => [Char]) -> p a b -> [Char]
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

-- | A category whose hom-sets are finite: the 'Finitary' counterpart of
-- 'Proarrow.Category.Enriched.Thin.Decidable', and one half of 'FiniteCat'.
class (CategoryOf k, Finitary (Hom k)) => LocallyFinite k

instance (CategoryOf k, Finitary (Hom k)) => LocallyFinite k

-- | A profunctor between categories with finite hom-sets is finitary exactly when it is enriched in
-- finite sets, so a 'Finitary' instance can be read off an enrichment as well as the other way
-- round: these are the counterparts of 'decidableSize' and 'decidableFromIndex' one level up.
--
-- 'finiteToIndex' and 'finiteFromIndex' number a hom-set by /searching/ its 'U.universeF', which is
-- all a bare 'U.Finite' instance allows. That is fine for small hom-sets, and an instance whose
-- hom-sets are large should compute the index arithmetically instead --
-- 'Proarrow.Category.Instance.FinHask.FinHask' does, because 'Elt'\'s 'P.Ord' is @'P.compare'@ on
-- indices and so pays for every comparison.
finiteSize :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (U.Finite (p a b)) => Natural
finiteSize :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Finite (p a b) =>
Natural
finiteSize = Tagged (p a b) Natural -> Natural
forall {k} (s :: k) b. Tagged s b -> b
U.unTagged (forall a. Finite a => Tagged a Natural
U.cardinality @(p a b))

finiteToIndex :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (U.Finite (p a b), P.Eq (p a b)) => p a b -> Natural
finiteToIndex :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finite (p a b), Eq (p a b)) =>
p a b -> Natural
finiteToIndex p a b
x = case p a b -> [p a b] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex p a b
x [p a b]
forall a. Finite a => [a]
U.universeF 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]
"toIndex: not in the universe of the hom-set"

finiteFromIndex :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j). (U.Finite (p a b)) => Natural -> p a b
finiteFromIndex :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Finite (p a b) =>
Natural -> p a b
finiteFromIndex Natural
i = [p a b] -> Natural -> p a b
forall i a. Integral i => [a] -> i -> a
genericIndex (forall a. Finite a => [a]
U.universeF @(p a b)) Natural
i

-- | The one-object category has one arrow.
instance Finitary Unit where
  size :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => Natural
size = Natural
1
  toIndex :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => Unit a b -> Natural
toIndex Unit a b
Unit = Natural
0
  fromIndex :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => Natural -> Unit a b
fromIndex Natural
_ = Unit a b
Unit '() '()
Unit

-- | @'Proarrow.Category.Instance.Bool.BOOL'@ is thin, so each hom-set holds at most the one arrow.
instance Finitary Booleans where
  size :: forall (a :: BOOL) (b :: BOOL). (Ob a, Ob b) => Natural
size @a @b = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural
forall (p :: BOOL +-> BOOL) (a :: BOOL) (b :: BOOL).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural
decidableSize @Booleans @a @b
  toIndex :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
Booleans a b -> Natural
toIndex Booleans a b
_ = Natural
0
  fromIndex :: forall (a :: BOOL) (b :: BOOL).
(Ob a, Ob b) =>
Natural -> Booleans a b
fromIndex @a @b = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural -> p a b
forall (p :: BOOL +-> BOOL) (a :: BOOL) (b :: BOOL).
(DecidableProfunctor p, Ob a, Ob b) =>
Natural -> p a b
decidableFromIndex @Booleans @a @b

-- * Products and coproducts

-- | The terminal profunctor has one element everywhere.
instance (CategoryOf j, CategoryOf k) => Finitary (TerminalProfunctor :: j +-> k) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size = Natural
1
  toIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
TerminalProfunctor a b -> Natural
toIndex TerminalProfunctor a b
TerminalProfunctor = Natural
0
  fromIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Natural -> TerminalProfunctor a b
fromIndex Natural
_ = TerminalProfunctor a b
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor

-- | A pair of indices as one index, row-major: @i * 'size' \@q + j@.
instance (Finitary p, Finitary q) => Finitary (p :*: q) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = 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 -> Natural
forall a. Num a => a -> a -> a
P.* 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
  toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => (:*:) p q a b -> Natural
toIndex @a @b (p a b
x :*: q a b
y) = 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 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
P.* 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 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ 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
y
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> (:*:) p q a b
fromIndex @a @b Natural
i = case 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 of
    Natural
0 -> [Char] -> (:*:) p q a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"fromIndex: a factor of the product has no elements"
    Natural
n -> let (Natural
l, Natural
r) = Natural
i Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`P.divMod` Natural
n in Natural -> p a b
forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex Natural
l p a b -> q a b -> (:*:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: Natural -> q a b
forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex Natural
r

-- | The initial profunctor has no elements anywhere.
instance (CategoryOf j, CategoryOf k) => Finitary (InitialProfunctor :: j +-> k) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size = Natural
0
  toIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
InitialProfunctor a b -> Natural
toIndex = \case {}
  fromIndex :: forall (a :: k) (b :: j).
(Ob a, Ob b) =>
Natural -> InitialProfunctor a b
fromIndex Natural
_ = [Char] -> InitialProfunctor a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"fromIndex: the initial profunctor has no elements"

-- | The indices of @p@ first, then those of @q@.
instance (Finitary p, Finitary q) => Finitary (p :+: q) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = 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 -> Natural
forall a. Num a => a -> a -> a
+ 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
  toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => (:+:) p q a b -> Natural
toIndex @a @b = \case
    InjL p a b
x -> 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
    InjR q a b
y -> 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 -> Natural
forall a. Num a => a -> a -> a
+ 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
y
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> (:+:) p q a b
fromIndex @a @b Natural
i = if Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< 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 then p a b -> (:+:) p q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL (Natural -> p a b
forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex Natural
i) else q a b -> (:+:) p q a b
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR (Natural -> q a b
forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> q a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
Natural -> p a b
fromIndex (Natural
i Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- 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))

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) where
  factorize :: forall (a :: FINITARY j k) (b :: FINITARY j k).
(a ~> b) -> (:.:) (Hom (FINITARY j k)) (Hom (FINITARY j k)) a b
factorize = (a ~> b) -> (:.:) (Hom (FINITARY j k)) (Hom (FINITARY j k)) a b
forall k (a :: k) (b :: k).
(HasPushouts k, HasEqualizers k) =>
(a ~> b) -> (:.:) (Hom k) (Hom k) a b
defaultFactorize

-- * Ends by enumeration

-- | A finite category: finitely many objects, and finitely many arrows between them. The first is
-- 'Enumerable', the second does not follow from it, and the ends below need both.
class (Enumerable k, Finitary (Hom k)) => FiniteCat k

instance (Enumerable k, Finitary (Hom k)) => FiniteCat k

-- | One point of the domain of an end at @a@\/@b@, as a key into a tabulated family: an object
-- pair and, there, an arrow into @a@, an arrow out of @b@ and an element of @p@.
type EndKey = (Natural, Natural, Natural, Natural, Natural)

-- | Visit every point of that domain, in one fixed order. Everything that tabulates or reads a
-- family walks it with this, so that a family is a list of values in this order.
endDomain
  :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r
   . (Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => (forall c d. (Ob c, Ob d) => c ~> a -> b ~> d -> p c d -> r)
  -> [r]
endDomain :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain forall (c :: k) (d :: j).
(Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> r
f =
  forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @c ->
    forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @d ->
      -- Bound outside the comprehension so that each is enumerated once, not once per outer choice.
      let cas :: [Hom k a a]
cas = 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; bds :: [Hom j b a]
bds = 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; 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 @c @d
      in [Hom k a a -> Hom j b a -> p a a -> r
forall (c :: k) (d :: j).
(Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> r
f Hom k a a
ca Hom j b a
bd p a a
x | Hom k a a
ca <- [Hom k a a]
cas, Hom j b a
bd <- [Hom j b a]
bds, p a a
x <- [p a a]
xs]

endKey
  :: forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) a b
   . (FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d)
  => c ~> a -> b ~> d -> p c d -> EndKey
endKey :: forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey c ~> a
ca b ~> d
bd p c d
x = c ~> a
ca (c ~> a) -> ((Ob c, Ob a) => EndKey) -> EndKey
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) => EndKey) -> EndKey
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (forall (a :: k). (Enumerable k, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @c, forall (a :: j). (Enumerable j, Ob a) => Natural
forall {k} (a :: k). (Enumerable k, Ob a) => Natural
objIndex @d, (c ~> a) -> Natural
forall (a :: k) (b :: k). (Ob a, Ob b) => (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
ca, (b ~> d) -> Natural
forall (a :: j) (b :: j). (Ob a, Ob b) => (a ~> b) -> Natural
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
p a b -> Natural
toIndex b ~> d
bd, p c d -> 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 c d
x)

-- | Where each key sits in a tabulated family.
endPositions
  :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j)
   . (Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => M.Map EndKey P.Int
endPositions :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map EndKey Int
endPositions = [(EndKey, Int)] -> Map EndKey Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([EndKey] -> [Int] -> [(EndKey, Int)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @p @a @b @EndKey (c ~> a) -> (b ~> d) -> p c d -> EndKey
forall (c :: k) (d :: j).
(Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey) [Int
Item [Int]
0 ..])

-- | The naturality conditions on a family: at each pair of arrows @g@, @h@, the point a given point
-- is carried to, and the transport of @q@\'s indices that the family must commute with. The
-- transport is a table rather than a function, so that @q@ is enumerated once per condition.
endLaws
  :: 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)
  => [(EndKey, EndKey, [Natural])]
endLaws :: 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) =>
[(EndKey, EndKey, [Natural])]
endLaws =
  forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @c ->
    forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @d ->
      forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @k \ @c' ->
        forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @d' ->
          let gs :: [Hom k a a]
gs = 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' @c
              hs :: [Hom j a a]
hs = 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) @d @d'
              cas :: [Hom k a a]
cas = 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
              bds :: [Hom j b a]
bds = 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
              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 @c @d
          in [ (Hom k a a -> Hom j b a -> p a a -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey Hom k a a
ca Hom j b a
bd p a a
x, (a ~> a) -> (b ~> a) -> p a a -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey (Hom k a a
ca Hom k a a -> Hom k a a -> 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
. Hom k a a
g) (Hom j a a
h Hom j a a -> Hom j b a -> b ~> a
forall (b :: j) (c :: j) (a :: j). (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
. Hom j b a
bd) (Hom k a a -> Hom j a a -> p a a -> p a a
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 Hom k a a
g Hom j a a
h p a a
x), (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
. Hom k a a -> Hom j a a -> q a a -> q a a
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> q a b -> q 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 Hom k a a
g Hom j 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 +-> k) (a :: k) (b :: j).
(Finitary p, Ob a, Ob b) =>
[p a b]
elements @q @c @d))
             | Hom k a a
g <- [Hom k a a]
gs
             , Hom j a a
h <- [Hom j a a]
hs
             , Hom k a a
ca <- [Hom k a a]
cas
             , Hom j b a
bd <- [Hom j b a]
bds
             , p a a
x <- [p a a]
xs
             ]

-- | Enumerate an end by brute force: every way of choosing a value at each point of the domain,
-- kept when it satisfies every condition. The candidate space is the product of the choices over
-- the whole domain, so this is only ever run on small categories.
endElements :: [[v]] -> [(P.Int, P.Int, v -> v -> P.Bool)] -> [[v]]
endElements :: forall v. [[v]] -> [(Int, Int, v -> v -> Bool)] -> [[v]]
endElements [[v]]
choices [(Int, Int, v -> v -> Bool)]
laws = ([v] -> Bool) -> [[v]] -> [[v]]
forall a. (a -> Bool) -> [a] -> [a]
P.filter [v] -> Bool
ok ([[v]] -> [[v]]
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: Type -> Type) a. Monad m => [m a] -> m [a]
P.sequence [[v]]
choices)
  where
    ok :: [v] -> Bool
ok [v]
t = ((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 ([v] -> Int -> v
forall i a. Integral i => [a] -> i -> a
genericIndex [v]
t Int
src) ([v] -> Int -> v
forall i a. Integral i => [a] -> i -> a
genericIndex [v]
t Int
tgt)) [(Int, Int, v -> v -> Bool)]
laws

-- | Every natural family, as its list of @q@-indices in 'endDomain' order.
expElements
  :: 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)
  => [[Natural]]
expElements :: 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) =>
[[Natural]]
expElements =
  [[Natural]]
-> [(Int, Int, Natural -> Natural -> Bool)] -> [[Natural]]
forall v. [[v]] -> [(Int, Int, v -> v -> Bool)] -> [[v]]
endElements
    (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @p @a @b \ @c @d c ~> a
_ b ~> d
_ p c d
_ -> 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 @c @d))
    [(EndKey -> Int
at EndKey
src, EndKey -> Int
at EndKey
tgt, \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) | (EndKey
src, EndKey
tgt, [Natural]
tr) <- 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) =>
[(EndKey, EndKey, [Natural])]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[(EndKey, EndKey, [Natural])]
endLaws @p @q @a @b]
  where
    at :: EndKey -> Int
at = (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map EndKey Int
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map EndKey Int
endPositions @p @a @b Map EndKey Int -> EndKey -> Int
forall k a. Ord k => Map k a -> k -> a
M.!)

-- | Read a tabulated family back as a function on the keys.
atKey
  :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) v
   . (Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => [v] -> EndKey -> v
atKey :: forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
atKey [v]
row = ([(EndKey, v)] -> Map EndKey v
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([EndKey] -> [v] -> [(EndKey, v)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @p @a @b @EndKey (c ~> a) -> (b ~> d) -> p c d -> EndKey
forall (c :: k) (d :: j).
(Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey) [v]
row) Map EndKey v -> EndKey -> v
forall k a. Ord k => Map k a -> k -> a
M.!)

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

-- | The internal hom of finitary profunctors is finitary: its elements are the natural families,
-- 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) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Natural]]
expElements @p @q @a @b)
  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) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @p @a @b \c ~> a
ca b ~> d
bd p c d
x -> q c d -> 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 ((c ~> a) -> (b ~> d) -> p c d -> q c d
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> p c d -> q c d
f c ~> a
ca b ~> d
bd p c d
x))
    where
      es :: [[Natural]]
es = 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) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Natural]]
expElements @p @q @a @b
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> (:~>:) p q a b
fromIndex @a @b Natural
i =
    let at :: EndKey -> Natural
at = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
forall (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
atKey @p @a @b ([[Natural]] -> Natural -> [Natural]
forall i a. Integral i => [a] -> i -> a
genericIndex (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) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Natural]]
expElements @p @q @a @b) Natural
i)
    in (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 (EndKey -> Natural
at ((c ~> a) -> (b ~> d) -> p c d -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey c ~> a
ca b ~> d
bd p c d
x))
  elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [(:~>:) p q a b]
elements @a @b =
    ([Natural] -> (:~>:) p q a b) -> [[Natural]] -> [(:~>:) p q a b]
forall a b. (a -> b) -> [a] -> [b]
P.map
      (\[Natural]
row -> let at :: EndKey -> Natural
at = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
forall (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
atKey @p @a @b [Natural]
row in (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 (EndKey -> Natural
at ((c ~> a) -> (b ~> d) -> p c d -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey c ~> a
ca b ~> d
bd p c d
x)))
      (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) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[[Natural]]
expElements @p @q @a @b)

-- | 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, as the points of the representable it contains, in 'endDomain' order: all subsets,
-- kept when closed. The representable at @a@\/@b@ is the domain of the end at the terminal object,
-- and the closure conditions are that end's naturality conditions read as implications.
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]]
endElements
    (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @TerminalProfunctor @a @b \c ~> a
_ b ~> d
_ TerminalProfunctor c d
_ -> [Bool
Item [Bool]
P.False, Bool
Item [Bool]
P.True])
    [(EndKey -> Int
at EndKey
src, EndKey -> Int
at EndKey
tgt, \Bool
s Bool
t -> Bool -> Bool
P.not Bool
s Bool -> Bool -> Bool
P.|| Bool
t) | (EndKey
src, EndKey
tgt, [Natural]
_) <- 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) =>
[(EndKey, EndKey, [Natural])]
forall (p :: j +-> k) (q :: j +-> k) (a :: k) (b :: j).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[(EndKey, EndKey, [Natural])]
endLaws @TerminalProfunctor @TerminalProfunctor @a @b]
  where
    at :: EndKey -> Int
at = (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map EndKey Int
forall (p :: j +-> k) (a :: k) (b :: j).
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Map EndKey Int
endPositions @TerminalProfunctor @a @b Map EndKey Int -> EndKey -> Int
forall k a. Ord k => Map k a -> k -> a
M.!)

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 = \(Sieve forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s) -> [Char] -> [[Bool]] -> [Bool] -> Natural
forall v. Eq v => [Char] -> [[v]] -> [v] -> Natural
familyIndex [Char]
"toIndex: not a sieve" [[Bool]]
es (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
forall (p :: j +-> k) (a :: k) (b :: j) r.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
(forall (c :: k) (d :: j).
 (Ob c, Ob d) =>
 (c ~> a) -> (b ~> d) -> p c d -> r)
-> [r]
endDomain @TerminalProfunctor @a @b \c ~> a
ca b ~> d
bd TerminalProfunctor c d
_ -> (c ~> a) -> (b ~> d) -> Bool
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s c ~> a
ca b ~> d
bd)
    where
      es :: [[Bool]]
es = 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
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> Sieve a b
fromIndex @a @b Natural
i = [Bool] -> Sieve a b
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[Bool] -> Sieve a b
sieveAt ([[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 = ([Bool] -> Sieve a b) -> [[Bool]] -> [Sieve a b]
forall a b. (a -> b) -> [a] -> [b]
P.map [Bool] -> Sieve a b
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[Bool] -> Sieve a b
sieveAt (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) => [P.Bool] -> Sieve a b
sieveAt :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[Bool] -> Sieve a b
sieveAt [Bool]
row =
  let at :: EndKey -> Bool
at = forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
forall (p :: j +-> k) (a :: k) (b :: j) v.
(Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
[v] -> EndKey -> v
atKey @TerminalProfunctor @a @b [Bool]
row
  in (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
// EndKey -> Bool
at ((c ~> a) -> (b ~> d) -> TerminalProfunctor c d -> EndKey
forall {j} {k} (c :: k) (d :: j) (p :: j +-> k) (a :: k) (b :: j).
(FiniteCat j, FiniteCat k, Finitary p, Ob c, Ob d) =>
(c ~> a) -> (b ~> d) -> p c d -> EndKey
endKey c ~> a
ca b ~> d
bd TerminalProfunctor c d
forall {j} {k} (a :: j) (b :: k).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
TerminalProfunctor a b
TerminalProfunctor)

-- | 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 -> (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
_ b ~> d
_ -> Bool
P.True))
  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))