Commit 2024-10-10 08:57 09585751
View on Github →chore(CategoryTheory/Limits/Shapes/BinaryProducts): Make some WalkingPair
-related constructions computable (#17597)
Change the computability of some constructions related to WalkingPair
, so that mapPair
, diagramIsoPair
and pairComp
are no longer marked as noncomputable.