feat(category_theory/types): add explicit pullbacks in Type u (#6973)

Add an explicit construction of binary pullbacks in the
category of types.

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/pullbacks.20in.20Type.20u

src/category_theory/limits/shapes/pullbacks.lean

@@ -37,11 +37,11 @@ The type of objects for the diagram indexing a pullback, defined as a special ca
 abbreviation walking_cospan : Type v := wide_pullback_shape walking_pair
 
 /-- The left point of the walking cospan. -/
-abbreviation walking_cospan.left : walking_cospan := some walking_pair.left
+@[pattern] abbreviation walking_cospan.left : walking_cospan := some walking_pair.left
 /-- The right point of the walking cospan. -/
-abbreviation walking_cospan.right : walking_cospan := some walking_pair.right
+@[pattern] abbreviation walking_cospan.right : walking_cospan := some walking_pair.right
 /-- The central point of the walking cospan. -/
-abbreviation walking_cospan.one : walking_cospan := none
+@[pattern] abbreviation walking_cospan.one : walking_cospan := none
 
 /--
 The type of objects for the diagram indexing a pushout, defined as a special case of
@@ -50,23 +50,23 @@ The type of objects for the diagram indexing a pushout, defined as a special cas
 abbreviation walking_span : Type v := wide_pushout_shape walking_pair
 
 /-- The left point of the walking span. -/
-abbreviation walking_span.left : walking_span := some walking_pair.left
+@[pattern] abbreviation walking_span.left : walking_span := some walking_pair.left
 /-- The right point of the walking span. -/
-abbreviation walking_span.right : walking_span := some walking_pair.right
+@[pattern] abbreviation walking_span.right : walking_span := some walking_pair.right
 /-- The central point of the walking span. -/
-abbreviation walking_span.zero : walking_span := none
+@[pattern] abbreviation walking_span.zero : walking_span := none
 
 namespace walking_cospan
 
 /-- The type of arrows for the diagram indexing a pullback. -/
 abbreviation hom : walking_cospan → walking_cospan → Type v := wide_pullback_shape.hom
 
 /-- The left arrow of the walking cospan. -/
-abbreviation hom.inl : left ⟶ one := wide_pullback_shape.hom.term _
+@[pattern] abbreviation hom.inl : left ⟶ one := wide_pullback_shape.hom.term _
 /-- The right arrow of the walking cospan. -/
-abbreviation hom.inr : right ⟶ one := wide_pullback_shape.hom.term _
+@[pattern] abbreviation hom.inr : right ⟶ one := wide_pullback_shape.hom.term _
 /-- The identity arrows of the walking cospan. -/
-abbreviation hom.id (X : walking_cospan) : X ⟶ X := wide_pullback_shape.hom.id X
+@[pattern] abbreviation hom.id (X : walking_cospan) : X ⟶ X := wide_pullback_shape.hom.id X
 
 instance (X Y : walking_cospan) : subsingleton (X ⟶ Y) := by tidy
 
@@ -78,11 +78,11 @@ namespace walking_span
 abbreviation hom : walking_span → walking_span → Type v := wide_pushout_shape.hom
 
 /-- The left arrow of the walking span. -/
-abbreviation hom.fst : zero ⟶ left := wide_pushout_shape.hom.init _
+@[pattern] abbreviation hom.fst : zero ⟶ left := wide_pushout_shape.hom.init _
 /-- The right arrow of the walking span. -/
-abbreviation hom.snd : zero ⟶ right := wide_pushout_shape.hom.init _
+@[pattern] abbreviation hom.snd : zero ⟶ right := wide_pushout_shape.hom.init _
 /-- The identity arrows of the walking span. -/
-abbreviation hom.id (X : walking_span) : X ⟶ X := wide_pushout_shape.hom.id X
+@[pattern] abbreviation hom.id (X : walking_span) : X ⟶ X := wide_pushout_shape.hom.id X
 
 instance (X Y : walking_span) : subsingleton (X ⟶ Y) := by tidy
 
@@ -161,7 +161,7 @@ abbreviation snd (t : pullback_cone f g) : t.X ⟶ Y := t.π.app walking_cospan.
 
 /-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
     only asks for a proof of facts that carry any mathematical content -/
-def is_limit_aux (t : pullback_cone f g) (lift : Π (s : cone (cospan f g)), s.X ⟶ t.X)
+def is_limit_aux (t : pullback_cone f g) (lift : Π (s : pullback_cone f g), s.X ⟶ t.X)
   (fac_left : ∀ (s : pullback_cone f g), lift s ≫ t.fst = s.fst)
   (fac_right : ∀ (s : pullback_cone f g), lift s ≫ t.snd = s.snd)
   (uniq : ∀ (s : pullback_cone f g) (m : s.X ⟶ t.X)

src/category_theory/limits/shapes/types.lean

@@ -19,7 +19,11 @@ In this file, we provide definitions of the "standard" special shapes of limits
 giving the expected definitional implementation:
 * the terminal object is `punit`
 * the binary product of `X` and `Y` is `X × Y`
-* the product of a family `f : J → Type` is `Π j, f j`.
+* the product of a family `f : J → Type` is `Π j, f j`
+* the binary coproduct of `X` and `Y` is the sum type `X ⊕ Y`
+* the equalizer of a pair of maps `(g, h)` is the subtype `{x : Y // g x = h x}`
+* the pullback of `f : X ⟶ Z` and `g : Y ⟶ Z` is the subtype `{ p : X × Y // f p.1 = g p.2 }`
+  of the product
 
 Because these are not intended for use with the `has_limit` API,
 we instead construct terms of `limit_data`.
@@ -223,4 +227,76 @@ def equalizer_limit : limits.limit_cone (parallel_pair g h) :=
 
 end fork
 
+section pullback
+open category_theory.limits.walking_pair
+open category_theory.limits.walking_cospan
+open category_theory.limits.walking_cospan.hom
+
+variables {W X Y Z : Type u}
+variables (f : X ⟶ Z) (g : Y ⟶ Z)
+
+/--
+The usual explicit pullback in the category of types, as a subtype of the product.
+The full `limit_cone` data is bundled as `pullback_limit_cone f g`.
+-/
+@[nolint has_inhabited_instance]
+abbreviation pullback_obj : Type u := { p : X × Y // f p.1 = g p.2 }
+
+-- `pullback_obj f g` comes with a coercion to the product type `X × Y`.
+example (p : pullback_obj f g) : X × Y := p
+
+/--
+The explicit pullback cone on `pullback_obj f g`.
+This is bundled with the `is_limit` data as `pullback_limit_cone f g`.
+-/
+abbreviation pullback_cone : limits.pullback_cone f g :=
+pullback_cone.mk (λ p : pullback_obj f g, p.1.1) (λ p, p.1.2) (funext (λ p, p.2))
+
+/--
+The explicit pullback in the category of types, bundled up as a `limit_cone`
+for given `f` and `g`.
+-/
+@[simps]
+def pullback_limit_cone (f : X ⟶ Z) (g : Y ⟶ Z) : limits.limit_cone (cospan f g) :=
+{ cone := pullback_cone f g,
+  is_limit := pullback_cone.is_limit_aux _
+    (λ s x, ⟨⟨s.fst x, s.snd x⟩, congr_fun s.condition x⟩)
+    (by tidy)
+    (by tidy)
+    (λ s m w, funext $ λ x, subtype.ext $
+     prod.ext (congr_fun (w walking_cospan.left) x)
+              (congr_fun (w walking_cospan.right) x)) }
+
+/--
+The pullback cone given by the instance `has_pullbacks (Type u)` is isomorphic to the
+explicit pullback cone given by `pullback_limit_cone`.
+-/
+noncomputable def pullback_cone_iso_pullback : limit.cone (cospan f g) ≅ pullback_cone f g :=
+(limit.is_limit _).unique_up_to_iso (pullback_limit_cone f g).is_limit
+
+/--
+The pullback given by the instance `has_pullbacks (Type u)` is isomorphic to the
+explicit pullback object given by `pullback_limit_obj`.
+-/
+noncomputable def pullback_iso_pullback : pullback f g ≅ pullback_obj f g :=
+(cones.forget _).map_iso $ pullback_cone_iso_pullback f g
+
+@[simp] lemma pullback_iso_pullback_hom_fst (p : pullback f g) :
+  ((pullback_iso_pullback f g).hom p : X × Y).fst = (pullback.fst : _ ⟶ X) p :=
+congr_fun ((pullback_cone_iso_pullback f g).hom.w left) p
+
+@[simp] lemma pullback_iso_pullback_hom_snd (p : pullback f g) :
+  ((pullback_iso_pullback f g).hom p : X × Y).snd = (pullback.snd : _ ⟶ Y) p :=
+congr_fun ((pullback_cone_iso_pullback f g).hom.w right) p
+
+@[simp] lemma pullback_iso_pullback_inv_fst :
+  (pullback_iso_pullback f g).inv ≫ pullback.fst = (λ p, (p : X × Y).fst) :=
+(pullback_cone_iso_pullback f g).inv.w left
+
+@[simp] lemma pullback_iso_pullback_inv_snd :
+  (pullback_iso_pullback f g).inv ≫ pullback.snd = (λ p, (p : X × Y).snd) :=
+(pullback_cone_iso_pullback f g).inv.w right
+
+end pullback
+
 end category_theory.limits.types