Lemma complementaryDecisions (C : ComplementaryPair) : iscontr (isTrue C ⨿ isFalse C). Proof. intros. apply iscontrifweqtounit. assert (w := weqcoprodsplit (λ _:unit, chooser C)). apply invweq. apply (weqcomp w). apply weqcoprodf; apply weqhfiberunit. Defined.
Require Import UniMath.MoreFoundations.Tactics.