Commit 2025-10-01 08:55 75a0561f
View on Github →feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform): more lemmas about isomorphisms of CatCospanTransform (#26547)
We construct ways to extract left, right or base components of ismorphisms of CatCospanTransform, as well as various IsIso instances, and lemmas allowing to compute the left, right or base component of the inverse of a CatCospanTransformMorphism that has an IsIso instance.