The category of graded objects #
For any type
β-graded object over some category
C is just
β → C into the objects of
We put the "pointwise" category structure on these, as the non-dependent specialization of
We describe the
comap functors obtained by precomposing with functions
β → γ.
As a consequence a fixed element (e.g.
1) in an additive group
β provides a shift
Pull back an
I-graded object in
C to a
J-graded object along a function
J → I.
The natural isomorphism comparing between pulling back along two propositionally equal functions.
The equivalence between β-graded objects and γ-graded objects, given an equivalence between β and γ.
The total object of a graded object is the coproduct of the graded components.
total functor taking a graded object to the coproduct of its graded components is faithful.
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
which follows from the fact we have zero morphisms and decidable equality for the grading.