{P : Sort u} →
  {f : Type u₀ → Type u₁} →
    {g : Type v₀ → Type v₁} →
      {t : ULiftable f g} →
        {f' : Type u₀ → Type u₁} →
          {g' : Type v₀ → Type v₁} →
            {t' : ULiftable f' g'} → f = f' → g = g' → t ≍ t' → ULiftable.noConfusionType P t t'