Def CategoryTheory.Limits.Sigma.functorι

Modification history

2026-09-11 21:15

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

chore(CategoryTheory/Limits/Shapes/Products): use `to_dual` (#43542) …

Deleted CategoryTheory.Limits.Sigma.functorι View on Github →

2026-05-06 00:44

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

refactor(CategoryTheory/Limits): redefine `IsIPC` in terms of `IsIPCOfShape` (#38378) …

Added CategoryTheory.Limits.Sigma.functorι View on Github →