Surjection_iff_Right_Cancellable

import Mathlib.Logic.Function.Basic

theorem Surjection_iff_Right_Cancellable {α β : Type _} (f : α → β) : Function.Surjective f ↔ ∀ (γ : Type _) (g₁ g₂ : β → γ), g₁ ∘ f = g₂ ∘ f → g₁ = g₂ := by sorry