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