  Voevodsky 2015 introduces also a notion of equivalence between types, notion which generalizes in an uniform way the notions of logical equivalence between propositions, bijection between sets, categorical equivalence between groupoids, and so on. We say that a map \(f:A\rightarrow B\) is an equivalence if, for any element \(b\) in \(B\) the type of pairs \(a,p\) where \(p\) is of type \(\mathbf{Id}_B (f a,b)\), is a proposition and is inhabited. This expresses in a strong way that an element in \(B\) is the image of exactly one element in \(A\), and if \(A\) and \(B\) are sets, we recover the usual notion of bijection between sets. (In general if \(f:A\rightarrow B\) is an equivalence, then we have a map \(B\rightarrow A\), which can be thought of as the inverse of \(f\).) It can be shown for instance that the identity map is always an equivalence. Let \(\text{Equiv}(A,B)\) be the type of pairs \(f,p\) where \(f:A\rightarrow B\) and \(p\) is a proof that \(f\) is an equivalence. Using the fact that the identity map is an equivalence we have an element of \(\text{Equiv}(A,A)\) for any type \(A\). This implies that we have a map