# Law of the Excluded Middle for Mere Propositions

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}$$?

• You are correct that we cannot prove LEM from univalence. In order to actually prove this, one would need to come up with a model or interpretation of homotopy type theory in which LEM is not true. This is a pretty technical topic - you'll probably want to ask on MathOverflow, but be prepared for a highly technical counterexample. Also, the HoTT book generally avoids assuming LEM - in fact, large parts of the book are designed specifically to avoid LEM, such as the section on the Cauchy reals higher inductive definition. Mar 16, 2021 at 1:04
• Ok, thank you for your response. Mar 16, 2021 at 4:03

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.