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

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.

Enumerate a set of families by brute force: every way of choosing a value at each point of the domain, kept when it satisfies every condition. A condition is checked as soon as both of its points have been chosen, so a violation prunes the whole subtree of completions rather than rejecting each of them in turn -- which is what keeps the candidate space from being the full product. Families come out in the same order as sequence choices would give them: the earliest point varies slowest.

Which of the enumerated families a tabulated one is.

One point of the domain of the end ∫ Set(p c d, q c d) whose elements are the natural transformations p -> q: an object pair and an element of p there. Every end below is one of these: the internal hom only changes the weight p, and the subobject classifier also changes what the conditions are read as. So this is the single enumeration the topos is built on.

Visit every point of that domain, in one fixed order.

Where each point of the domain sits in a tabulated family. This is the same for every family over a given weight, so bind it once outside a loop over them.

Read a tabulated family back as a function on the points, given those positions.

Every natural transformation p -> q, as its list of q-indices in natDomain order. Naturality is the only condition: the value at x and the value at dimap g h x must agree after transport.

The conditions as positions in a tabulated family, with q's transport handed to the relation. Only the internal hom reads that transport; the sieves below ignore it, and pass TerminalProfunctor for q so that computing it costs nothing.

The naturality conditions on a transformation. As in closedUnder, dimap g h is lmap g . rmap h, so commuting with the two whiskerings separately is commuting with the action: two walks over three objects rather than one over four, and the transport table depends on the arrow alone rather than on each element.

A natural transformation as its table of q-indices, in natDomain order. That is everything there is to see of one, so it serves for both comparing and showing.

Every natural transformation p -> q, as an arrow of FINITARY j k. This is what makes the category of finitary profunctors testable: its hom-sets are enumerable, so a generator can pick from them, where in general a natural transformation is not something one can generate.

A tabulated transformation as an arrow.

What the internal hom at a/b is a set of natural transformations out of. An element of it over c/d is an arrow into a, an arrow out of b and an element of p -- exactly the three arguments an Exp takes.

A tabulated family as an element of the internal hom.

Every sieve at a/b, as the points of Yo a (OP b) it contains, in natDomain order: all subsets, kept when closed. This is the same end again, at the weight Yo a (OP b) and valued in booleans, with the naturality conditions read as implications rather than equations.

A sieve as the tabulation of its membership, in natDomain order -- the inverse of sieveAt.

A tabulated sieve as a sieve.