Commit 2026-08-15 18:18 49d8727d

chore(CategoryTheory/Discrete/Basic): refactor the hom type for to_dual (#42796) This PR uses to_dual for Discrete. This is a prerequisite for using to_dual for e.g. BinaryProducts. We refactor the hom type of the discrete category using a special structure that has to_dual annotations. to_dual needs this abstraction boundary to work. We add the theorem Discrete.hom_eq, which is useful to fix one of the broken proofs.