∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : SizeOf C] [inst_4 : SizeOf D] [inst_5 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W x)] [inst_6 : SizeOf E]
  (inverts : W.IsInvertedBy L) (lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy F → CategoryTheory.Functor D E)
  (fac : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (lift F hF) = F)
  (uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂),
  sizeOf { inverts := inverts, lift := lift, fac := fac, uniq := uniq } = 1