Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *)
(* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Inductive trunc_index := minus_two | trunc_S (_ : trunc_index).
Axiom IsTrunc : trunc_index -> Type -> Type.
Existing Class IsTrunc.
Axiom Contr : Type -> Type.
Inductive Trunc (n : trunc_index) (A :Type) : Type := tr : A -> Trunc n A.
Module NonPrim.
  Unset Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim _ _))).
    exact b.
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim _ _))).
    exact b.
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End NonPrim.

Module Prim.
  Set Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim _ _))).
    exact b.
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim _ _))).
    exact b.
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End Prim.