pullbacks in Type u

Stream: Is there code for X?

[Greg Price]

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]

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]

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?

[Scott Morrison]

What's your github username?

[Greg Price]

gnprice

[Greg Price]

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.

[Scott Morrison]

Sent.

[Greg Price]

Got it, thanks!

[Greg Price]

#6973