The lifting functor from `Type u` to `Type (max u v)` preserves limits and colimits.

ulift_functor_preserves_limits.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 cone_of_element {lc : cone (F ⋙ ulift_functor.{v u})} (x : lc.X) : cone F :=
{ X := punit, π :=
  { app := λ j _, (lc.π.app j x).down,
    naturality' := λ i j f, by { rw ← lc.w f, refl } } }

lemma preserves_limits : preserves_limits_of_size.{w' w} ulift_functor.{v u} :=
{ preserves_limits_of_shape := λ J _, by exactI { preserves_limit := λ F, { preserves := λ c h,
  { lift := λ lc, λ x, ⟨h.lift (cone_of_element x) punit.star⟩,
    fac' := λ lc j, by { ext, apply congr_fun (h.fac _ j) },
    uniq' := λ lc f hf, by { ext, apply congr_fun (h.uniq _ (λ _, (f x).down) _),
      intro j, ext ⟨⟩, have := congr_fun (hf j) x, exact congr_arg ulift.down this } } } } }

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

def set.cocone (s : set lc.X) : cocone F :=
{ X := ulift Prop, ι :=
  { app := λ j x, ⟨s $ lc.ι.app j ⟨x⟩⟩,
    naturality' := λ i j f, by { rw ← lc.w f, refl } } }

variables {c : cocone F} (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

def desc_set (s : set lc.X) : set c.X := λ x, (h.desc s.cocone x).down

lemma desc_set_spec (s : set c.X) (ls : set lc.X) :
  desc_set h ls = s ↔ ∀ j x, lc.ι.app j ⟨x⟩ ∈ ls ↔ c.ι.app j x ∈ s :=
begin
  split,
  { rintro rfl j x,
    exact (congr_arg ulift.down (congr_fun (h.fac ls.cocone j) x).symm).to_iff },
  { intro he, funext,
    have := congr_fun (h.uniq ls.cocone (λ x, ⟨s x⟩) (λ j, by {ext y, exact (he j y).symm})) x,
    exact (congr_arg ulift.down this).symm },
end

lemma desc_set_atom_iff (x : lc.X) (j : J) (y : F.obj j) :
  lc.ι.app j ⟨y⟩ = x ↔ c.ι.app j y ∈ desc_set h ({x} : set lc.X) :=
(desc_set_spec h _ ({x} : set lc.X)).1 rfl j y

variable (lc)

lemma desc_set_univ : desc_set h (set.univ : set lc.X) = set.univ := by simp [desc_set_spec]

lemma desc_set_atoms : (⋃ x, desc_set h ({x} : set lc.X)) = set.univ :=
begin
  symmetry, rw [← desc_set_univ lc h, desc_set_spec], intros j x,
  erw [true_iff, set.mem_Union], use lc.ι.app j ⟨x⟩, rw ← desc_set_atom_iff,
end

lemma desc_set_empty : desc_set h (∅ : set lc.X) = ∅ := by simp [desc_set_spec]

lemma desc_set_ne (x y : lc.X) (hn : x ≠ y) :
  desc_set h ({x} : set lc.X) ∩ desc_set h ({y} : set lc.X) = ∅ :=
begin
  symmetry, rw [← desc_set_empty lc h, desc_set_spec], intros j z,
  erw false_iff, rintro ⟨hx,hy⟩, rw ← desc_set_atom_iff at hx hy, exact hn (hx ▸ hy),
end

lemma uniq (x : c.X) : ∃! y, x ∈ desc_set h ({y} : set lc.X) :=
exists_unique_of_exists_of_unique
  (set.mem_Union.1 $ set.eq_univ_iff_forall.1 (desc_set_atoms lc h) x) $
  λ y₁ y₂ h₁ h₂, by_contra $ λ hn,
    set.eq_empty_iff_forall_not_mem.1 (desc_set_ne lc h y₁ y₂ hn) x ⟨h₁,h₂⟩

noncomputable def desc_fun (x : c.X) : lc.X := (uniq lc h x).exists.some

lemma desc_fun_app_spec (x : c.X) (y : lc.X) :
  desc_fun lc h x = y ↔ x ∈ desc_set h ({y} : set lc.X) :=
let hu := uniq lc h x, hm := hu.exists.some_spec in ⟨λ he, he ▸ hm, hu.unique hm⟩

lemma desc_fun_spec (f : c.X → lc.X) :
  f = desc_fun lc h ↔ ∀ j, f ∘ c.ι.app j = lc.ι.app j ∘ ulift.up :=
⟨by { rintro rfl j, ext, apply (desc_fun_app_spec lc h _ _).2, rw ← desc_set_atom_iff },
 by { intro he, ext, symmetry, apply (desc_fun_app_spec lc h _ _).2,
   rw [(joint_surj h x).some_spec.some_spec, ← desc_set_atom_iff],
   exact (congr_fun (he _) _).symm }⟩

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 x, desc_fun lc h x.down,
    fac' := λ lc j, by { ext ⟨⟩, apply congr_fun ((desc_fun_spec lc h _).1 rfl j) },
    uniq' := λ lc f hf, by { ext ⟨⟩, apply congr_fun ((desc_fun_spec lc h (f ∘ ulift.up)).2 _),
      intro j, ext y, apply congr_fun (hf j) ⟨y⟩ } } } } }