fact: Definition Pullback {a b c : C} (f : b --> a) (g : c --> a) := ∑ pfg : (∑ p : C, (p --> b) × (p --> c)), ∑ (H : pr1 (pr2 pfg) · f = pr2 (pr2 pfg) · g), isPullback f g (pr1 (pr2 pfg)) (pr2 (pr2 pfg)) H.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics