>>> import Proarrow.Colimit.Pushout (isEpi)
>>> let f :: FinHask (FH (Fin 3)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1)]
>>> (pushout f f \(FinHask g1) (FinHask g2) -> P.show (g1, g2)) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
>>> isEpi (f :: FinHask (FH (Fin 3)) (FH (Fin 3)))
True
>>> import Proarrow.Limit.Pullback (isMono)
>>> (pullback f f \(FinHask l) (FinHask r) -> P.show (l, r)) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,0),(1,1),(2,2)])"
>>> isMono f
True
>>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
>>> (case factorize f of p :.: q -> P.show (p, q) \\ p \\ q) :: P.String
"(fromList [(0,0),(1,1),(2,2)],fromList [(0,2),(1,0),(2,1)])"
>>> (classifyImage f, classifyKernelPair f)
(fromList [(0,True),(1,True),(2,True)],fromList [((0,0),True),((0,1),False),((0,2),False),((1,0),False),((1,1),True),((1,2),False),((2,0),False),((2,1),False),((2,2),True)])
>>> [and, or, implies] :: [FinHask (FH (Bool, Bool)) (FH Bool)]
[fromList [((False,False),False),((False,True),False),((True,False),False),((True,True),True)],fromList [((False,False),False),((False,True),True),((True,False),True),((True,True),True)],fromList [((False,False),True),((False,True),True),((True,False),False),((True,True),True)]]
>>> false :: FinHask (FH ()) (FH Bool)
fromList [((),False)]

>>> import Proarrow.Colimit.Pushout (isEpi)
>>> import Data.Fin
>>> import Data.Type.Nat
>>> let f :: FinSet (FS Nat3) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: VNil
>>> (pushout f f \(FinSet g1) (FinSet g2) -> P.show (g1, g2)) :: P.String
"(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
>>> isEpi f
True
>>> import Proarrow.Limit.Pullback (isMono)
>>> (pullback f f \(FinSet l) (FinSet r) -> P.show (l, r)) :: P.String
"(0 ::: 1 ::: 2 ::: VNil,0 ::: 1 ::: 2 ::: VNil)"
>>> isMono f
True
>>> import Proarrow.Category.Topos (classifyImage, classifyKernelPair, and, or, implies, false)
>>> (classifyImage f, classifyKernelPair f)
(FinSet {unFinSet = 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: 0 ::: 0 ::: 0 ::: 1 ::: VNil})
>>> [and, or, implies] :: [FinSet (FS Nat4) (FS Nat2)]
[FinSet {unFinSet = 0 ::: 0 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 0 ::: 1 ::: 1 ::: 1 ::: VNil},FinSet {unFinSet = 1 ::: 1 ::: 0 ::: 1 ::: VNil}]
>>> false :: FinSet (FS Nat1) (FS Nat2)
FinSet {unFinSet = 0 ::: VNil}

The classifier is the closed sieves, and an arrow is classified by FINITARY's graph sieve, closed. For an arrow of sheaves that sieve is already closed, since a sheaf is separated. The closedSieve call guards against a Sheaf instance that was asserted instead of decided, which would otherwise fail later in familyIndex as "not a closed sieve".

The subobject classifier is the profunctor of sieves, and an arrow classifies its graph.

Epi-mono factorization is computed via defaultFactorize: f factors as the coequalizer of its cokernel pair (the epi onto its image) followed by the equalizer factorization of f through that epi (the mono inclusion of the image).

>>> import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
>>> let h = Mat @(S (S Z)) @(S (S Z)) ((1 ::: 2 ::: VNil) ::: (2 ::: 4 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S (S Z)) :: MatK P.Double)
>>> (case factorize h of e :.: m -> case (e, m) of (Mat ev, Mat mv) -> P.show (ev, mv, unMat (m . e))) :: P.String
"((2.0 ::: 4.0 ::: VNil) ::: VNil,(0.5 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: 2.0 ::: VNil) ::: (2.0 ::: 4.0 ::: VNil) ::: VNil)"

Image factorization is unchanged by making the tensor the product.

The image of a natural transformation is the equalizer of its cokernel pair.

The image of an arrow of sheaves, by the same cokernel-pair construction as in FINITARY: the pushout is a colimit and so sheafified, the equalizer that follows it is not.

The topos of sheaves. Finite limits and colimits, cartesian closed, a subobject classifier, and image factorization, all defined above and none of them postulated.

The exponential needs StableSite. A full subcategory is closed when it contains its internal homs, and an internal hom is a sheaf by gluing pointwise into the codomain, which needs the cover pulled back along the argument.

Finitary profunctors between finite categories form an elementary topos: finite limits and colimits, cartesian closed, a subobject classifier, and image factorization.