proposition: Lemma Book_6_9_not_id {ua : Univalence} `{fs : Funext} : Book_6_9 Bool = negb.
proof: Proof. apply path_forall; intro b. unfold Book_6_9. destruct (@LEM (Contr { f : Bool <~> Bool & ~(forall x, f x = x) }) _) as [C|H']. - set (f := @center _ C). pose proof (bool_map_equiv_not_idmap f b). destruct (f.1 b), b; match goal with | _ => assumption | _ => reflexivity | [ H : ~(_ = _) |- _ ] => exact (match H idpath with end) | [ H : true = false |- _ ] => exact (match true_ne_false H with end) | [ H : false = true |- _ ] => exact (match false_ne_true H with end) end. - refine (match H' _ with end). apply (Build_Contr _ (exist (fun f : Bool <~> Bool => ~(forall x, f x = x)) (Build_Equiv _ _ negb _) (fun H => false_ne_true (H true)))); simpl. intro f. apply path_sigma_uncurried; simpl. refine ((fun H'' => (equiv_path_equiv _ _ H''; path_ishprop _ _)) _); simpl. apply path_forall; intro b'. pose proof (bool_map_equiv_not_idmap f b'). destruct (f.1 b'), b'; match goal with | _ => assumption | _ => reflexivity | [ H : ~(_ = _) |- _ ] => exact (match H idpath with end) | [ H : true = false |- _ ] => exact (match true_ne_false H with end) | [ H : false = true |- _ ] => exact (match false_ne_true H with end) end. Qed.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)