proposition: Lemma Book_5_5 `{fs : Funext} : ~forall P : nat -> Type, IsEquiv (@ind_nat P).
proof: Proof. intro H. specialize (H (fun _ => Bool)). pose proof (eissect (@ind_nat (fun _ => Bool)) (true, (fun _ _ => true))) as H1. pose proof (eissect (@ind_nat (fun _ => Bool)) (true, (fun _ => idmap))) as H2. cut (ind_nat (fun _ : nat => Bool) (true, fun (_ : nat) (_ : Bool) => true) = (ind_nat (fun _ : nat => Bool) (true, fun _ : nat => idmap))). - intro H'. apply true_ne_false. exact (ap10 (apD10 (ap snd (H1^ @ ap _ H' @ H2)) 0) false). - apply path_forall. intro n; induction n; trivial. unfold ind_nat in *; simpl in *. rewrite <- IHn. destruct n; reflexivity. 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)