Categories of indexed families of objects. #
We define the pointwise category structure on indexed families of objects in a category (and also the dependent generalization).
This provides some assistance to typeclass search in a common situation,
which otherwise fails. (Without this
The natural isomorphism between pulling back a grading along the identity function, and the identity functor.
The natural isomorphism comparing between pulling back along two successive functions, and pulling back along their composition
The natural isomorphism between pulling back then evaluating, and just evaluating.
The bifunctor combining an
I-indexed family of objects with a
J-indexed family of objects
to obtain an
I ⊕ J-indexed family of objects.
An isomorphism between
I-indexed objects gives an isomorphism between each
pair of corresponding components.
I-indexed family of functors into a functor between the pi types.
pi, but all functors come from the same category
Two functors to a product category are equal iff they agree on every coordinate.
I-indexed family of natural transformations into a single natural transformation.