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.

The subcategory of finitary profunctors, as Proarrow.Category.Instance.Rep does for representable ones.

[0 .. n-1], which n being a Natural rules out writing directly.

The position of an object in its kind's object list.

Everything an enumeration of a kind's objects can do at each of them, concatenated.

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.

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 FINHASK -- see its EnrichedProfunctor FINHASK instance -- exactly as a decided profunctor is one enriched in BOOL.

A category whose hom-sets are finite: the Finitary counterpart of Decidable, and one half of FiniteCat.

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 universeF, which is all a bare Finite instance allows. That is fine for small hom-sets, and an instance whose hom-sets are large should compute the index arithmetically instead -- FinHask does, because Elt's Ord is compare on indices and so pays for every comparison.

A type-level list of naturals, reflected.

A type-level list of lists of naturals, reflected: the fibres of a partial surjection out of one hom-set.

Reify a list of lists of naturals.

A table: a row for each object of k, and in each row the fibres at each object of j.

Build a table by visiting every pair of objects, reifying each cell.

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.

The fibres at a pair of objects, found by walking the table to the objects' positions.

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.

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.

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.

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.

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.

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.

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.

Where each key sits in a tabulated family.

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.

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.

Every natural family, as its list of q-indices in endDomain order.

Read a tabulated family back as a function on the keys.

Which of the enumerated families a tabulated one is.

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.

A tabulated sieve as a sieve.