recognizing filtered colimits of types

src/category_theory/limits/types.lean

@@ -83,6 +83,20 @@ instance : has_colimits.{u} (Type u) :=
     (λ p, c.ι.app p.1 p.2)
     (λ p p' ⟨f, h⟩, by rw h; exact (functor_to_types.naturality _ _ c.ι f _).symm) := rfl
 
+lemma jointly_surjective (F : J ⥤ Type u) {t : limits.cocone F} (h : limits.is_colimit t)
+  (x : t.X) : ∃ j y, t.ι.app j y = x :=
+begin
+  suffices : (λ (x : t.X), ulift.up (∃ j y, t.ι.app j y = x)) = (λ _, ulift.up true),
+  { have := congr_fun this x,
+    have H := congr_arg ulift.down this,
+    dsimp at H,
+    rwa eq_true at H },
+  refine h.hom_ext _,
+  intro j, ext y,
+  erw iff_true,
+  exact ⟨j, y, rfl⟩
+end
+
 namespace filtered_colimit
 /- For filtered colimits of types, we can give an explicit description
   of the equivalence relation generated by the relation used to form
@@ -148,6 +162,37 @@ begin
   convert equiv.apply_eq_iff_eq e'.to_equiv _ _; rw ←e.hom.w; refl
 end
 
+variables (t)
+/-- Recognizing filtered colimits of types. -/
+noncomputable def is_colimit_of (hsurj : ∀ (x : t.X), ∃ i xi, x = t.ι.app i xi)
+  (hinj : ∀ i j xi xj, t.ι.app i xi = t.ι.app j xj →
+   ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj) : is_colimit t :=
+-- Strategy: Prove that the map from "the" colimit of F (defined above) to t.X
+-- is a bijection.
+begin
+  apply is_colimit.of_iso_colimit (colimit.is_colimit F),
+  refine cocones.ext (equiv.to_iso (equiv.of_bijective _)) _,
+  { exact colimit.desc F t },
+  { split,
+    { show function.injective _,
+      intros a b h,
+      rcases jointly_surjective F (colimit.is_colimit F) a with ⟨i, xi, rfl⟩,
+      rcases jointly_surjective F (colimit.is_colimit F) b with ⟨j, xj, rfl⟩,
+      change (colimit.ι F i ≫ colimit.desc F t) xi = (colimit.ι F j ≫ colimit.desc F t) xj at h,
+      rw [colimit.ι_desc, colimit.ι_desc] at h,
+      rcases hinj i j xi xj h with ⟨k, f, g, h'⟩,
+      change colimit.ι F i xi = colimit.ι F j xj,
+      rw [←colimit.w F f, ←colimit.w F g],
+      change colimit.ι F k (F.map f xi) = colimit.ι F k (F.map g xj),
+      rw h' },
+    { show function.surjective _,
+      intro x,
+      rcases hsurj x with ⟨i, xi, rfl⟩,
+      use colimit.ι F i xi,
+      simp } },
+  { intro j, apply colimit.ι_desc }
+end
+
 end filtered_colimit
 
 end category_theory.limits.types