Documentation

Identity natural transformation, used as a 2-cell between profunctors that happen to be syntactically equal.

A type-level list of profunctors, from category j to category k.

(as +++ bs) +++ cs and as +++ (bs +++ cs) are the same Path. Proved once, up front, by (mutual) induction with IsOb's superclasses -- see there for how the induction actually goes through -- so that every other associativity fact needed anywhere in Proarrow.Squares is a free ~ coercion instead of a function call.

Fold a Path down to the single profunctor its elements compose to.

Which per-element property a SPath witnesses. Tight plays the role of the tight (vertical, Representable) legs of the Prof equipment; a later Cotight would do the same for Corepresentable legs.

The per-element constraint a Tag stands for. c is applied homogeneously at every element of a path, each of a (potentially) different i +-> j kind -- a genuinely impredicative use GHC's kind system can't express with c itself as the parameter, so Tag is the (monomorphic, first-order) proxy for it instead. Mirrors Proarrow.Bicategory.Sub's IsOb/SUBCAT tag mechanism.

Runtime witness that every element of a Path satisfies Sat t. Replaces having a separate witness type per tag (what used to be SPath/TPath), so (|||)/(===) only need one append lemma (withObAppend), not one per kind of leg.

ps is a path all of whose elements satisfy Sat t. Only two cases (Nil/Cons) are needed: the head p stays concrete at each step of withObAppend's recursion, so GHC's own instance resolution reattaches it to the recursively-derived IsOb t (ps +++ qs) for free -- it never needs to reduce ps +++ qs itself, just match the (:::) shape.

Concatenate two witnesses. Plain recursion, no constraint solving -- unlike withObAppend, which additionally proves IsOb t (ps +++ qs).

Bring a specific instantiation of IsOb t ps's quantified Assoc ps qs rs superclass into scope. Needed explicitly: GHC won't search the superclasses of an arbitrary given constraint to solve an unrelated ~ goal, so uses of associativity (e.g. in (|||)/(===)) have to ask for it by name at the specific ps/qs/rs in play, even though the fact itself is free once asked for.

A well-formed (horizontal) path: every element is a plain Profunctor.

A tight (vertical) path: every element is Representable.

A tight path is, in particular, a well-formed path (Representable implies Profunctor). Needed explicitly because different Tags don't otherwise know anything about each other.

ps,qs both satisfy Sat t pointwise ⟹ so does ps +++ qs.

Extract Profunctor evidence for Fold ps from a runtime witness.

Extract Representable evidence for Fold ps from a runtime witness. The body is identical to withFoldOb's -- both just extract Sat t (Fold ps), which needs the same single-vs-multi-element case split Fold itself has -- but there's no polymorphic t anywhere that would let one definition serve both: every call site already knows its tag concretely, so there's nothing to be generic over.

Combine the composites of two adjacent paths into the composite of their concatenation.

The inverse of concatFold.

Apply a 2-cell inside a concatenation, on the right.

Apply a 2-cell inside a concatenation, on the left.