bug_failed_defined_01.v

(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "theories" "HoTT" "-top" "HoTTBookExercises") -*- *)
(* File reduced by coq-bug-finder from original input, then from 1168 lines to 33 lines, then from 138 lines to 34 lines, then from 220 lines to 35 lines, then from 93 lines to 37 lines, then from 118 lines to 41 lines, then from 293 lines to 52 lines, then from 350 lines to 86 lines, then from 126 lines to 85 lines, then from 296 lines to 119 lines *)
(* coqc version 8.5pl1 (June 2016) compiled on Jun 27 2016 15:21:22 with OCaml 4.02.3
   coqtop version 8.5pl1 (June 2016) *)
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require HoTT.Basics.Equivalences.
Module Export Trunc.
Import HoTT.Basics.Overture.
Import HoTT.Basics.Equivalences.
Generalizable Variables A B m n f.

Global Instance trunc_succ `{IsTrunc n A} : IsTrunc n.+1 A | 1000.
admit.
Defined.

Definition trunc_equiv A {B} (f : A -> B)
  `{IsTrunc n A} `{IsEquiv A B f}
  : IsTrunc n B.
Proof.
  generalize dependent B; generalize dependent A.
  simple_induction n n IH; simpl; intros A ? B f ?.
  -
 exact (contr_equiv _ f).
  -
 intros x y.
    exact (IH (f^-1 x = f^-1 y) (H (f^-1 x) (f^-1 y)) (x = y) ((ap (f^-1))^-1) _).
Qed.

Theorem path_ishprop `{H : IsHProp A} : forall x y : A, x = y.
Proof.
  apply H.
Defined.

Theorem hprop_allpath (A : Type) : (forall (x y : A), x = y) -> IsHProp A.
admit.
Defined.

End Trunc.

Export HoTT.Basics.Overture.

Module Export Forall.

Generalizable Variables A B f g e n.

Section AssumeFunext.
Context `{Funext}.

Global Instance contr_forall `{P : A -> Type} `{forall a, Contr (P a)}
  : Contr (forall a, P a) | 100.
Proof.
  exists (fun a => center (P a)).
  intro f.
 apply path_forall.
 intro a.
 apply contr.
Defined.

Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
  : IsTrunc n (forall a, P a) | 100.
Proof.
  generalize dependent P.
  simple_induction n n IH; simpl; intros P ?.

  -
 exact _.

  -
 intros f g; apply (trunc_equiv _ (apD10 ^-1)).
Defined.

End AssumeFunext.

End Forall.

Generalizable Variables A B C D f g n.

Section AssumeFunext.
Context `{Funext}.

Global Instance trunc_arrow {A B : Type} `{IsTrunc n B}
  : IsTrunc n (A -> B) | 100
:= trunc_forall.

End AssumeFunext.

Global Instance hprop_Empty : IsHProp Empty.
Proof.
intro x.
destruct x.
Defined.

Section Book_3_14.
  Context `{Funext}.
  Hypothesis LEM : forall A : Type, IsHProp A -> A + ~A.

  Definition Book_3_14
  : forall A (P : ~~A -> Type),
    (forall a, P (fun na => na a))
    -> (forall x y (z : P x) (w : P y), transport P (path_ishprop x y) z = w)
    -> forall x, P x.
  Proof.
    intros A P base p nna.
    assert (forall x, IsHProp (P x)).
    -
 intro x.
      apply hprop_allpath.
      intros x' y'.
      etransitivity; [ symmetry; apply (p x x y' x') | ].
      assert (H' : idpath = path_ishprop x x) by apply path_ishprop.
      destruct H'.
      reflexivity.
    -
 destruct (LEM (P nna) _) as [pnna|npnna]; trivial.
      refine (match _ : Empty with end).
      apply nna.
      intro a.
      apply npnna.
      exact (transport P (path_ishprop _ _) (base a)).
  Defined.