{-# LANGUAGE AllowAmbiguousTypes #-}
-- The instances on 'SHEAVES' are orphans for the reason "Proarrow.Category.Enriched.Finitary.Topos"
-- gives for its own: the kind is 'SUBCAT' of a predicate, and both come from other modules.
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Sheaves on a finite site, decided by enumeration.
--
-- A cover of @a@ generates a 'Sieve' ('generatedSieve'), and a matching family for that cover is
-- exactly a natural transformation out of the sieve -- which over finitary profunctors is a finite
-- thing you can list. So the sheaf condition becomes a comparison of two finite lists ('sheafAt'):
-- restrict each element at @a@ to get one table per element, enumerate the matching families to get
-- the other list, and check the two agree as multisets. Comparing only their /lengths/ is not
-- enough: @Props.Sheaf@'s @Collapse@ has as many elements as matching families and is still not a
-- sheaf.
--
-- The same coverage is a Lawvere–Tierney topology on the topos. 'closure' sends a sieve to the pairs
-- @(g, h)@ along which it pulls back to a covering one, and 'lawvereTierney' packages that as an
-- arrow on 'Omega'.
--
-- The topology also has a /sheafification/, 'Sheafify', with its unit and universal property --
-- computed rather than postulated, so it is one more thing that can be enumerated and compared.
module Proarrow.Category.Enriched.Finitary.Sheaf where

import Data.Kind (Type)
import Data.List (find, genericIndex, genericLength, sort)
import Data.Map.Strict qualified as M
import Data.Maybe (fromMaybe, isJust, listToMaybe, mapMaybe)
import Numeric.Natural (Natural)
import Prelude (type (~))
import Prelude qualified as P

import Proarrow.Category.Enriched.Finitary
  ( Finitary (..)
  , FiniteCat
  , LocallyFinite
  , factorThrough
  , factorsThrough
  , foreachOb
  )
import Proarrow.Category.Enriched.Finitary.Topos
  ( FINITARY
  , KnownTables
  , Tabulated
  , equalizeNat
  , factorThroughEqualizer
  , fromTabulated
  , natDomain
  , natElements
  , natIndex
  , natKey
  , natPositionsBy
  , natTable
  , sieveTable
  , toTabulated
  , withSubobject
  , withTables
  )
import Proarrow.Category.Enriched.Thin (Enumerable)
import Proarrow.Category.Instance.Opposite (OPPOSITE (..))
import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Instance.Sub (SUBCAT (..), Sub (..))
import Proarrow.Category.Sheaf (HasFiniteCovers (..), Sheaf (..), Site (..), SomeCover (..), SomeLeg (..))
import Proarrow.Category.Topos (HasSubobjectClassifier (..))
import Proarrow.Core
  ( CategoryOf (..)
  , OB
  , Profunctor (..)
  , Promonad (..)
  , UN
  , (//)
  , (\\)
  , type (+->)
  , type (:&&:)
  , type (:~>)
  )
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), PROD (..), Prod (..))
import Proarrow.Limit.Equalizer (HasEqualizers (..))
import Proarrow.Limit.Pullback (HasPullbacks)
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Instance.Sieve (Sieve (..), maximalSieve, sieveMeet)
import Proarrow.Profunctor.Instance.Terminal (TerminalProfunctor (..))
import Proarrow.Profunctor.Instance.Yoneda (Yo (..))

-- | The sieve a cover generates at @(a, b)@: the arrows into @a@ that factor through a leg,
-- paired with every arrow out of @b@.
generatedSieve
  :: forall t {j} {k} (a :: k) (b :: j) c
   . (Site t k, LocallyFinite k, CategoryOf j, Ob a, Ob b)
  => Cover t k a c
  -> Sieve a b
generatedSieve :: forall t {j} {k} (a :: k) (b :: j) c.
(Site t k, LocallyFinite k, CategoryOf j, Ob a, Ob b) =>
Cover t k a c -> Sieve a b
generatedSieve Cover t k a c
c = (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
_ -> (SomeLeg t k a c -> Bool) -> [SomeLeg t k a c] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
P.any (\(SomeLeg Leg t k a c x
l) -> let f :: x ~> a
f = Leg t k a c x -> x ~> a
forall (a :: k) c (x :: k). Leg t k a c x -> x ~> a
forall t k (a :: k) c (x :: k). Site t k => Leg t k a c x -> x ~> a
legArrow Leg t k a c x
l in (c ~> a) -> (x ~> a) -> Bool
forall {k} (x :: k) (y :: k) (a :: k).
(LocallyFinite k, Ob x, Ob y, Ob a) =>
(x ~> a) -> (y ~> a) -> Bool
factorsThrough c ~> a
g x ~> a
f ((Ob x, Ob a) => Bool) -> (x ~> a) -> Bool
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ x ~> a
f ((Ob c, Ob a) => Bool) -> (c ~> a) -> Bool
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
g) (Cover t k a c -> [SomeLeg t k a c]
forall (a :: k) c. Cover t k a c -> [SomeLeg t k a c]
forall t k (a :: k) c.
Site t k =>
Cover t k a c -> [SomeLeg t k a c]
legs Cover t k a c
c)

-- | Whether a sieve is the maximal one -- every arrow of the category is in it.
isMaximal :: forall {j} {k} (a :: k) (b :: j). (FiniteCat j, FiniteCat k) => Sieve a b -> P.Bool
isMaximal :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isMaximal Sieve a b
s = [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and (Sieve a b -> [Bool]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> [Bool]
sieveTable Sieve a b
s)

-- | Whether every point of the second sieve is a point of the first.
contains :: forall {j} {k} (a :: k) (b :: j). (FiniteCat j, FiniteCat k) => Sieve a b -> Sieve a b -> P.Bool
contains :: forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> Sieve a b -> Bool
contains Sieve a b
s = \Sieve a b
s' -> [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and ((Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
P.zipWith (\Bool
x Bool
y -> Bool -> Bool
P.not Bool
y Bool -> Bool -> Bool
P.|| Bool
x) [Bool]
ts (Sieve a b -> [Bool]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> [Bool]
sieveTable Sieve a b
s'))
  where
    -- tabulated before the second sieve arrives, so a partial application tabulates @s@ once
    ts :: [Bool]
ts = Sieve a b -> [Bool]
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> [Bool]
sieveTable Sieve a b
s

-- | Whether a sieve is covering: either it is the maximal sieve, or it contains the sieve that some
-- cover of its object generates -- which, a sieve being closed under composition, is to contain
-- that cover's legs ('coveringCover').
--
-- That is the coverage taken at face value. It agrees with the Grothendieck topology the coverage
-- generates only when the covers are stable and compose. When they do not, 'closure' stops being
-- idempotent, and 'Proarrow.Testing.Laws.testLawvereTierney' is where that shows up.
isCovering
  :: forall t {j} {k} (a :: k) (b :: j)
   . (HasFiniteCovers t k, FiniteCat j, FiniteCat k)
  => Sieve a b
  -> P.Bool
isCovering :: forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isCovering Sieve a b
s = Sieve a b -> Bool
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isMaximal Sieve a b
s Bool -> Bool -> Bool
P.|| Maybe (SomeCover t k a) -> Bool
forall a. Maybe a -> Bool
isJust (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, CategoryOf j) =>
Sieve a b -> Maybe (SomeCover t k a)
coveringCover @t Sieve a b
s)

-- | The first listed cover all of whose legs lie in the sieve, if there is one. This is the search
-- 'isCovering' makes and the one 'extendPlus' needs, and it needs no tabulation: whether a sieve
-- contains the legs at the identity decides whether it contains everything they generate.
--
-- So it trusts the closure "Proarrow.Profunctor.Instance.Sieve" does not enforce: on a hand-built
-- predicate that is not a sieve it says yes where comparing the whole generated sieve says no.
coveringCover
  :: forall t {j} {k} (a :: k) (b :: j)
   . (HasFiniteCovers t k, CategoryOf j)
  => Sieve a b
  -> P.Maybe (SomeCover t k a)
coveringCover :: forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, CategoryOf j) =>
Sieve a b -> Maybe (SomeCover t k a)
coveringCover (Sieve forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s) = (SomeCover t k a -> Bool)
-> [SomeCover t k a] -> Maybe (SomeCover t k a)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\(SomeCover Cover t k a c
c) -> (SomeLeg t k a c -> Bool) -> [SomeLeg t k a c] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
P.all (\(SomeLeg Leg t k a c x
l) -> (x ~> a) -> (b ~> b) -> Bool
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s (Leg t k a c x -> x ~> a
forall (a :: k) c (x :: k). Leg t k a c x -> x ~> a
forall t k (a :: k) c (x :: k). Site t k => Leg t k a c x -> x ~> a
legArrow Leg t k a c x
l) b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) (Cover t k a c -> [SomeLeg t k a c]
forall (a :: k) c. Cover t k a c -> [SomeLeg t k a c]
forall t k (a :: k) c.
Site t k =>
Cover t k a c -> [SomeLeg t k a c]
legs Cover t k a c
c)) (forall t k (a :: k).
(HasFiniteCovers t k, Ob a) =>
[SomeCover t k a]
covers @t @k @a)

-- | The Lawvere–Tierney closure of a sieve: the pairs @(g, h)@ along which it pulls back to a
-- covering one. A sieve is covering exactly when its closure is the maximal sieve.
--
-- Note /both/ components -- @'dimap' g h@, not just @'lmap' g@. A coverage constrains only the
-- contravariant side, but a sieve over @j '+->' k@ has two, which is why @Props.Sheaf@ checks this
-- function's naturality at a non-trivial @j@.
closure
  :: forall t {j} {k} (a :: k) (b :: j)
   . (HasFiniteCovers t k, FiniteCat j, FiniteCat k)
  => Sieve a b
  -> Sieve a b
closure :: forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Sieve a b
closure s :: Sieve a b
s@Sieve{} = (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 -> forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isCovering @t ((c ~> a) -> (b ~> d) -> Sieve a b -> Sieve c d
forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Sieve a b -> Sieve 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 Sieve a b
s) ((Ob c, Ob a) => Bool) -> (c ~> a) -> Bool
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (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
\\ c ~> a
g ((Ob b, Ob d) => Bool) -> (b ~> d) -> Bool
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (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
\\ b ~> d
h

-- | The coverage as a Lawvere–Tierney topology on the topos of finitary profunctors: 'closure', as
-- an arrow on the subobject classifier.
lawvereTierney
  :: forall t j k. (HasFiniteCovers t k, FiniteCat j, FiniteCat k) => (Omega :: PROD (FINITARY j k)) ~> Omega
lawvereTierney :: forall t j k.
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Omega ~> Omega
lawvereTierney = Sub Prof (SUB Sieve) (SUB Sieve)
-> Prod (Sub Prof) (PR (SUB Sieve)) (PR (SUB Sieve))
forall {j} {k} (p :: j +-> k) (a1 :: k) (b1 :: j).
p a1 b1 -> Prod p (PR a1) (PR b1)
Prod (Prof Sieve Sieve -> Sub Prof (SUB Sieve) (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 ((Sieve :~> Sieve) -> Prof Sieve Sieve
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \s :: Sieve a b
s@Sieve{} -> forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Sieve a b
closure @t Sieve a b
s))

-- | Whether a finitary profunctor is a sheaf for the coverage: at every pair of objects and every
-- cover, restriction is a bijection from the elements at the covered object to the matching
-- families on the sieve the cover generates.
isSheaf
  :: forall t {j} {k} (p :: j +-> k)
   . (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k)
  => P.Bool
isSheaf :: forall t {j} {k} (p :: j +-> k).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) =>
Bool
isSheaf =
  [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 ->
        let cs :: [SomeCover t k a]
cs = forall t k (a :: k).
(HasFiniteCovers t k, Ob a) =>
[SomeCover t k a]
covers @t @k @a -- does not depend on @b@, so bound outside the inner walk
        in forall k r. Enumerable k => (forall (a :: k). Ob a => [r]) -> [r]
foreachOb @j \ @b -> [forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j) c.
(Site t k, Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Cover t k a c -> Bool
sheafAt @t @p @a @b Cover t k a c
c | SomeCover Cover t k a c
c <- [SomeCover t k a]
cs]
    )

-- | The sheaf condition at one cover: the restrictions of the elements at the covered object are
-- exactly the matching families on the sieve it generates, as multisets.
sheafAt
  :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j) c
   . (Site t k, Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => Cover t k a c
  -> P.Bool
sheafAt :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j) c.
(Site t k, Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Cover t k a c -> Bool
sheafAt Cover t k a c
c = Sieve a b
-> (forall (q :: j +-> k).
    Finitary q =>
    (q :~> Yo a (OP b)) -> Bool)
-> Bool
forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (forall t {j} {k} (a :: k) (b :: j) c.
(Site t k, LocallyFinite k, CategoryOf j, Ob a, Ob b) =>
Cover t k a c -> Sieve a b
generatedSieve @t @a @b Cover t k a c
c) \ @q q :~> Yo a (OP b)
incl ->
  [[Natural]] -> [[Natural]]
forall a. Ord a => [a] -> [a]
sort [forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
natTable @q @p (\q a b
y -> case q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl q a b
y of Yo a ~> a
g b1 ~> b
h -> (a ~> a) -> (b ~> b) -> p a b -> p a b
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 a ~> a
g b ~> b
b1 ~> b
h 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]
    [[Natural]] -> [[Natural]] -> Bool
forall a. Eq a => a -> a -> Bool
P.== [[Natural]] -> [[Natural]]
forall a. Ord a => [a] -> [a]
sort (forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @q @p)

-- | Present a finitary profunctor by its tables, as
-- 'Proarrow.Category.Enriched.Finitary.Topos.withTabulated' does, and tag the presentation with the
-- coverage -- which is to give it a 'Sheaf' instance. What that instance asserts is decided here,
-- by 'isSheaf', so the assertion is backed by an enumeration and not by the caller\'s word; the
-- failure continuation is taken when the profunctor is no sheaf for @t@.
--
-- This is how a sheaf with no 'Sheaf' instance of its own -- a representable, a sheafification --
-- becomes an object of 'SHEAVES'. It is also the cheap way to be one: the condition is decided on
-- the tables rather than on @p@, where a 'Sheafify' answers a single 'toIndex' by re-running the
-- whole plus construction.
withTabulatedSheaf
  :: forall t {j} {k} (p :: j +-> k) r
   . (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k)
  => ( forall {lm} {rm} (tab :: j +-> k)
        . (tab ~ Tabulated t lm rm, KnownTables j k lm rm, Sheaf t tab)
       => (p :~> tab)
       -> (tab :~> p)
       -> r
     )
  -> r
  -> r
withTabulatedSheaf :: forall t {j} {k} (p :: j +-> k) r.
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) =>
(forall {lm :: [[[[Nat]]]]} {rm :: [[[[Nat]]]]} (tab :: j +-> k).
 (tab ~ Tabulated t lm rm, KnownTables j k lm rm, Sheaf t tab) =>
 (p :~> tab) -> (tab :~> p) -> r)
-> r -> r
withTabulatedSheaf forall {lm :: [[[[Nat]]]]} {rm :: [[[[Nat]]]]} (tab :: j +-> k).
(tab ~ Tabulated t lm rm, KnownTables j k lm rm, Sheaf t tab) =>
(p :~> tab) -> (tab :~> p) -> r
ok r
notSheaf = forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (lm :: [[[[Nat]]]]) (rm :: [[[[Nat]]]]).
 KnownTables j k lm rm =>
 r)
-> r
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (lm :: [[[[Nat]]]]) (rm :: [[[[Nat]]]]).
 KnownTables j k lm rm =>
 r)
-> r
withTables @p \ @lm @rm ->
  if forall t {j} {k} (p :: j +-> k).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) =>
Bool
isSheaf @t @(Tabulated t lm rm :: j +-> k)
    then forall {lm :: [[[[Nat]]]]} {rm :: [[[[Nat]]]]} (tab :: j +-> k).
(tab ~ Tabulated t lm rm, KnownTables j k lm rm, Sheaf t tab) =>
(p :~> tab) -> (tab :~> p) -> r
forall (tab :: j +-> k).
(tab ~ Tabulated t lm rm, KnownTables j k lm rm, Sheaf t tab) =>
(p :~> tab) -> (tab :~> p) -> r
ok @(Tabulated t lm rm) p a b -> Tabulated t lm rm a b
p :~> Tabulated t lm rm
forall {j} {k} t (lm :: [[[[Nat]]]]) (rm :: [[[[Nat]]]])
       (p :: j +-> k).
Finitary p =>
p :~> Tabulated t lm rm
toTabulated Tabulated t lm rm a b -> p a b
Tabulated t lm rm :~> p
forall {j} {k} t (lm :: [[[[Nat]]]]) (rm :: [[[[Nat]]]])
       (p :: j +-> k).
Finitary p =>
Tabulated t lm rm :~> p
fromTabulated
    else r
notSheaf

-- | A sieve as a subobject of the representable, handed on with its inclusion: the natural
-- transformations out of that subobject are exactly the matching families on the sieve, with no
-- separate treatment of the points outside it and no argument about which naturality conditions
-- may be dropped. This is the one notion of matching family in the module; 'sheafAt' and 'Plus'
-- both go through it.
--
-- 'withSubobject' checks the closure a sieve must have, and its failure branch is unreachable for
-- any coverage, lawful or not: 'generatedSieve'\'s membership ignores its covariant argument and
-- is closed under precomposition, and 'leastDenseSieve' is a meet of sieves. Reaching it would take
-- a 'Finitary' instance on the hom-profunctor whose 'elements' omits an arrow, which
-- 'Proarrow.Testing.Laws.testFinitary' rules out.
withSieve
  :: forall {j} {k} (a :: k) (b :: j) r
   . (FiniteCat j, FiniteCat k)
  => Sieve a b
  -> (forall q. (Finitary q) => (q :~> Yo a (OP b)) -> r)
  -> r
withSieve :: forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (Sieve forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s) forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r
k =
  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
forall (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 @(Yo a (OP b))
    (\(Yo a ~> a
g b1 ~> b
h) -> (a ~> a) -> (b ~> b) -> Bool
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Bool
s a ~> a
g b ~> b
b1 ~> b
h)
    (\ @q (Sub (Prof q :~> Yo a (OP b)
incl)) -> forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r
k @q q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl)
    ([Char] -> r
forall a. HasCallStack => [Char] -> a
P.error [Char]
"withSieve: not a sieve")

-- * Sheafification

-- | One step of the plus construction for the topology @t@. An element at @(a, b)@ is a matching
-- family on a dense sieve, taken up to agreement on a dense sieve; a 'Plus' value holds one such
-- family, as a partial function whose support is its sieve -- the sieve is never stored separately
-- and so cannot disagree with the family. On a finite site whose coverage is a Grothendieck topology
-- the dense sieves have a least one, 'leastDenseSieve', and every element has exactly one family on
-- it: so the element a value stands for is its restriction to that sieve, 'plusTable', and that is
-- what 'Finitary' numbers and "Proarrow.Testing" compares. Nothing has to be quotiented.
--
-- That is 'HasFiniteCovers'\'s Composition law, and 'leastDenseSieve' fails loudly rather than
-- compute where it does not hold.
--
-- __The constructor checks none of__: that the support is a sieve, that it is dense, that the
-- family is matching -- as 'Sieve'\'s does not check closure. 'plusElements' builds only lawful
-- values; one built by hand is its builder's responsibility.
type Plus :: forall {j} {k}. Type -> j +-> k -> j +-> k
data Plus t p a b where
  Plus :: (Ob a, Ob b) => (forall c d. c ~> a -> b ~> d -> P.Maybe (p c d)) -> Plus t p a b

instance (CategoryOf j, CategoryOf k) => Profunctor (Plus t p :: j +-> k) where
  dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> Plus t p a b -> Plus t p c d
dimap c ~> a
l b ~> d
r (Plus forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f) = c ~> a
l (c ~> a) -> ((Ob c, Ob a) => Plus t p c d) -> Plus t p 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
r (b ~> d) -> ((Ob b, Ob d) => Plus t p c d) -> Plus t p 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 (c :: k) (d :: j). (c ~> c) -> (d ~> d) -> Maybe (p c d))
-> Plus t p c d
forall {k} {j} (a :: k) (b :: j) (p :: j +-> k) t.
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
Plus \c ~> c
g d ~> d
h -> (c ~> a) -> (b ~> d) -> Maybe (p c d)
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f (c ~> a
l (c ~> a) -> (c ~> c) -> c ~> 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
. c ~> c
g) (d ~> d
h (d ~> d) -> (b ~> d) -> b ~> d
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
. b ~> d
r)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: j) r.
((Ob a, Ob b) => r) -> Plus t p a b -> r
\\ Plus{} = r
(Ob a, Ob b) => r
r

-- | The sieve a value is defined on.
support :: Plus t p :~> Sieve
support :: forall {k1} {k} t (p :: k1 +-> k) (a :: k) (b :: k1).
Plus t p a b -> Sieve a b
support (Plus forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f) = (forall (c :: k) (d :: k1). (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 -> Maybe (p c d) -> Bool
forall a. Maybe a -> Bool
isJust ((c ~> a) -> (b ~> d) -> Maybe (p c d)
forall (c :: k) (d :: k1). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f c ~> a
g b ~> d
h)

-- | Whether a sieve is dense for the topology: its 'closure' is the maximal sieve. On a lawful
-- coverage this agrees with 'isCovering' -- 'Proarrow.Testing.Laws.testDenseIsCovering' checks
-- that -- but it is the stable notion, and 'Plus' needs stability, since 'dimap' pulls a support
-- back along arrows.
isDense
  :: forall t {j} {k} (a :: k) (b :: j)
   . (HasFiniteCovers t k, FiniteCat j, FiniteCat k)
  => Sieve a b
  -> P.Bool
isDense :: forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isDense Sieve a b
s = Sieve a b -> Bool
forall {j} {k} (a :: k) (b :: j).
(FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isMaximal (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Sieve a b
closure @t Sieve a b
s)

-- | The meet of all the dense sieves at a pair of objects, and so the least dense sieve -- when
-- the covers compose, since that is what makes 'closure' preserve meets. Restriction to it is what
-- picks one matching family out of each element of 'Plus'. On a coverage whose covers pull back but
-- do not compose the meet need not be dense, and this errors, naming the law that failed, rather
-- than let 'Plus' compute on it: a poset @w ≤ x ≤ a@, @w ≤ y ≤ a@ with @a@ covered by @x@ and by
-- @y@ separately and each of those by @w@ is the smallest example.
leastDenseSieve
  :: forall t {j} {k} (a :: k) (b :: j)
   . (HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => Sieve a b
leastDenseSieve :: forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Sieve a b
leastDenseSieve
  | forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isDense @t Sieve a b
s = Sieve a b
s
  | Bool
P.otherwise = [Char] -> Sieve a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"leastDenseSieve: the dense sieves have no least one -- the covers do not compose"
  where
    s :: Sieve a b
s = (Sieve a b -> Sieve a b -> Sieve a b)
-> Sieve a b -> [Sieve a b] -> Sieve a b
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 Sieve a b -> Sieve a b -> Sieve a b
forall {k} {j} (a :: k) (b :: j).
Sieve a b -> Sieve a b -> Sieve a b
sieveMeet Sieve a b
forall {j} {k} (a :: k) (b :: j).
(CategoryOf j, CategoryOf k, Ob a, Ob b) =>
Sieve a b
maximalSieve ((Sieve a b -> Bool) -> [Sieve a b] -> [Sieve a b]
forall a. (a -> Bool) -> [a] -> [a]
P.filter (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k) =>
Sieve a b -> Bool
isDense @t) (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 @(Sieve :: j +-> k) @a @b))

-- | The elements of 'Plus' at a pair of objects: the matching families on the least dense sieve, in
-- the order 'natElements' lists them.
plusElements
  :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j)
   . (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k, Ob a, Ob b)
  => [Plus t p a b]
plusElements :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k, Ob a,
 Ob b) =>
[Plus t p a b]
plusElements = Sieve a b
-> (forall (q :: j +-> k).
    Finitary q =>
    (q :~> Yo a (OP b)) -> [Plus t p a b])
-> [Plus t p a b]
forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Sieve a b
leastDenseSieve @t @a @b) \ @q q :~> Yo a (OP b)
incl ->
  -- the sieve's points as points of the representable, at the positions a row lists them
  let pos :: Map NatKey Int
pos = forall {j} {k} (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> NatKey)
-> Map NatKey Int
forall (p :: j +-> k).
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> NatKey)
-> Map NatKey Int
natPositionsBy @q \q a b
y -> Yo a (OP b) a b -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey (q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl q a b
y)
  in [ (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
forall {k} {j} (a :: k) (b :: j) (p :: j +-> k) t.
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
Plus \c ~> a
g b ~> d
h -> c ~> a
g (c ~> a) -> ((Ob c, Ob a) => Maybe (p c d)) -> Maybe (p 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
h (b ~> d) -> ((Ob b, Ob d) => Maybe (p c d)) -> Maybe (p c d)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) r.
Profunctor p =>
p a b -> ((Ob a, Ob b) => r) -> r
// (Int -> p c d) -> Maybe Int -> Maybe (p c d)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (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 -> p c d) -> (Int -> Natural) -> Int -> p c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
P.. ([Natural]
row [Natural] -> Int -> Natural
forall a. HasCallStack => [a] -> Int -> a
P.!!)) (NatKey -> Map NatKey Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Yo a (OP b) c d -> NatKey
forall {j} {k} (a :: k) (b :: j) (p :: j +-> k).
(FiniteCat j, FiniteCat k, Finitary p, Ob a, Ob b) =>
p a b -> NatKey
natKey ((c ~> a) -> (b ~> d) -> Yo a (OP b) c d
forall {k} {j} (c :: k) (a :: k) (b1 :: j) (d :: j).
(c ~> a) -> (b1 ~> d) -> Yo a (OP b1) c d
Yo c ~> a
g b ~> d
h)) Map NatKey Int
pos)
     | [Natural]
row <- forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[[Natural]]
natElements @q @p
     ]

-- | A value restricted to a sieve reified as a subobject: the natural transformation out of it
-- that the value's family is.
restrictTo
  :: forall {j} {k} q (a :: k) (b :: j) t (p :: j +-> k)
   . (q :~> Yo a (OP b))
  -> Plus t p a b
  -> q :~> p
restrictTo :: forall {j} {k} (q :: k -> j -> Type) (a :: k) (b :: j) t
       (p :: k -> j -> Type).
(q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
restrictTo q :~> Yo a (OP b)
incl (Plus forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f) q a b
y = case q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl q a b
y of
  Yo a ~> a
g b1 ~> b
h ->
    p a b -> Maybe (p a b) -> p a b
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> p a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"restrictTo: the sieve is not inside the support -- see HasFiniteCovers's Composition law") ((a ~> a) -> (b ~> b) -> Maybe (p a b)
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f a ~> a
g b ~> b
b1 ~> b
h)

-- | A value's restriction to the least dense sieve, as its 'natTable': the indices of its values
-- at that sieve's points. See 'Plus' for what that determines.
plusTable
  :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j)
   . (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k)
  => Plus t p a b
  -> [Natural]
plusTable :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) =>
Plus t p a b -> [Natural]
plusTable x :: Plus t p a b
x@Plus{} = Sieve a b
-> (forall (q :: j +-> k).
    Finitary q =>
    (q :~> Yo a (OP b)) -> [Natural])
-> [Natural]
forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Sieve a b
leastDenseSieve @t @a @b) \ @q q :~> Yo a (OP b)
incl -> forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
(p :~> q) -> [Natural]
natTable @q @p ((q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
forall {j} {k} (q :: k -> j -> Type) (a :: k) (b :: j) t
       (p :: k -> j -> Type).
(q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
restrictTo q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl Plus t p a b
x)

-- | Whether two values stand for the same element: their restrictions to the least dense sieve
-- agree. One sieve for the pair, where two 'plusTable's would each build their own -- which is what
-- "Proarrow.Testing"\'s equality on 'Plus' wants, since it compares far more often than it shows.
samePlus
  :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j)
   . (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k)
  => Plus t p a b
  -> Plus t p a b
  -> P.Bool
samePlus :: forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) =>
Plus t p a b -> Plus t p a b -> Bool
samePlus x :: Plus t p a b
x@Plus{} Plus t p a b
y = Sieve a b
-> (forall (q :: j +-> k).
    Finitary q =>
    (q :~> Yo a (OP b)) -> Bool)
-> Bool
forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Sieve a b
leastDenseSieve @t @a @b) \ @q q :~> Yo a (OP b)
incl ->
  -- one walk for the pair, and one 'toIndex' per point: at 'Sheafify' that is itself an enumeration
  [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
P.and
    (forall {j} {k} (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
forall (p :: j +-> k) r.
(Finitary p, FiniteCat j, FiniteCat k) =>
(forall (a :: k) (b :: j). (Ob a, Ob b) => p a b -> r) -> [r]
natDomain @q @P.Bool \ @c @d q a b
z -> let ix :: p a b -> Natural
ix = 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 @p @c @d in p a b -> Natural
ix ((q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
forall {j} {k} (q :: k -> j -> Type) (a :: k) (b :: j) t
       (p :: k -> j -> Type).
(q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
restrictTo q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl Plus t p a b
x q a b
z) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
P.== p a b -> Natural
ix ((q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
forall {j} {k} (q :: k -> j -> Type) (a :: k) (b :: j) t
       (p :: k -> j -> Type).
(q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
restrictTo q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl Plus t p a b
y q a b
z))

-- | Numbered by 'plusElements', as the internal hom is numbered by the natural transformations
-- out of its weight.
instance (HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k) => Finitary (Plus t p :: j +-> k) where
  size :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural
size @a @b = [Plus t p a b] -> Natural
forall i a. Num i => [a] -> i
genericLength (forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k, Ob a,
 Ob b) =>
[Plus t p a b]
plusElements @t @p @a @b)

  -- above the argument lambda: the sieve too, not just 'natIndex'\'s enumeration
  toIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Plus t p a b -> Natural
toIndex @a @b = Sieve a b
-> (forall (q :: j +-> k).
    Finitary q =>
    (q :~> Yo a (OP b)) -> Plus t p a b -> Natural)
-> Plus t p a b
-> Natural
forall {j} {k} (a :: k) (b :: j) r.
(FiniteCat j, FiniteCat k) =>
Sieve a b
-> (forall (q :: j +-> k). Finitary q => (q :~> Yo a (OP b)) -> r)
-> r
withSieve (forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, FiniteCat j, FiniteCat k, Ob a, Ob b) =>
Sieve a b
leastDenseSieve @t @a @b) \ @q q :~> Yo a (OP b)
incl ->
    let ix :: (q :~> p) -> Natural
ix = forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[Char] -> (p :~> q) -> Natural
forall (p :: j +-> k) (q :: j +-> k).
(Finitary p, Finitary q, FiniteCat j, FiniteCat k) =>
[Char] -> (p :~> q) -> Natural
natIndex @q @p [Char]
"toIndex: not natural on the least dense sieve"
    in \Plus t p a b
x -> (q :~> p) -> Natural
ix ((q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
forall {j} {k} (q :: k -> j -> Type) (a :: k) (b :: j) t
       (p :: k -> j -> Type).
(q :~> Yo a (OP b)) -> Plus t p a b -> q :~> p
restrictTo q a b -> Yo a (OP b) a b
q :~> Yo a (OP b)
incl Plus t p a b
x)
  fromIndex :: forall (a :: k) (b :: j). (Ob a, Ob b) => Natural -> Plus t p a b
fromIndex @a @b = [Plus t p a b] -> Natural -> Plus t p a b
forall i a. Integral i => [a] -> i -> a
genericIndex (forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k, Ob a,
 Ob b) =>
[Plus t p a b]
plusElements @t @p @a @b)
  elements :: forall (a :: k) (b :: j). (Ob a, Ob b) => [Plus t p a b]
elements @a @b = forall t {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(HasFiniteCovers t k, Finitary p, FiniteCat j, FiniteCat k, Ob a,
 Ob b) =>
[Plus t p a b]
plusElements @t @p @a @b

-- | Sheafification: the plus construction twice. One 'Plus' makes a profunctor /separated/ -- two
-- elements with the same restrictions to a dense sieve are equal -- and the second makes it a
-- sheaf. The first alone need not: @Props.Sheaf@'s constant presheaf on the two-point space has one
-- section over the empty set after one plus, but still two over the whole space where a sheaf needs
-- four. On a site whose covers have no overlaps, 'Proarrow.Category.Sheaf.ByArrow' say, one plus is
-- already a sheaf and the second changes nothing.
type Sheafify :: forall {j} {k}. Type -> j +-> k -> j +-> k
type Sheafify t p = Plus t (Plus t p)

-- | The unit of the plus construction: an element as the family of its own restrictions, on the
-- maximal sieve.
unitPlus :: forall t {j} {k} (p :: j +-> k). (Profunctor p) => p :~> Plus t p
unitPlus :: forall t {j} {k} (p :: j +-> k). Profunctor p => p :~> Plus t p
unitPlus p a b
x = (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
forall {k} {j} (a :: k) (b :: j) (p :: j +-> k) t.
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
Plus (\c ~> a
g b ~> d
h -> p c d -> Maybe (p c d)
forall a. a -> Maybe a
P.Just ((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
g b ~> d
h p a b
x)) ((Ob a, Ob b) => Plus t p a b) -> p a b -> Plus t p a b
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

-- | 'unitPlus' twice: the unit of sheafification.
unitSheafify :: forall t {j} {k} (p :: j +-> k). (Profunctor p) => p :~> Sheafify t p
unitSheafify :: forall t {j} {k} (p :: j +-> k). Profunctor p => p :~> Sheafify t p
unitSheafify p a b
x = forall t {j} {k} (p :: j +-> k). Profunctor p => p :~> Plus t p
unitPlus @t (forall t {j} {k} (p :: j +-> k). Profunctor p => p :~> Plus t p
unitPlus @t p a b
x)

-- | The universal property, one plus at a time: a map into a sheaf extends along 'unitPlus'. A
-- dense support either is everything, and the family is read off at the identity, or contains the
-- legs of some listed cover -- that is what density at the identity says, and 'coveringCover' finds
-- it -- and the family restricted to those legs glues. Which cover is found does not matter, @q@
-- being a sheaf; nor need @q@ be 'Finitary' -- gluing is all that is asked of it.
extendPlus
  :: forall t {j} {k} (p :: j +-> k) q
   . (HasFiniteCovers t k, Sheaf t q)
  => (p :~> q) -> Plus t p :~> q
extendPlus :: forall t {j} {k} (p :: j +-> k) (q :: j +-> k).
(HasFiniteCovers t k, Sheaf t q) =>
(p :~> q) -> Plus t p :~> q
extendPlus p :~> q
n x :: Plus t p a b
x@(Plus forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f) = case (a ~> a) -> (b ~> b) -> Maybe (p a b)
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p 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 of
  P.Just p a b
v -> p a b -> q a b
p :~> q
n p a b
v
  Maybe (p a b)
P.Nothing -> case forall t {j} {k} (a :: k) (b :: j).
(HasFiniteCovers t k, CategoryOf j) =>
Sieve a b -> Maybe (SomeCover t k a)
coveringCover @t (Plus t p a b -> Sieve a b
forall {k1} {k} t (p :: k1 +-> k) (a :: k) (b :: k1).
Plus t p a b -> Sieve a b
support Plus t p a b
x) of
    -- the error is unreachable: 'coveringCover' returned this cover by testing these same legs. It
    -- cannot be dropped either -- 'glue' wants a total function on legs, and they arrive packed.
    P.Just (SomeCover Cover t k a c
c) -> forall {j} {k} t (p :: j +-> k) (a :: k) c (b :: j).
(Sheaf t p, Ob a, Ob b) =>
Cover t k a c -> (forall (x :: k). Leg t k a c x -> p x b) -> p a b
forall t (p :: j +-> k) (a :: k) c (b :: j).
(Sheaf t p, Ob a, Ob b) =>
Cover t k a c -> (forall (x :: k). Leg t k a c x -> p x b) -> p a b
glue @t Cover t k a c
c \Leg t k a c x
l -> q x b -> (p x b -> q x b) -> Maybe (p x b) -> q x b
forall b a. b -> (a -> b) -> Maybe a -> b
P.maybe ([Char] -> q x b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"extendPlus: a leg outside the support") p x b -> q x b
p :~> q
n ((x ~> a) -> (b ~> b) -> Maybe (p x b)
forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d)
f (Leg t k a c x -> x ~> a
forall (a :: k) c (x :: k). Leg t k a c x -> x ~> a
forall t k (a :: k) c (x :: k). Site t k => Leg t k a c x -> x ~> a
legArrow Leg t k a c x
l) b ~> b
forall (a :: j). Ob a => a ~> a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id)
    Maybe (SomeCover t k a)
P.Nothing -> [Char] -> q a b
forall a. HasCallStack => [Char] -> a
P.error [Char]
"extendPlus: the support is not dense"

-- | Gluing for the plus construction: a matching family over a cover, assembled into one family.
-- At @(g, h)@ it takes the first leg that @g@ factors through and whose family is defined at the
-- factor -- 'factorThrough' gives that factor @u@, and the value is the leg's family at @(u, h)@.
-- So the support of the result is what the legs generate from the legs' own supports, which is
-- dense by 'Proarrow.Category.Sheaf.HasFiniteCovers'\'s Composition law.
--
-- Well definedness -- that another leg, or another factorisation through the same leg, gives the
-- same value -- is exactly what /matching/ says, and 'glue' is unconstrained on families that are
-- not matching, so the first one found is as good as any.
gluePlus
  :: forall t {j} {k} (q :: j +-> k) (a :: k) c (b :: j)
   . (Site t k, LocallyFinite k, Ob a, Ob b)
  => Cover t k a c
  -> (forall x. Leg t k a c x -> Plus t q x b)
  -> Plus t q a b
gluePlus :: forall t {j} {k} (q :: j +-> k) (a :: k) c (b :: j).
(Site t k, LocallyFinite k, Ob a, Ob b) =>
Cover t k a c
-> (forall (x :: k). Leg t k a c x -> Plus t q x b) -> Plus t q a b
gluePlus Cover t k a c
c forall (x :: k). Leg t k a c x -> Plus t q x b
m =
  let ls :: [SomeLeg t k a c]
ls = Cover t k a c -> [SomeLeg t k a c]
forall (a :: k) c. Cover t k a c -> [SomeLeg t k a c]
forall t k (a :: k) c.
Site t k =>
Cover t k a c -> [SomeLeg t k a c]
legs Cover t k a c
c
  in (forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (q c d))
-> Plus t q a b
forall {k} {j} (a :: k) (b :: j) (p :: j +-> k) t.
(Ob a, Ob b) =>
(forall (c :: k) (d :: j). (c ~> a) -> (b ~> d) -> Maybe (p c d))
-> Plus t p a b
Plus \c ~> a
g b ~> d
h ->
       -- matching @Plus f@ is what brings the leg's source into scope, as 'plusTable' also relies on
       c ~> a
g (c ~> a) -> ((Ob c, Ob a) => Maybe (q c d)) -> Maybe (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
// [q c d] -> Maybe (q c d)
forall a. [a] -> Maybe a
listToMaybe ((SomeLeg t k a c -> Maybe (q c d)) -> [SomeLeg t k a c] -> [q c d]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(SomeLeg Leg t k a c x
l) -> case Leg t k a c x -> Plus t q x b
forall (x :: k). Leg t k a c x -> Plus t q x b
m Leg t k a c x
l of Plus forall (c :: k) (d :: j). (c ~> x) -> (b ~> d) -> Maybe (q c d)
f -> (c ~> a) -> (x ~> a) -> Maybe (c ~> x)
forall {k} (x :: k) (y :: k) (a :: k).
(LocallyFinite k, Ob x, Ob y, Ob a) =>
(x ~> a) -> (y ~> a) -> Maybe (x ~> y)
factorThrough c ~> a
g (Leg t k a c x -> x ~> a
forall (a :: k) c (x :: k). Leg t k a c x -> x ~> a
forall t k (a :: k) c (x :: k). Site t k => Leg t k a c x -> x ~> a
legArrow Leg t k a c x
l) Maybe (c ~> x) -> ((c ~> x) -> Maybe (q c d)) -> Maybe (q c d)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
P.>>= \c ~> x
u -> (c ~> x) -> (b ~> d) -> Maybe (q c d)
forall (c :: k) (d :: j). (c ~> x) -> (b ~> d) -> Maybe (q c d)
f c ~> x
u b ~> d
h) [SomeLeg t k a c]
ls)

-- | Sheafification lands in the sheaves. This is the theorem @Props.Sheaf@ checks by enumeration
-- with @'isSheaf' \@t \@('Sheafify' t p)@; here it is as an instance, so a 'Sheafify' can be used
-- wherever a 'Sheaf' is asked for.
--
-- 'gluePlus' would type-check for any @'Plus' t q@, but its laws need @q@ /separated/ -- which
-- @'Plus' t p@ always is, so the head is the double plus. The single-plus statement that is also
-- true, @'Sheaf' t p => 'Sheaf' t ('Plus' t p)@, is thereby foreclosed for good: it would overlap
-- this one with neither more specific.
instance (Site t k, LocallyFinite k, CategoryOf j) => Sheaf t (Sheafify t (p :: j +-> k)) where
  glue :: forall (a :: k) c (b :: j).
(Ob a, Ob b) =>
Cover t k a c
-> (forall (x :: k). Leg t k a c x -> Sheafify t p x b)
-> Sheafify t p a b
glue = forall t {j} {k} (q :: j +-> k) (a :: k) c (b :: j).
(Site t k, LocallyFinite k, Ob a, Ob b) =>
Cover t k a c
-> (forall (x :: k). Leg t k a c x -> Plus t q x b) -> Plus t q a b
gluePlus @t

-- | 'extendPlus' twice: a map into a sheaf extends along 'unitSheafify'.
extendSheafify
  :: forall t {j} {k} (p :: j +-> k) q
   . (HasFiniteCovers t k, Sheaf t q)
  => (p :~> q) -> Sheafify t p :~> q
extendSheafify :: forall t {j} {k} (p :: j +-> k) (q :: j +-> k).
(HasFiniteCovers t k, Sheaf t q) =>
(p :~> q) -> Sheafify t p :~> q
extendSheafify p :~> q
n = forall t {j} {k} (p :: j +-> k) (q :: j +-> k).
(HasFiniteCovers t k, Sheaf t q) =>
(p :~> q) -> Plus t p :~> q
extendPlus @t (forall t {j} {k} (p :: j +-> k) (q :: j +-> k).
(HasFiniteCovers t k, Sheaf t q) =>
(p :~> q) -> Plus t p :~> q
extendPlus @t p a b -> q a b
p :~> q
n)

-- * The category of sheaves

-- | The full subcategory of @'FINITARY' j k@ on the sheaves for @t@: the finitary profunctors that
-- have a 'Sheaf' instance. Its finite limits are computed exactly as 'FINITARY'\'s and are sheaves
-- by the closure instances -- 'TerminalProfunctor', ':*:', and
-- 'Proarrow.Category.Enriched.Finitary.Topos.Reindex' for the equalizers. Its colimits are /not/
-- computed as 'FINITARY'\'s: a quotient of sheaves is no sheaf, and they go through 'Sheafify'.
-- Its hom-sets are finitary by the conjunction instance in "Proarrow.Category.Enriched.Finitary.Topos".
type SHEAVES t j k = SUBCAT ((Finitary :&&: Sheaf t) :: OB (j +-> k))

-- | A sheaf as an object of 'SHEAVES', as 'Proarrow.Category.Enriched.Finitary.Topos.FIN' names
-- an object of 'FINITARY'.
type SHF t (p :: j +-> k) = SUB p :: SHEAVES t j k

instance (Site t k, CategoryOf j) => HasTerminalObject (SHEAVES t j k) where
  type TerminalObject = SUB TerminalProfunctor
  terminate :: forall (a :: SHEAVES t j k). Ob a => a ~> TerminalObject
terminate = Prof (UN SUB a) TerminalProfunctor
-> Sub Prof (SUB (UN SUB a)) (SUB 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 (Site t k, CategoryOf j) => HasBinaryProducts (SHEAVES t j k) where
  type a && b = SUB (UN SUB a :*: UN SUB b)
  withObProd :: forall (a :: SHEAVES t j k) (b :: SHEAVES t 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 :: SHEAVES t j k) (b :: SHEAVES t 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 :: SHEAVES t j k) (b :: SHEAVES t 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 :: SHEAVES t j k) (x :: SHEAVES t j k)
       (y :: SHEAVES t 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)

-- | Equalizers as in 'FINITARY', by 'equalizeNat'; the result is a sheaf for every coverage, which
-- 'Proarrow.Testing.Laws.testEqualizersAreSheaves' checks by enumeration.
instance (Site t k, Enumerable j, Enumerable k) => HasEqualizers (SHEAVES t j k) where
  equalize :: forall (a :: SHEAVES t j k) (b :: SHEAVES t j k) r.
(a ~> b)
-> (a ~> b) -> (forall (e :: SHEAVES t j k). (e ~> a) -> r) -> r
equalize (Sub (Prof a1 :~> b1
f)) (Sub (Prof a1 :~> b1
g)) forall (e :: SHEAVES t j k). (e ~> a) -> r
k = (a1 :~> b1)
-> (a1 :~> b1)
-> (forall (fs :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) fs =>
    (Reindex Subobject a1 fs :~> a1) -> r)
-> r
forall {j} {k} (p :: j +-> k) (q :: j +-> k) r.
(Finitary p, Finitary q, Enumerable j, Enumerable k) =>
(p :~> q)
-> (p :~> q)
-> (forall (fs :: [[[[Nat]]]]).
    KnownTable (Objects j) (Objects k) fs =>
    (Reindex Subobject p fs :~> p) -> r)
-> r
equalizeNat a1 a b -> b1 a b
a1 :~> b1
f a1 a b -> b1 a b
a1 :~> b1
g \Reindex Subobject a1 fs :~> a1
incl -> (SUB (Reindex Subobject a1 fs) ~> a) -> r
forall (e :: SHEAVES t j k). (e ~> a) -> r
k (Prof (Reindex Subobject a1 fs) a1
-> Sub Prof (SUB (Reindex Subobject a1 fs)) (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 ((Reindex Subobject a1 fs :~> a1)
-> Prof (Reindex Subobject a1 fs) a1
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof Reindex Subobject a1 fs a b -> a1 a b
Reindex Subobject a1 fs :~> a1
incl))
  factorEqualizer :: forall (e :: SHEAVES t j k) (x :: SHEAVES t j k)
       (e' :: SHEAVES t j k).
(e ~> x) -> (e' ~> x) -> e' ~> e
factorEqualizer (Sub (Prof a1 :~> b1
incl)) (Sub (Prof 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 ((a1 :~> a1) -> Prof a1 a1
forall {j} {k} (p :: j +-> k) (q :: j +-> k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof ((a1 :~> b1) -> (a1 :~> b1) -> a1 :~> a1
forall {j} {k} (e :: j +-> k) (x :: j +-> k) (e' :: j +-> k).
(Finitary e, Finitary x, Profunctor e') =>
(e :~> x) -> (e' :~> x) -> e' :~> e
factorThroughEqualizer a1 a b -> b1 a b
a1 :~> b1
incl a1 a b -> b1 a b
a1 :~> b1
h))

instance (Site t k, Enumerable j, Enumerable k) => HasPullbacks (SHEAVES t j k)