search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Discrepancy of `unique` of `Product` and `unique` of `IsPullback` #329

Open sergey-goncharov opened 2 years ago

sergey-goncharov commented 2 years ago

Binary products are special pullbacks. The current implementation of IsPullback in Categories.Diagram.Pullback almost conforms to the corresponding definition of binary products in Categories.Object.Product.Core, except one little twist: in the conclusion of the unique field the universal morphism is on the left in one case and on the right in the other case. Perhaps, this should be unified. It is probably easier to accept the order, as in products.

JacquesCarette commented 2 years ago

I agree that the order in Product is the better one. Especially as one sees uses of converse to prove very simple things using pullback, which is a hint that the order is wrong.