diff options
author | 2014-04-08 01:42:49 -0400 | |
---|---|---|
committer | 2014-05-10 15:39:30 +0200 | |
commit | 3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (patch) | |
tree | b3a938d606daa421a6e8d566d69fdc93b99f88fd /test-suite/bugs/closed/HoTT_coq_027.v | |
parent | 3507f3d81082f5f4aef165cc3f4b0207224fb0cb (diff) |
Add more regression tests for univ poly/prim proj
hese 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 fails.
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.
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_027.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_027.v | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_027.v b/test-suite/bugs/closed/HoTT_coq_027.v new file mode 100644 index 000000000..8132f51d2 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_027.v @@ -0,0 +1,75 @@ +Set Implicit Arguments. +Generalizable All Variables. +Set Asymmetric Patterns. +Set Universe Polymorphism. + +Record Category (obj : Type) := { Morphism : obj -> obj -> Type }. + +Record Functor `(C : Category objC) `(D : Category objD) := + { ObjectOf :> objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }. + +Definition TypeCat : @Category Type := @Build_Category Type (fun s d => s -> d). +Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d). + +Definition FunctorToSet `(C : @Category objC) := Functor C SetCat. +Definition FunctorToType `(C : @Category objC) := Functor C TypeCat. + +(* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *) +Identity Coercion FunctorToType_Id : FunctorToType >-> Functor. + +Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C) +: FunctorToType C. + refine (@Build_Functor _ C _ TypeCat + (fun x => F.(ObjectOf) x) + (fun s d m => F.(MorphismOf) _ _ m)). +Defined. (* Toplevel input, characters 0-8: +Error: +The term + "fun (objC : Type) (C : Category objC) (F : FunctorToSet C) => + {| + ObjectOf := fun x : objC => F x; + MorphismOf := fun (s d : objC) (m : Morphism C s d) => MorphismOf F s d m |}" +has type + "forall (objC : Type) (C : Category objC), + FunctorToSet C -> Functor C TypeCat" while it is expected to have type + "forall (objC : Type) (C : Category objC), FunctorToSet C -> FunctorToType C". + *) + +Coercion FunctorTo_Set2Type : FunctorToSet >-> FunctorToType. + +Record GrothendieckPair `(C : @Category objC) (F : Functor C TypeCat) := + { GrothendieckC : objC; + GrothendieckX : F GrothendieckC }. + +Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) := + { SetGrothendieckC : objC; + SetGrothendieckX : F' SetGrothendieckC }. + +Section SetGrothendieckCoercion. + Context `(C : @Category objC). + Variable F : Functor C SetCat. + Let F' := (F : FunctorToSet _) : FunctorToType _. + + Set Printing Universes. + Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F' + := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}. + (* Toplevel input, characters 0-187: +Error: Illegal application: +The term "ObjectOf (* Top.8375 Top.8376 Top.8379 Set *)" of type + "forall (objC : Type (* Top.8375 *)) + (C : Category (* Top.8375 Top.8376 *) objC) (objD : Type (* Top.8379 *)) + (D : Category (* Top.8379 Set *) objD), + Functor (* Top.8375 Top.8376 Top.8379 Set *) C D -> objC -> objD" +cannot be applied to the terms + "objC" : "Type (* Top.8375 *)" + "C" : "Category (* Top.8375 Top.8376 *) objC" + "Type (* Set *)" : "Type (* Set+1 *)" + "TypeCat (* Top.8379 Set *)" : "Category (* Top.8379 Set *) Set" + "F'" : "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" + "SetGrothendieckC (* Top.8375 Top.8376 Top.8379 *) G" : "objC" +The 5th term has type "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C" +which should be coercible to + "Functor (* Top.8375 Top.8376 Top.8379 Set *) C TypeCat (* Top.8379 Set *)". + *) +End SetGrothendieckCoercion. |