diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 12:33:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 13:10:02 +0200 |
| commit | 7a68038054193f5e392d75d7f11eb8f272727d6b (patch) | |
| tree | 53bbecba9460c1fc0950c14c315800f0913ea83e | |
| parent | 9753da73ed9f1e12d16b7d9b66d0c68b1d015918 (diff) | |
The uses of the funext axiom forced levels to Set, relaxing its use doesn't.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_064.v | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v index fe9773ecd..5f0a541b0 100644 --- a/test-suite/bugs/closed/HoTT_coq_064.v +++ b/test-suite/bugs/closed/HoTT_coq_064.v @@ -34,8 +34,9 @@ Module Export Overture. Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope. - Class Funext := - { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }. + Class Funext. + Axiom isequiv_apD10 : `{Funext} -> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) . + Existing Instance isequiv_apD10. Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : (forall x, f x = g x) -> f = g @@ -164,13 +165,14 @@ Definition pullback_along `{Funext} (C C' D : PreCategory) (p : Functor C C') : object ((C' -> D) -> (C -> D)) := Eval hnf in compose_functor _ _ _ p. -Definition IsColimit `{Funext} C D (F : Functor D C) (x : object - (@comma_category (indiscrete_category Unit) - (@functor_category H (indiscrete_category Unit) C) - (@functor_category H D C) - admit - (@pullback_along H D (indiscrete_category Unit) C - admit))) : Type +Definition IsColimit `{Funext} C D (F : Functor D C) + (x : object + (@comma_category (indiscrete_category Unit) + (@functor_category H (indiscrete_category Unit) C) + (@functor_category H D C) + admit + (@pullback_along H D (indiscrete_category Unit) C + admit))) : Type := admit. Generalizable All Variables. |