Lemma bool_eq_distinct : bool_eq1 != bool_eq2. Proof. intro H. refine (transportf (λ t, bool_to_type (negb t)) (_ : false = true) tt). change true with (negb_weq false). change false with (idweq _ false). apply (maponpaths (λ (f : _ ≃ _), f _)). apply (invmaponpathsweq (invweq (univalence _ _))). exact H. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.NoInjectivePairing. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Core.Categories.