Documentation

factorEqualizer incl h requires h's image to lie within incl's. Since BOOL is the 2-element total order FLS <= TRU, that means h's domain is <= incl's domain. That's always true when incl came from equalize (which only ever produces the identity), but since BOOL is totally ordered we can case on the shapes directly (at most 5 are reachable, since both share a codomain).

COST is thin and totally ordered, so equalizers are trivial. factorEqualizer incl h just compares e and e' directly (their common bound x does not matter), erroring when and only when e' is finite and strictly less than e, or e is INF while e' is finite.

>>> let f :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,0), (1,1), (2,1), (3,0)]
>>> let g :: FinHask (FH (Fin 4)) (FH (Fin 3)) = fromList [(0,2), (1,0), (2,1), (3,0)]
>>> let h :: FinHask (FH (Fin 3)) (FH (Fin 4)) = fromList [(0,3), (1,2), (2,3)]
>>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
"(fromList [(0,2),(1,3)],fromList [(0,1),(1,0),(2,1)],fromList [(0,3),(1,2),(2,3)])"

>>> import Data.Fin
>>> import Data.Type.Nat
>>> import Data.Vec.Lazy
>>> let f :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin0 ::: fin1 ::: fin1 ::: fin0 ::: VNil
>>> let g :: FinSet (FS Nat4) (FS Nat3) = FinSet $ fin2 ::: fin0 ::: fin1 ::: fin0 ::: VNil
>>> let h :: FinSet (FS Nat3) (FS Nat4) = FinSet $ fin3 ::: fin2 ::: fin3 ::: VNil
>>> (equalize f g \incl -> let p = factorEqualizer incl h in P.show (incl, p, incl . p)) :: P.String
"(FinSet {unFinSet = 2 ::: 3 ::: VNil},FinSet {unFinSet = 1 ::: 0 ::: 1 ::: VNil},FinSet {unFinSet = 3 ::: 2 ::: 3 ::: VNil})"

The equalizer of two linear maps f, g :: M m ~> M n is the kernel of f - g: the subspace of M m on which they agree. Computed by row-reducing f - g to reduced row echelon form; the free (non-pivot) columns of the result index a basis of the kernel.

>>> import Data.Vec.Lazy (Vec(..))
>>> let f = Mat @(S (S Z)) @(S Z) ((1 ::: 2 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let g = Mat @(S (S Z)) @(S Z) ((3 ::: 0 ::: VNil) ::: VNil) :: Mat (M (S (S Z))) (M (S Z) :: MatK P.Double)
>>> let h = Mat @(S Z) @(S (S Z)) ((1 ::: VNil) ::: (1 ::: VNil) ::: VNil) :: Mat (M (S Z)) (M (S (S Z)) :: MatK P.Double)
>>> (equalize f g \incl@(Mat inclv) -> case factorEqualizer incl h of p@(Mat pv) -> P.show (inclv, pv, unMat (incl . p))) :: P.String
"((1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: VNil,(1.0 ::: VNil) ::: (1.0 ::: VNil) ::: VNil)"

LTE is thin, so equalizers are trivial. factorEqualizer incl h just needs h's domain to be <= incl's domain. Since both share the codomain x, this can only fail when incl's domain is OZ (nothing below it) but h's domain is a successor (necessarily above OZ).

Equalizers are unchanged by making the tensor the product.

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.

Morphisms of COPRODUCT never cross sides, so this is a straight case split reusing either j's or k's own equalizer.

Equalizers as in FINITARY, by equalizeNat; the result is a sheaf for every coverage, which testEqualizersAreSheaves checks by enumeration.