Another proof that ulift_functor preserves colimits, further removed from boolean algebras.

ulift_functor_preserves_colimits.lean

import category_theory.limits.preserves.basic
open category_theory category_theory.limits opposite
universes u v w w'
variables {J : Type w} [category.{w'} J] (F : J ⥤ Type u)

def real_colim := quot (λ x y : (Σ j, F.obj j), ∃ f : x.1 ⟶ y.1, F.map f x.2 = y.2)

variables {F} (c: cocone F) (lc : cocone (F ⋙ ulift_functor.{v u}))

def mk_colim (j : J) (x : F.obj j) : real_colim F := quot.mk _ ⟨j,x⟩

@[simps] def cocone_of_fun {α : Type u} (f : real_colim F → α) : cocone F :=
{ X := α, ι :=
  { app := λ j, f ∘ mk_colim j,
    naturality' := λ i j f, by { ext, dsimp, congr' 1, symmetry, apply quot.sound, use f } } }

def sigma_to_X (x : Σ j, F.obj j) : c.X := c.ι.app x.1 x.2
def sigma_to_lX (x : Σ j, F.obj j) : lc.X := lc.ι.app x.1 ⟨x.2⟩

def colim_to_X : real_colim F → c.X :=
quot.lift (sigma_to_X c) (by { rintros x y ⟨f,h⟩,
  dsimp [sigma_to_X], rw ← h, have := c.w f, exact (congr_fun this x.2).symm })

def colim_to_lX : real_colim F → lc.X :=
quot.lift (sigma_to_lX lc) (by { rintros x y ⟨f,h⟩, 
  dsimp [sigma_to_lX], rw ← h, have := lc.w f, exact (congr_fun this ⟨x.2⟩).symm })

lemma lfac (j : J) (x : F.obj j) : colim_to_lX lc (mk_colim j x) = lc.ι.app j ⟨x⟩ := rfl

variables {c} (h : is_colimit c)
include h

lemma joint_surj (x : c.X) : ∃ j y, x = c.ι.app j y :=
begin
  by_contra hx, push_neg at hx, apply (_ : (λ y, ulift.up true) ≠ λ y, ⟨x ≠ y⟩),
  { apply h.hom_ext, intro j, ext y, exact (true_iff _).2 (hx j y) },
  { exact λ he, let he' := congr_fun he x in cast eq_true (congr_arg ulift.down he').symm rfl },
end

lemma colim_to_X_surj : function.surjective (colim_to_X c) :=
λ x, let ⟨j,y,hy⟩ := joint_surj h x in ⟨quot.mk _ ⟨j,y⟩, hy.symm⟩

lemma colim_to_X_inj : function.injective (colim_to_X c) :=
λ x y he, let cc := cocone_of_fun (λ z, ulift.up (x = z)) in -- uses `ulift Prop : Type v` here
begin
  have hc : ∀ z, h.desc cc (colim_to_X c z) = ⟨x = z⟩,
  { rintro ⟨⟨j,z⟩⟩, exact congr_fun (h.fac cc j) z },
  have := congr_arg (ulift.down ∘ h.desc cc) he,
  dsimp at this, rw [hc,hc] at this, exact cast this rfl,
end

noncomputable def X_equiv_colim : c.X ≃ real_colim F :=
(equiv.of_bijective (colim_to_X c) ⟨colim_to_X_inj h, colim_to_X_surj h⟩).symm

lemma fac (j : J) (x : F.obj j) : X_equiv_colim h (c.ι.app j x) = mk_colim j x :=
by { apply_fun colim_to_X c, apply equiv.of_bijective_apply_symm_apply, apply colim_to_X_inj h }

noncomputable def preserves_colimits : preserves_colimits_of_size.{w' w} ulift_functor.{v u} :=
{ preserves_colimits_of_shape := λ J _, by exactI { preserves_colimit := λ F, { preserves := λ c h,
  { desc := λ lc, colim_to_lX lc ∘ X_equiv_colim h ∘ ulift.down,
    fac' := λ lc j, by { ext ⟨⟩, dsimp, rw [fac, lfac] },
    uniq' := λ lc f hf, by { ext ⟨⟩, rw (joint_surj h x).some_spec.some_spec,
      dsimp, rw [fac, lfac], exact congr_fun (hf _) ⟨_⟩ } } } } }