Cartesian products of categories #
We define the category instance on
C × D when
D are categories.
sectl C Z: the functor
C ⥤ C × Dgiven by
X ↦ ⟨X, Z⟩
sectr Z D: the functor
D ⥤ C × Dgiven by
Y ↦ ⟨Z, Y⟩
fst: the functor
⟨X, Y⟩ ↦ X
snd: the functor
⟨X, Y⟩ ↦ Y
swap: the functor
C × D ⥤ D × Cgiven by
⟨X, Y⟩ ↦ ⟨Y, X⟩(and the fact this is an equivalence)
Two rfl lemmas that cannot be generated by
Category.uniformProd C D is an additional instance specialised so both factors have the same
universe levels. This helps typeclass resolution.
Swapping the factors of a cartesian product of categories twice is naturally isomorphic to the identity functor.
The "evaluation at
X" functor, such that
(evaluation.obj X).obj F = F.obj X,
which is functorial in both
The constant functor followed by the evaluation functor is just the identity.
The cartesian product of two functors.
prod, but both functors start from the same category
F.prod' G followed by projection on the first component is isomorphic to
F.prod' G followed by projection on the second component is isomorphic to
The cartesian product of two natural transformations.
F.flip composed with evaluation is the same as evaluating
The forward direction for
The backward direction for
The unit isomorphism for
The counit isomorphism for
The equivalence of categories between
(A ⥤ B) × (A ⥤ C) and
A ⥤ (B × C)