A function f : A → B : 𝑓 → 𝐴 𝐵 f:A\to B is surjective if for every b : B : 𝑏 𝐵 b:B , the type of Fibres f − 1 ( b ) superscript 𝑓 1 𝑏 f^{-1}(b) is Merely Inhabited.