proposition: Lemma Book_3_11 `{Univalence} : ~ (forall A, Trunc (-1) A -> A).
proof: Proof. intros g. assert (end_contr : forall A, Contr (Trunc (-1) A -> Trunc (-1) A)). { intros A. apply Book_3_4_solution_1. apply istrunc_truncation. } pose (contr b := (not_fixed_negb (g Bool b)) (happly (univalence_func_natural_equiv _ end_contr g equiv_negb) b)). contradiction (contr (tr true)). Defined.
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)