We have seen that functions should be regarded as equal if they are homotopic. As usual in mathematics, we have a corresponding notion of equivalence between types, namely a function $f: A \to B$ is an equivalence if there is an inverse functions with compositions equal, i.e., homotopic, to the identity. However, if we naturally turn this into a type, the result (as we see below) is not wellbehaved. So we call this relation quasiequivalence.
1 2 

Instead, we define $f$ to be an equivalence if it has separate left and right equivalences. As we see in Algebra, this is an equivalent condition. However, this is better behaved in that the proofs of the proposition as types is generally unique in this formulation.
1 2 

## Exercise: Construct a function from $isEquiv(f)$ to $isQuasiEquiv(f)$.
An Equivalence
The function $not: Bool \to Bool$ is an equivalence, with itself as an inverse.
1 2 3 4 5 6 

Monodromy for QuasiEquivalences
We now see the subtle problem in using the relation that we called quasiequivalence. Consider the identity map on a type $A$. Let $g$ be an inverse of the identity, so that both conditions become $g \sim id$. However elements of the type are in general two proofs of $g \sim id$. For $a : A$, these are two paths from $a$ to $g(a)$. Combining these we get a path from $a$ to itself, the monodromy. In type theoretic terms, this is the following.
1 2 

Thus, for a point $a : A$, an element of $isQuasiEquiv(A)$ gives an element of $a = a$, i.e., a loop. If there are nontrivial loops in $A$, we have more than one proof that identity is an equivalence.