{α : Sort u_1} →
  {β : Sort u_2} →
    {γ : Sort u_4} →
      {r : α → α → Prop} →
        {s : β → β → Prop} →
          Quot r →
            Quot s →
              (f : α → β → γ) →
                (∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
                  (∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) → γ