A function f : X → Y : 𝑓 → 𝑋 𝑌 f:X\to Y is an equivalence if for every y : Y : 𝑦 𝑌 y:Y , the type of Fibres f − 1 ( y ) superscript 𝑓 1 𝑦 f^{-1}(y) is Contractible.