In the Homotopy Type Theory book, they define the (non-contradictory) law of the excluded middle as $$\operatorname{LEM}:\prod_{A:\mathcal U}\big(\operatorname{isProp}(A)\to(A+\lnot A)\big).\tag{3.4.1}$$ Here, $\operatorname{isProp}(A)$ is the assertion that all elements of $A$ are propositionally equal. The book goes on to treat this as an axiom; I'm guessing this means that $\operatorname{LEM}$ does not follow from univalence but would like confirmation.
Additionally, how would we go about showing that we cannot exhibit $\operatorname{LEM}$?
As Mark says, univalence does not imply LEM, and one way to prove this is to exhibit a model satisfying univalence but not LEM. To my knowledge the first such model was constructed in my paper Univalence for inverse diagrams and homotopy canonicity, and is not that complicated to describe: given essentially any model of HoTT, one can construct a new model in which the types are pairs $(A_0,A_1)$ where $A_0$ is a type in the old model and $A_1$ is an $A_0$-indexed family of types in the old model. This new model, called the "Sierpinski topos" over the old model, violates LEM, because it has three different closed propositions: $0=(0,0)$, $1=(1,1)$, but also $(1,0)$. It's based on the "simplest Kripke model" for set-based constructive mathematics. Now we know there are many other models too, including models in all higher toposes and also cubical set models that are computational.