Preserving binary products #
Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.
In particular, we show that ProdComparison G X Y
is an isomorphism iff G
preserves
the product of X
and Y
.
The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute BinaryFan.mk
with Functor.mapCone
.
Instances For
The property of preserving products expressed in terms of binary fans.
Instances For
The property of reflecting products expressed in terms of binary fans.
Instances For
If G
preserves binary products and C
has them, then the binary fan constructed of the mapped
morphisms of the binary product cone is a limit.
Instances For
If the product comparison map for G
at (X,Y)
is an isomorphism, then G
preserves the
pair of (X,Y)
.
Instances For
If G
preserves the product of (X,Y)
, then the product comparison map for G
at (X,Y)
is
an isomorphism.
Instances For
The map of a binary cofan is a colimit iff
the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute BinaryCofan.mk
with Functor.mapCocone
.
Instances For
The property of preserving coproducts expressed in terms of binary cofans.
Instances For
The property of reflecting coproducts expressed in terms of binary cofans.
Instances For
If G
preserves binary coproducts and C
has them, then the binary cofan constructed of the mapped
morphisms of the binary product cocone is a colimit.
Instances For
If the coproduct comparison map for G
at (X,Y)
is an isomorphism, then G
preserves the
pair of (X,Y)
.
Instances For
If G
preserves the coproduct of (X,Y)
, then the coproduct comparison map for G
at (X,Y)
is
an isomorphism.