Source: ProCGroups.ProC.Category.Pushouts
1import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
2import ProCGroups.ProC.Category.Basic
4/-!
5# Pro C Groups / pro-C / Category / Pushouts
7Pushout universal properties in `ProCGrp C` use mathlib's
8`CategoryTheory.IsPushout` predicate and its standard `desc`, factorization,
9extensionality, and comparison-isomorphism API. This module remains as the
10stable import boundary for those definitions.
11-/