Commit 2023-11-20 12:33 1a013164

View on Github →

fix(CategoryTheory): remove unnecessary noncomputable modifier (#8528) The EffectiveEpiStruct for a RegularEpi turned out to become computable after applying suggestions from code review.

Estimated changes