## Stream: Is there code for X?

### Topic: pullbacks in Type u

#### Greg Price (Mar 31 2021 at 05:39):

Is there an explicit construction in mathlib of pullbacks in the category of types? I'd like to have something like this:

import category_theory.types
open category_theory category_theory.category

universes u
variables {X Y Z : Type u}

def pullback_obj (f : X ⟶ Z) (g : Y ⟶ Z) : Type u :=
{ p : X × Y // f p.1 = g p.2 }


along with the associated cone and is_limit.

I think I see where such a construction would be -- category_theory.limits.shapes.types -- and I don't see it there. But I know I could be missing something.

#### Scott Morrison (Mar 31 2021 at 05:40):

Yep, it's missing. Definitely okay to add it. Make sure to add both the isomorphism to the pullback coming from has_pullbacks, and the @[simp] lemmas saying how that isomorphism commutes with pullback.fst and pullback.snd.

#### Greg Price (Mar 31 2021 at 05:42):

Cool. I actually have an implementation already, which I wrote the other day -- I'd be glad to send a PR. And I'll be sure to add those pieces.

Could I have an invitation to be able to push a branch?

gnprice

#### Greg Price (Mar 31 2021 at 05:44):

I'm also interested in the specialization where one of the maps is mono:

def mono_pullback_obj (f : X ⟶ Z) (m : Y ⟶ Z) [mono m] : Type u :=
{ x // ∃ y, m y = f x }


(Or perhaps the better setup would be for m to be the inclusion of a subtype too? Not sure.)

That's probably most natural to do after the more general case, though.

Sent.

Got it, thanks!

#### Greg Price (Mar 31 2021 at 07:42):

#6973

Last updated: May 07 2021 at 22:14 UTC