From d1a39e06c44dc451d8a56a286017885d400ac435 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 6 May 2014 09:51:21 -0400
Subject: Add regression tests for univ. poly. and prim proj

These regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.
These are the tests that trunk currently passes.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.
---
 test-suite/bugs/closed/HoTT_coq_112.v | 75 +++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_112.v

(limited to 'test-suite/bugs/closed/HoTT_coq_112.v')

diff --git a/test-suite/bugs/closed/HoTT_coq_112.v b/test-suite/bugs/closed/HoTT_coq_112.v
new file mode 100644
index 000000000..150f2ecc8
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_112.v
@@ -0,0 +1,75 @@
+(* File reduced by coq-bug-finder from 4464 lines to 4137 lines, then from 3683 lines to 118 lines, then from 124 lines to 75 lines. *)
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : forall x, f (equiv_inv x) = x
+}.
+
+Arguments eisretr {A B} f {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun :> A -> B ;
+  equiv_isequiv :> IsEquiv equiv_fun
+}.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+Local Open Scope equiv_scope.
+
+Instance isequiv_path {A B : Type} (p : A = B)
+  : IsEquiv (transport (fun X:Type => X) p) | 0
+  := admit.
+Definition equiv_path (A B : Type) (p : A = B) : A <~> B
+  := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
+
+Class Univalence := {
+  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+}.
+
+Section Univalence.
+  Context `{Univalence}.
+
+  Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
+    := (equiv_path A B)^-1 f.
+
+  Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B)
+    := path_universe_uncurried (BuildEquiv _ _ f feq).
+
+  Set Printing Universes.
+  Definition transport_path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
+  : transport (fun X:Type => X) (path_universe f) z = f z
+    := apD10 (ap (equiv_fun A B) (eisretr (equiv_path A B) (BuildEquiv _ _ f feq))) z.
+  (* Toplevel input, characters 0-231:
+Error: Illegal application:
+The term "isequiv_equiv_path (* Top.1003 Top.1003 Top.1001 Top.997 *)"
+of type
+ "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *) ->
+  forall (A : Type (* Top.1003 *)) (B : Type (* Top.997 *)),
+  IsEquiv (* Top.1003 Top.1001 *)
+    (equiv_path (* Top.997 Top.1003 Top.1001 Top.1003 *) A B)"
+cannot be applied to the terms
+ "H" : "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
+ "A" : "Type (* Top.996 *)"
+ "B" : "Type (* Top.997 *)"
+The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
+which should be coercible to
+ "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)".
+ *)
-- 
cgit v1.2.3