leave comment about functoriality of products following from symmetry

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jan 11, 2024 · 7449583 · 7449583
1 parent 244b5cd
commit 7449583
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
@@ -171,6 +171,8 @@ Class HasBinaryProducts (A : Type) `{Is1Cat A} := {
 (** *** Product functor *)
 
 (** Binary products are functorial in each argument. *)
+
+(* TODO: jdchristensen: Another approach to handling functoriality on the right is to first prove that products are symmetric. Then functoriality on the right follows from functoriality on the left... *)
 Global Instance is0functor_cat_prod_l {A : Type}
   `{HasBinaryProducts A} y
   : Is0Functor (fun x => cat_prod x y).