summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3480.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3480.v
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3480.v')
-rw-r--r--test-suite/bugs/closed/3480.v47
1 files changed, 47 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3480.v b/test-suite/bugs/closed/3480.v
new file mode 100644
index 00000000..99ac2efa
--- /dev/null
+++ b/test-suite/bugs/closed/3480.v
@@ -0,0 +1,47 @@
+Set Primitive Projections.
+Axiom admit : forall {T}, T.
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+Open Scope fibration_scope.
+Notation "x .1" := (projT1 x) (at level 3) : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Set Implicit Arguments.
+Delimit Scope category_scope with category.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Local Open Scope category_scope.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
+Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :> @morphism C s d ; isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+Definition idtoiso (C : PreCategory) (x y : C) (H : x = y) : Isomorphic x y := admit.
+Record NotionOfStructure (X : PreCategory) := { structure :> X -> Type }.
+Record Smorphism (X : PreCategory) (P : NotionOfStructure X) (xa yb : { x : X & P x }) := { f : morphism X xa.1 yb.1 }.
+Definition precategory_of_structures X (P : NotionOfStructure X) : PreCategory.
+Proof.
+ refine (@Build_PreCategory _ (@Smorphism _ P)).
+Defined.
+Section sip.
+ Variable X : PreCategory.
+ Variable P : NotionOfStructure X.
+
+ Let StrX := @precategory_of_structures X P.
+
+ Definition sip_isotoid (xa yb : StrX) (f : xa <~=~> yb) : xa = yb.
+ admit.
+ Defined.
+
+ Lemma structure_identity_principle_helper (xa yb : StrX)
+ (x : xa <~=~> yb) : Smorphism P xa yb.
+ Proof.
+ refine ((idtoiso (precategory_of_structures P) (sip_isotoid x) : @morphism _ _ _) : morphism _ _ _).
+(* Toplevel input, characters 24-95:
+Error:
+In environment
+X : PreCategory
+P : NotionOfStructure X
+StrX := precategory_of_structures P : PreCategory
+xa : object StrX
+yb : object StrX
+x : xa <~=~> yb
+The term "morphism_isomorphic:@morphism (precategory_of_structures P) xa yb"
+has type "@morphism (precategory_of_structures P) xa yb"
+while it is expected to have type "morphism ?40 ?41 ?42". *) \ No newline at end of file