From 14ae5f4534ee5e632d82990e7db76305b9ca9b75 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 21 Jun 2014 16:14:59 +0200 Subject: - Add an option to refresh only algebraic universes, for e_type_of. The goal there is not the same as in Evd.define. - Fixed bugs #3330 and #3331. --- test-suite/bugs/closed/3330.v | 1105 +++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/3331.v | 31 ++ test-suite/bugs/opened/3330.v | 1083 ---------------------------------------- test-suite/bugs/opened/3331.v | 36 -- 4 files changed, 1136 insertions(+), 1119 deletions(-) create mode 100644 test-suite/bugs/closed/3330.v create mode 100644 test-suite/bugs/closed/3331.v delete mode 100644 test-suite/bugs/opened/3330.v delete mode 100644 test-suite/bugs/opened/3331.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v new file mode 100644 index 0000000000..0bd3033acb --- /dev/null +++ b/test-suite/bugs/closed/3330.v @@ -0,0 +1,1105 @@ +(* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) +Set Universe Polymorphism. +Definition setleq (A : Type@{i}) (B : Type@{j}) := A : Type@{j}. + +Inductive foo : Type@{l} := bar : foo . +Section MakeEq. + Variables (a : foo@{i}) (b : foo@{j}). + + Let t := $(let ty := type of b in exact ty)$. + Definition make_eq (x:=b) := a : t. +End MakeEq. + +Definition same (x : foo@{i}) (y : foo@{i}) := x. + +Section foo. + + Variables x : foo@{i}. + Variables y : foo@{j}. + + Let AleqB := let foo := make_eq x y in (Type * Type)%type. + + Definition baz := same x y. +End foo. + +Definition baz' := Eval unfold baz in baz@{i j k l}. + +Module Export HoTT_DOT_Overture. +Module Export HoTT. +Module Export Overture. + +Definition relation (A : Type) := A -> A -> Type. +Class Symmetric {A} (R : relation A) := + symmetry : forall x y, R x y -> R y x. + +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := + fun x => g (f x). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. + +Open Scope function_scope. + +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. + +Delimit Scope path_scope with path. + +Local Open Scope path_scope. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p q) (at level 20) : path_scope. + +Notation "p ^" := (inverse p) (at level 3) : path_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 pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type + := forall x:A, f x = g x. + +Hint Unfold pointwise_paths : typeclass_instances. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) + : f == g + := fun x => match h with idpath => 1 end. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Delimit Scope equiv_scope with equiv. + +Local Open Scope equiv_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Fixpoint nat_to_trunc_index (n : nat) : trunc_index + := match n with + | 0 => trunc_S (trunc_S minus_two) + | S n' => trunc_S (nat_to_trunc_index n') + end. + +Coercion nat_to_trunc_index : nat >-> trunc_index. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation IsHSet := (IsTrunc 0). + +Class Funext := + { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }. + +Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : + f == g -> f = g + := + (@apD10 A P f g)^-1. + +End Overture. + +End HoTT. + +End HoTT_DOT_Overture. + +Module Export HoTT_DOT_categories_DOT_Category_DOT_Core. + +Module Export HoTT. +Module Export categories. +Module Export Category. +Module Export Core. +Set Universe Polymorphism. + +Set Implicit Arguments. +Delimit Scope morphism_scope with morphism. + +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. + +Record PreCategory := + Build_PreCategory' { + object :> Type; + morphism : object -> object -> Type; + + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1); + + associativity_sym : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + m3 o (m2 o m1) = (m3 o m2) o m1; + + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f; + + identity_identity : forall x, identity x o identity x = identity x; + + trunc_morphism : forall s d, IsHSet (morphism s d) + }. + +Bind Scope category_scope with PreCategory. + +Arguments identity [!C%category] x%object : rename. +Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Definition Build_PreCategory + object morphism compose identity + associativity left_identity right_identity + := @Build_PreCategory' + object + morphism + compose + identity + associativity + (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _)) + left_identity + right_identity + (fun _ => left_identity _ _ _). + +Existing Instance trunc_morphism. + +Hint Resolve @left_identity @right_identity @associativity : category morphism. + +Module Export CategoryCoreNotations. + + Infix "o" := compose : morphism_scope. +End CategoryCoreNotations. +End Core. + +End Category. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Category_DOT_Core. + +Module Export HoTT_DOT_types_DOT_Forall. + +Module Export HoTT. +Module Export types. +Module Export Forall. +Generalizable Variables A B f g e n. + +Section AssumeFunext. + +Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)} + : IsTrunc n (forall a, P a) | 100. + +admit. +Defined. +End AssumeFunext. + +End Forall. + +End types. + +End HoTT. + +End HoTT_DOT_types_DOT_Forall. + +Module Export HoTT_DOT_types_DOT_Prod. + +Module Export HoTT. +Module Export types. +Module Export Prod. +Local Open Scope path_scope. + +Definition path_prod_uncurried {A B : Type} (z z' : A * B) + (pq : (fst z = fst z') * (snd z = snd z')) + : (z = z') + := match pq with (p,q) => + match z, z' return + (fst z = fst z') -> (snd z = snd z') -> (z = z') with + | (a,b), (a',b') => fun p q => + match p, q with + idpath, idpath => 1 + end + end p q + end. + +Definition path_prod {A B : Type} (z z' : A * B) : + (fst z = fst z') -> (snd z = snd z') -> (z = z') + := fun p q => path_prod_uncurried z z' (p,q). + +Definition path_prod' {A B : Type} {x x' : A} {y y' : B} + : (x = x') -> (y = y') -> ((x,y) = (x',y')) + := fun p q => path_prod (x,y) (x',y') p q. + +End Prod. + +End types. + +End HoTT. + +End HoTT_DOT_types_DOT_Prod. + +Module Export HoTT_DOT_categories_DOT_Functor_DOT_Core. + +Module Export HoTT. +Module Export categories. +Module Export Functor. +Module Export Core. +Set Universe Polymorphism. + +Set Implicit Arguments. +Delimit Scope functor_scope with functor. + +Local Open Scope morphism_scope. + +Section Functor. + + Variable C : PreCategory. + Variable D : PreCategory. + + Record Functor := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d); + composition_of : forall s d d' + (m1 : morphism C s d) (m2: morphism C d d'), + morphism_of _ _ (m2 o m1) + = (morphism_of _ _ m2) o (morphism_of _ _ m1); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. + +End Functor. +Bind Scope functor_scope with Functor. + +Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. +Module Export FunctorCoreNotations. + + Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. +End FunctorCoreNotations. +End Core. + +End Functor. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Functor_DOT_Core. + +Module Export HoTT_DOT_categories_DOT_Category_DOT_Morphisms. + +Module Export HoTT. +Module Export categories. +Module Export Category. +Module Export Morphisms. +Set Universe Polymorphism. + +Local Open Scope morphism_scope. + +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := + { + morphism_inverse : morphism C d s; + left_inverse : morphism_inverse o m = identity _; + right_inverse : m o morphism_inverse = identity _ + }. + +Class Isomorphic {C : PreCategory} s d := + { + morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic + }. + +Module Export CategoryMorphismsNotations. + + Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope. + +End CategoryMorphismsNotations. +End Morphisms. + +End Category. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Category_DOT_Morphisms. + +Module Export HoTT_DOT_categories_DOT_Category_DOT_Dual. + +Module Export HoTT. +Module Export categories. +Module Export Category. +Module Export Dual. +Set Universe Polymorphism. + +Local Open Scope morphism_scope. + +Section opposite. + + Definition opposite (C : PreCategory) : PreCategory + := @Build_PreCategory' + C + (fun s d => morphism C d s) + (identity (C := C)) + (fun _ _ _ m1 m2 => m2 o m1) + (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _) + (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _) + (fun _ _ => @right_identity _ _ _) + (fun _ _ => @left_identity _ _ _) + (@identity_identity C) + _. +End opposite. + +Module Export CategoryDualNotations. + + Notation "C ^op" := (opposite C) (at level 3) : category_scope. +End CategoryDualNotations. +End Dual. + +End Category. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Category_DOT_Dual. + +Module Export HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core. + +Module Export HoTT. +Module Export categories. +Module Export Functor. +Module Export Composition. +Module Export Core. +Set Universe Polymorphism. + +Set Implicit Arguments. +Local Open Scope morphism_scope. + +Section composition. + + Variable C : PreCategory. + Variable D : PreCategory. + Variable E : PreCategory. + Variable G : Functor D E. + Variable F : Functor C D. + + Local Notation c_object_of c := (G (F c)) (only parsing). + + Local Notation c_morphism_of m := (morphism_of G (morphism_of F m)) (only parsing). + + Let compose_composition_of' s d d' + (m1 : morphism C s d) (m2 : morphism C d d') + : c_morphism_of (m2 o m1) = c_morphism_of m2 o c_morphism_of m1. +admit. +Defined. + Definition compose_composition_of s d d' m1 m2 + := Eval cbv beta iota zeta delta + [compose_composition_of'] in + @compose_composition_of' s d d' m1 m2. + Let compose_identity_of' x + : c_morphism_of (identity x) = identity (c_object_of x). + +admit. +Defined. + Definition compose_identity_of x + := Eval cbv beta iota zeta delta + [compose_identity_of'] in + @compose_identity_of' x. + Definition compose : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => morphism_of G (morphism_of F m)) + compose_composition_of + compose_identity_of. + +End composition. +Module Export FunctorCompositionCoreNotations. + + Infix "o" := compose : functor_scope. +End FunctorCompositionCoreNotations. +End Core. + +End Composition. + +End Functor. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core. + +Module Export HoTT_DOT_categories_DOT_Functor_DOT_Dual. + +Module Export HoTT. +Module Export categories. +Module Export Functor. +Module Export Dual. +Set Universe Polymorphism. + +Set Implicit Arguments. + +Section opposite. + + Variable C : PreCategory. + Variable D : PreCategory. + Definition opposite (F : Functor C D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). + +End opposite. +Module Export FunctorDualNotations. + + Notation "F ^op" := (opposite F) : functor_scope. +End FunctorDualNotations. +End Dual. + +End Functor. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Functor_DOT_Dual. + +Module Export HoTT_DOT_categories_DOT_Functor_DOT_Identity. + +Module Export HoTT. +Module Export categories. +Module Export Functor. +Module Export Identity. +Set Universe Polymorphism. + +Section identity. + + Definition identity C : Functor C C + := Build_Functor C C + (fun x => x) + (fun _ _ x => x) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). +End identity. +Module Export FunctorIdentityNotations. + + Notation "1" := (identity _) : functor_scope. +End FunctorIdentityNotations. +End Identity. + +End Functor. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Functor_DOT_Identity. + +Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core. + +Module Export HoTT. +Module Export categories. +Module Export NaturalTransformation. +Module Export Core. +Set Universe Polymorphism. + +Set Implicit Arguments. +Local Open Scope morphism_scope. + +Section NaturalTransformation. + + Variable C : PreCategory. + Variable D : PreCategory. + Variables F G : Functor C D. + + Record NaturalTransformation := + Build_NaturalTransformation' { + components_of :> forall c, morphism D (F c) (G c); + commutes : forall s d (m : morphism C s d), + components_of d o F _1 m = G _1 m o components_of s; + + commutes_sym : forall s d (m : C.(morphism) s d), + G _1 m o components_of s = components_of d o F _1 m + }. + +End NaturalTransformation. +End Core. + +End NaturalTransformation. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core. + +Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual. + +Module Export HoTT. +Module Export categories. +Module Export NaturalTransformation. +Module Export Dual. +Set Universe Polymorphism. + +Section opposite. + + Variable C : PreCategory. + Variable D : PreCategory. + + Definition opposite + (F G : Functor C D) + (T : NaturalTransformation F G) + : NaturalTransformation G^op F^op + := Build_NaturalTransformation' (G^op) (F^op) + (components_of T) + (fun s d => commutes_sym T d s) + (fun s d => commutes T d s). + +End opposite. + +End Dual. + +End NaturalTransformation. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual. + +Module Export HoTT_DOT_categories_DOT_Category_DOT_Strict. + +Module Export HoTT. +Module Export categories. +Module Export Category. +Module Export Strict. + +Export Category.Core. +Set Universe Polymorphism. + +End Strict. + +End Category. + +End categories. + +End HoTT. + +End HoTT_DOT_categories_DOT_Category_DOT_Strict. + +Module Export HoTT. +Module Export categories. +Module Export Category. +Module Export Prod. +Set Universe Polymorphism. + +Local Open Scope morphism_scope. + +Section prod. + + Variable C : PreCategory. + Variable D : PreCategory. + Definition prod : PreCategory. + + refine (@Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + (fun x => (identity (fst x), identity (snd x))) + (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) + _ + _ + _ + _); admit. + Defined. +End prod. +Module Export CategoryProdNotations. + + Infix "*" := prod : category_scope. +End CategoryProdNotations. +End Prod. + +End Category. + +End categories. + +End HoTT. + +Module Functor. +Module Export Prod. +Set Universe Polymorphism. + +Set Implicit Arguments. +Local Open Scope morphism_scope. + +Section proj. + + Context {C : PreCategory}. + Context {D : PreCategory}. + Definition fst : Functor (C * D) C + := Build_Functor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). + + Definition snd : Functor (C * D) D + := Build_Functor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). + +End proj. + +Section prod. + + Variable C : PreCategory. + Variable D : PreCategory. + Variable D' : PreCategory. + Definition prod (F : Functor C D) (F' : Functor C D') + : Functor C (D * D') + := Build_Functor + C (D * D') + (fun c => (F c, F' c)) + (fun s d m => (F _1 m, F' _1 m)) + (fun _ _ _ _ _ => path_prod' (composition_of F _ _ _ _ _) + (composition_of F' _ _ _ _ _)) + (fun _ => path_prod' (identity_of F _) (identity_of F' _)). + +End prod. +Local Infix "*" := prod : functor_scope. + +Section pair. + + Variable C : PreCategory. + Variable D : PreCategory. + Variable C' : PreCategory. + Variable D' : PreCategory. + Variable F : Functor C D. + Variable F' : Functor C' D'. + Definition pair : Functor (C * C') (D * D') + := (F o fst) * (F' o snd). + +End pair. + +Module Export FunctorProdNotations. + + Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : functor_scope. +End FunctorProdNotations. +End Prod. + +End Functor. + +Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core. + +Module Export HoTT. +Module categories. +Module Export NaturalTransformation. +Module Export Composition. +Module Export Core. +Set Universe Polymorphism. + +Set Implicit Arguments. +Local Open Scope path_scope. + +Local Open Scope morphism_scope. + +Section composition. + + Section compose. + Variable C : PreCategory. + Variable D : PreCategory. + Variables F F' F'' : Functor C D. + Variable T' : NaturalTransformation F' F''. + + Variable T : NaturalTransformation F F'. + Local Notation CO c := (T' c o T c). + + Definition compose_commutes s d (m : morphism C s d) + : CO d o morphism_of F m = morphism_of F'' m o CO s + := (associativity _ _ _ _ _ _ _ _) + @ ap (fun x => _ o x) (commutes T _ _ m) + @ (associativity_sym _ _ _ _ _ _ _ _) + @ ap (fun x => x o _) (commutes T' _ _ m) + @ (associativity _ _ _ _ _ _ _ _). + + Definition compose_commutes_sym s d (m : morphism C s d) + : morphism_of F'' m o CO s = CO d o morphism_of F m + := (associativity_sym _ _ _ _ _ _ _ _) + @ ap (fun x => x o _) (commutes_sym T' _ _ m) + @ (associativity _ _ _ _ _ _ _ _) + @ ap (fun x => _ o x) (commutes_sym T _ _ m) + @ (associativity_sym _ _ _ _ _ _ _ _). + + Definition compose + : NaturalTransformation F F'' + := Build_NaturalTransformation' F F'' + (fun c => CO c) + compose_commutes + compose_commutes_sym. + + End compose. + End composition. +Module Export NaturalTransformationCompositionCoreNotations. + + Infix "o" := compose : natural_transformation_scope. +End NaturalTransformationCompositionCoreNotations. +End Core. + +End Composition. + +End NaturalTransformation. + +End categories. + +Set Universe Polymorphism. + +Section path_natural_transformation. + + Context `{Funext}. + Variable C : PreCategory. + + Variable D : PreCategory. + Variables F G : Functor C D. + + Global Instance trunc_natural_transformation + : IsHSet (NaturalTransformation F G). + +admit. +Defined. + Section path. + + Variables T U : NaturalTransformation F G. + + Lemma path'_natural_transformation + : components_of T = components_of U + -> T = U. + +admit. +Defined. + Lemma path_natural_transformation + : components_of T == components_of U + -> T = U. + + Proof. + intros. + apply path'_natural_transformation. + apply path_forall; assumption. + Qed. + End path. +End path_natural_transformation. + +Ltac path_natural_transformation := + repeat match goal with + | _ => intro + | _ => apply path_natural_transformation; simpl + end. + +Module Export Identity. +Set Universe Polymorphism. + +Set Implicit Arguments. +Local Open Scope morphism_scope. + +Local Open Scope path_scope. +Section identity. + + Variable C : PreCategory. + Variable D : PreCategory. + + Section generalized. + + Variables F G : Functor C D. + Hypothesis HO : object_of F = object_of G. + Hypothesis HM : transport (fun GO => forall s d, + morphism C s d + -> morphism D (GO s) (GO d)) + HO + (morphism_of F) + = morphism_of G. + Local Notation CO c := (transport (fun GO => morphism D (F c) (GO c)) + HO + (identity (F c))). + + Definition generalized_identity_commutes s d (m : morphism C s d) + : CO d o morphism_of F m = morphism_of G m o CO s. + + Proof. + case HM. +case HO. + exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^). + Defined. + Definition generalized_identity_commutes_sym s d (m : morphism C s d) + : morphism_of G m o CO s = CO d o morphism_of F m. + +admit. +Defined. + Definition generalized_identity + : NaturalTransformation F G + := Build_NaturalTransformation' + F G + (fun c => CO c) + generalized_identity_commutes + generalized_identity_commutes_sym. + + End generalized. + Definition identity (F : Functor C D) + : NaturalTransformation F F + := Eval simpl in @generalized_identity F F 1 1. + +End identity. +Module Export NaturalTransformationIdentityNotations. + + Notation "1" := (identity _) : natural_transformation_scope. +End NaturalTransformationIdentityNotations. +End Identity. + +Module Export Laws. +Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories. +Set Universe Polymorphism. + +Local Open Scope natural_transformation_scope. +Section natural_transformation_identity. + + Context `{fs : Funext}. + Variable C : PreCategory. + + Variable D : PreCategory. + + Lemma left_identity (F F' : Functor C D) + (T : NaturalTransformation F F') + : 1 o T = T. + + Proof. + path_natural_transformation; auto with morphism. + Qed. + + Lemma right_identity (F F' : Functor C D) + (T : NaturalTransformation F F') + : T o 1 = T. + + Proof. + path_natural_transformation; auto with morphism. + Qed. +End natural_transformation_identity. +Section associativity. + + Section nt. + + Context `{fs : Funext}. + Definition associativity + C D F G H I + (V : @NaturalTransformation C D F G) + (U : @NaturalTransformation C D G H) + (T : @NaturalTransformation C D H I) + : (T o U) o V = T o (U o V). + + Proof. + path_natural_transformation. + apply associativity. + Qed. + End nt. +End associativity. +End Laws. + +Module Export FunctorCategory. +Module Export Core. +Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories. +Set Universe Polymorphism. + +Section functor_category. + + Context `{Funext}. + Variable C : PreCategory. + + Variable D : PreCategory. + + Definition functor_category : PreCategory + := @Build_PreCategory (Functor C D) + (@NaturalTransformation C D) + (@identity C D) + (@compose C D) + (@associativity _ C D) + (@left_identity _ C D) + (@right_identity _ C D) + _. + +End functor_category. +Module Export FunctorCategoryCoreNotations. + + Notation "C -> D" := (functor_category C D) : category_scope. +End FunctorCategoryCoreNotations. +End Core. + +End FunctorCategory. + +Module Export Morphisms. +Set Universe Polymorphism. + +Set Implicit Arguments. + +Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G := + @Isomorphic (C -> D) F G. + +Module Export FunctorCategoryMorphismsNotations. + + Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope. +End FunctorCategoryMorphismsNotations. +End Morphisms. + +Module Export HSet. +Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. + +Global Existing Instance iss. +End HSet. + +Module Export Core. +Set Universe Polymorphism. + +Notation cat_of obj := + (@Build_PreCategory obj + (fun x y => x -> y) + (fun _ x => x) + (fun _ _ _ f g => f o g)%core + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ _ _ => idpath) + _). + +Definition set_cat `{Funext} : PreCategory := cat_of hSet. +Set Universe Polymorphism. + +Local Open Scope morphism_scope. + +Section hom_functor. + + Context `{Funext}. + Variable C : PreCategory. + Local Notation obj_of c'c := + (BuildhSet + (morphism + C + (fst (c'c : object (C^op * C))) + (snd (c'c : object (C^op * C)))) + _). + + Let hom_functor_morphism_of s's d'd (hf : morphism (C^op * C) s's d'd) + : morphism set_cat (obj_of s's) (obj_of d'd) + := fun g => snd hf o g o fst hf. + + Definition hom_functor : Functor (C^op * C) set_cat. + + refine (Build_Functor (C^op * C) set_cat + (fun c'c => obj_of c'c) + hom_functor_morphism_of + _ + _); + subst hom_functor_morphism_of; + simpl; admit. + Defined. +End hom_functor. +Set Universe Polymorphism. + +Import Category.Dual Functor.Dual. +Import Category.Prod Functor.Prod. +Import Functor.Composition.Core. +Import Functor.Identity. +Set Universe Polymorphism. + +Local Open Scope functor_scope. +Local Open Scope natural_transformation_scope. +Section Adjunction. + + Context `{Funext}. + Variable C : PreCategory. + Variable D : PreCategory. + Variable F : Functor C D. + Variable G : Functor D C. + + Let Adjunction_Type := + Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). + + Record AdjunctionHom := + { + mate_of : + @NaturalIsomorphism H + (Prod.prod (Category.Dual.opposite C) D) + (@set_cat H) + (@compose (Prod.prod (Category.Dual.opposite C) D) + (Prod.prod (Category.Dual.opposite D) D) + (@set_cat H) (@hom_functor H D) + (@pair (Category.Dual.opposite C) + (Category.Dual.opposite D) D D + (@opposite C D F) (identity D))) + (@compose (Prod.prod (Category.Dual.opposite C) D) + (Prod.prod (Category.Dual.opposite C) C) + (@set_cat H) (@hom_functor H C) + (@pair (Category.Dual.opposite C) + (Category.Dual.opposite C) D C + (identity (Category.Dual.opposite C)) G)) + }. +End Adjunction. +(* Error: Illegal application: +The term "NaturalIsomorphism" of type + "forall (H : Funext) (C D : PreCategory), + (C -> D)%category -> (C -> D)%category -> Type" +cannot be applied to the terms + "H" : "Funext" + "(C ^op * D)%category" : "PreCategory" + "set_cat" : "PreCategory" + "hom_functor D o (F ^op, 1)" : "Functor (C ^op * D) set_cat" + "hom_functor C o (1, G)" : "Functor (C ^op * D) set_cat" +The 5th term has type "Functor (C ^op * D) set_cat" +which should be coercible to "object (C ^op * D -> set_cat)". +*) diff --git a/test-suite/bugs/closed/3331.v b/test-suite/bugs/closed/3331.v new file mode 100644 index 0000000000..9cd44bd0ca --- /dev/null +++ b/test-suite/bugs/closed/3331.v @@ -0,0 +1,31 @@ +(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *) +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (x = y :>_) : type_scope. +Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. +Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. +Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y) := H x y. +Notation Contr := (IsTrunc minus_two). +Section groupoid_category. + Variable X : Type. + Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}. + Goal X -> True. + intro d. + pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *) + clear H'. + compute in H. + change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H. + assert (H' := H). + set (foo:=_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* success *) + clear H' foo. + Set Typeclasses Debug. + pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). +Abort. \ No newline at end of file diff --git a/test-suite/bugs/opened/3330.v b/test-suite/bugs/opened/3330.v deleted file mode 100644 index face3b2d54..0000000000 --- a/test-suite/bugs/opened/3330.v +++ /dev/null @@ -1,1083 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) -Module Export HoTT_DOT_Overture. -Module Export HoTT. -Module Export Overture. - -Definition relation (A : Type) := A -> A -> Type. -Class Symmetric {A} (R : relation A) := - symmetry : forall x y, R x y -> R y x. - -Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := - fun x => g (f x). - -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. - -Open Scope function_scope. - -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. - -Delimit Scope path_scope with path. - -Local Open Scope path_scope. - -Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := - match p, q with idpath, idpath => idpath end. - -Definition inverse {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A. - -Notation "1" := idpath : path_scope. - -Notation "p @ q" := (concat p q) (at level 20) : path_scope. - -Notation "p ^" := (inverse p) (at level 3) : path_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 pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type - := forall x:A, f x = g x. - -Hint Unfold pointwise_paths : typeclass_instances. - -Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. - -Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) - : f == g - := fun x => match h with idpath => 1 end. - -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := - forall x : A, r (s x) = x. - -Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { - equiv_inv : B -> A ; - eisretr : Sect equiv_inv f; - eissect : Sect f equiv_inv; - eisadj : forall x : A, eisretr (f x) = ap f (eissect x) -}. - -Delimit Scope equiv_scope with equiv. - -Local Open Scope equiv_scope. - -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope. - -Class Contr_internal (A : Type) := BuildContr { - center : A ; - contr : (forall y : A, center = y) -}. - -Inductive trunc_index : Type := -| minus_two : trunc_index -| trunc_S : trunc_index -> trunc_index. - -Fixpoint nat_to_trunc_index (n : nat) : trunc_index - := match n with - | 0 => trunc_S (trunc_S minus_two) - | S n' => trunc_S (nat_to_trunc_index n') - end. - -Coercion nat_to_trunc_index : nat >-> trunc_index. - -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | minus_two => Contr_internal A - | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) - end. - -Class IsTrunc (n : trunc_index) (A : Type) : Type := - Trunc_is_trunc : IsTrunc_internal n A. - -Notation IsHSet := (IsTrunc 0). - -Class Funext := - { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }. - -Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : - f == g -> f = g - := - (@apD10 A P f g)^-1. - -End Overture. - -End HoTT. - -End HoTT_DOT_Overture. - -Module Export HoTT_DOT_categories_DOT_Category_DOT_Core. - -Module Export HoTT. -Module Export categories. -Module Export Category. -Module Export Core. -Set Universe Polymorphism. - -Set Implicit Arguments. -Delimit Scope morphism_scope with morphism. - -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. - -Record PreCategory := - Build_PreCategory' { - object :> Type; - morphism : object -> object -> Type; - - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - - identity_identity : forall x, identity x o identity x = identity x; - - trunc_morphism : forall s d, IsHSet (morphism s d) - }. - -Bind Scope category_scope with PreCategory. - -Arguments identity [!C%category] x%object : rename. -Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Definition Build_PreCategory - object morphism compose identity - associativity left_identity right_identity - := @Build_PreCategory' - object - morphism - compose - identity - associativity - (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _)) - left_identity - right_identity - (fun _ => left_identity _ _ _). - -Existing Instance trunc_morphism. - -Hint Resolve @left_identity @right_identity @associativity : category morphism. - -Module Export CategoryCoreNotations. - - Infix "o" := compose : morphism_scope. -End CategoryCoreNotations. -End Core. - -End Category. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Category_DOT_Core. - -Module Export HoTT_DOT_types_DOT_Forall. - -Module Export HoTT. -Module Export types. -Module Export Forall. -Generalizable Variables A B f g e n. - -Section AssumeFunext. - -Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)} - : IsTrunc n (forall a, P a) | 100. - -admit. -Defined. -End AssumeFunext. - -End Forall. - -End types. - -End HoTT. - -End HoTT_DOT_types_DOT_Forall. - -Module Export HoTT_DOT_types_DOT_Prod. - -Module Export HoTT. -Module Export types. -Module Export Prod. -Local Open Scope path_scope. - -Definition path_prod_uncurried {A B : Type} (z z' : A * B) - (pq : (fst z = fst z') * (snd z = snd z')) - : (z = z') - := match pq with (p,q) => - match z, z' return - (fst z = fst z') -> (snd z = snd z') -> (z = z') with - | (a,b), (a',b') => fun p q => - match p, q with - idpath, idpath => 1 - end - end p q - end. - -Definition path_prod {A B : Type} (z z' : A * B) : - (fst z = fst z') -> (snd z = snd z') -> (z = z') - := fun p q => path_prod_uncurried z z' (p,q). - -Definition path_prod' {A B : Type} {x x' : A} {y y' : B} - : (x = x') -> (y = y') -> ((x,y) = (x',y')) - := fun p q => path_prod (x,y) (x',y') p q. - -End Prod. - -End types. - -End HoTT. - -End HoTT_DOT_types_DOT_Prod. - -Module Export HoTT_DOT_categories_DOT_Functor_DOT_Core. - -Module Export HoTT. -Module Export categories. -Module Export Functor. -Module Export Core. -Set Universe Polymorphism. - -Set Implicit Arguments. -Delimit Scope functor_scope with functor. - -Local Open Scope morphism_scope. - -Section Functor. - - Variable C : PreCategory. - Variable D : PreCategory. - - Record Functor := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. - -End Functor. -Bind Scope functor_scope with Functor. - -Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. -Module Export FunctorCoreNotations. - - Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. -End FunctorCoreNotations. -End Core. - -End Functor. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Functor_DOT_Core. - -Module Export HoTT_DOT_categories_DOT_Category_DOT_Morphisms. - -Module Export HoTT. -Module Export categories. -Module Export Category. -Module Export Morphisms. -Set Universe Polymorphism. - -Local Open Scope morphism_scope. - -Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Class Isomorphic {C : PreCategory} s d := - { - morphism_isomorphic :> morphism C s d; - isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic - }. - -Module Export CategoryMorphismsNotations. - - Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope. - -End CategoryMorphismsNotations. -End Morphisms. - -End Category. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Category_DOT_Morphisms. - -Module Export HoTT_DOT_categories_DOT_Category_DOT_Dual. - -Module Export HoTT. -Module Export categories. -Module Export Category. -Module Export Dual. -Set Universe Polymorphism. - -Local Open Scope morphism_scope. - -Section opposite. - - Definition opposite (C : PreCategory) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _) - (fun _ _ => @left_identity _ _ _) - (@identity_identity C) - _. -End opposite. - -Module Export CategoryDualNotations. - - Notation "C ^op" := (opposite C) (at level 3) : category_scope. -End CategoryDualNotations. -End Dual. - -End Category. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Category_DOT_Dual. - -Module Export HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core. - -Module Export HoTT. -Module Export categories. -Module Export Functor. -Module Export Composition. -Module Export Core. -Set Universe Polymorphism. - -Set Implicit Arguments. -Local Open Scope morphism_scope. - -Section composition. - - Variable C : PreCategory. - Variable D : PreCategory. - Variable E : PreCategory. - Variable G : Functor D E. - Variable F : Functor C D. - - Local Notation c_object_of c := (G (F c)) (only parsing). - - Local Notation c_morphism_of m := (morphism_of G (morphism_of F m)) (only parsing). - - Let compose_composition_of' s d d' - (m1 : morphism C s d) (m2 : morphism C d d') - : c_morphism_of (m2 o m1) = c_morphism_of m2 o c_morphism_of m1. -admit. -Defined. - Definition compose_composition_of s d d' m1 m2 - := Eval cbv beta iota zeta delta - [compose_composition_of'] in - @compose_composition_of' s d d' m1 m2. - Let compose_identity_of' x - : c_morphism_of (identity x) = identity (c_object_of x). - -admit. -Defined. - Definition compose_identity_of x - := Eval cbv beta iota zeta delta - [compose_identity_of'] in - @compose_identity_of' x. - Definition compose : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - compose_composition_of - compose_identity_of. - -End composition. -Module Export FunctorCompositionCoreNotations. - - Infix "o" := compose : functor_scope. -End FunctorCompositionCoreNotations. -End Core. - -End Composition. - -End Functor. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core. - -Module Export HoTT_DOT_categories_DOT_Functor_DOT_Dual. - -Module Export HoTT. -Module Export categories. -Module Export Functor. -Module Export Dual. -Set Universe Polymorphism. - -Set Implicit Arguments. - -Section opposite. - - Variable C : PreCategory. - Variable D : PreCategory. - Definition opposite (F : Functor C D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -End opposite. -Module Export FunctorDualNotations. - - Notation "F ^op" := (opposite F) : functor_scope. -End FunctorDualNotations. -End Dual. - -End Functor. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Functor_DOT_Dual. - -Module Export HoTT_DOT_categories_DOT_Functor_DOT_Identity. - -Module Export HoTT. -Module Export categories. -Module Export Functor. -Module Export Identity. -Set Universe Polymorphism. - -Section identity. - - Definition identity C : Functor C C - := Build_Functor C C - (fun x => x) - (fun _ _ x => x) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -End identity. -Module Export FunctorIdentityNotations. - - Notation "1" := (identity _) : functor_scope. -End FunctorIdentityNotations. -End Identity. - -End Functor. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Functor_DOT_Identity. - -Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core. - -Module Export HoTT. -Module Export categories. -Module Export NaturalTransformation. -Module Export Core. -Set Universe Polymorphism. - -Set Implicit Arguments. -Local Open Scope morphism_scope. - -Section NaturalTransformation. - - Variable C : PreCategory. - Variable D : PreCategory. - Variables F G : Functor C D. - - Record NaturalTransformation := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. - -End NaturalTransformation. -End Core. - -End NaturalTransformation. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core. - -Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual. - -Module Export HoTT. -Module Export categories. -Module Export NaturalTransformation. -Module Export Dual. -Set Universe Polymorphism. - -Section opposite. - - Variable C : PreCategory. - Variable D : PreCategory. - - Definition opposite - (F G : Functor C D) - (T : NaturalTransformation F G) - : NaturalTransformation G^op F^op - := Build_NaturalTransformation' (G^op) (F^op) - (components_of T) - (fun s d => commutes_sym T d s) - (fun s d => commutes T d s). - -End opposite. - -End Dual. - -End NaturalTransformation. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual. - -Module Export HoTT_DOT_categories_DOT_Category_DOT_Strict. - -Module Export HoTT. -Module Export categories. -Module Export Category. -Module Export Strict. - -Export Category.Core. -Set Universe Polymorphism. - -End Strict. - -End Category. - -End categories. - -End HoTT. - -End HoTT_DOT_categories_DOT_Category_DOT_Strict. - -Module Export HoTT. -Module Export categories. -Module Export Category. -Module Export Prod. -Set Universe Polymorphism. - -Local Open Scope morphism_scope. - -Section prod. - - Variable C : PreCategory. - Variable D : PreCategory. - Definition prod : PreCategory. - - refine (@Build_PreCategory - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _); admit. - Defined. -End prod. -Module Export CategoryProdNotations. - - Infix "*" := prod : category_scope. -End CategoryProdNotations. -End Prod. - -End Category. - -End categories. - -End HoTT. - -Module Functor. -Module Export Prod. -Set Universe Polymorphism. - -Set Implicit Arguments. -Local Open Scope morphism_scope. - -Section proj. - - Context {C : PreCategory}. - Context {D : PreCategory}. - Definition fst : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - - Definition snd : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -End proj. - -Section prod. - - Variable C : PreCategory. - Variable D : PreCategory. - Variable D' : PreCategory. - Definition prod (F : Functor C D) (F' : Functor C D') - : Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m)) - (fun _ _ _ _ _ => path_prod' (composition_of F _ _ _ _ _) - (composition_of F' _ _ _ _ _)) - (fun _ => path_prod' (identity_of F _) (identity_of F' _)). - -End prod. -Local Infix "*" := prod : functor_scope. - -Section pair. - - Variable C : PreCategory. - Variable D : PreCategory. - Variable C' : PreCategory. - Variable D' : PreCategory. - Variable F : Functor C D. - Variable F' : Functor C' D'. - Definition pair : Functor (C * C') (D * D') - := (F o fst) * (F' o snd). - -End pair. - -Module Export FunctorProdNotations. - - Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : functor_scope. -End FunctorProdNotations. -End Prod. - -End Functor. - -Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core. - -Module Export HoTT. -Module categories. -Module Export NaturalTransformation. -Module Export Composition. -Module Export Core. -Set Universe Polymorphism. - -Set Implicit Arguments. -Local Open Scope path_scope. - -Local Open Scope morphism_scope. - -Section composition. - - Section compose. - Variable C : PreCategory. - Variable D : PreCategory. - Variables F F' F'' : Functor C D. - Variable T' : NaturalTransformation F' F''. - - Variable T : NaturalTransformation F F'. - Local Notation CO c := (T' c o T c). - - Definition compose_commutes s d (m : morphism C s d) - : CO d o morphism_of F m = morphism_of F'' m o CO s - := (associativity _ _ _ _ _ _ _ _) - @ ap (fun x => _ o x) (commutes T _ _ m) - @ (associativity_sym _ _ _ _ _ _ _ _) - @ ap (fun x => x o _) (commutes T' _ _ m) - @ (associativity _ _ _ _ _ _ _ _). - - Definition compose_commutes_sym s d (m : morphism C s d) - : morphism_of F'' m o CO s = CO d o morphism_of F m - := (associativity_sym _ _ _ _ _ _ _ _) - @ ap (fun x => x o _) (commutes_sym T' _ _ m) - @ (associativity _ _ _ _ _ _ _ _) - @ ap (fun x => _ o x) (commutes_sym T _ _ m) - @ (associativity_sym _ _ _ _ _ _ _ _). - - Definition compose - : NaturalTransformation F F'' - := Build_NaturalTransformation' F F'' - (fun c => CO c) - compose_commutes - compose_commutes_sym. - - End compose. - End composition. -Module Export NaturalTransformationCompositionCoreNotations. - - Infix "o" := compose : natural_transformation_scope. -End NaturalTransformationCompositionCoreNotations. -End Core. - -End Composition. - -End NaturalTransformation. - -End categories. - -Set Universe Polymorphism. - -Section path_natural_transformation. - - Context `{Funext}. - Variable C : PreCategory. - - Variable D : PreCategory. - Variables F G : Functor C D. - - Global Instance trunc_natural_transformation - : IsHSet (NaturalTransformation F G). - -admit. -Defined. - Section path. - - Variables T U : NaturalTransformation F G. - - Lemma path'_natural_transformation - : components_of T = components_of U - -> T = U. - -admit. -Defined. - Lemma path_natural_transformation - : components_of T == components_of U - -> T = U. - - Proof. - intros. - apply path'_natural_transformation. - apply path_forall; assumption. - Qed. - End path. -End path_natural_transformation. - -Ltac path_natural_transformation := - repeat match goal with - | _ => intro - | _ => apply path_natural_transformation; simpl - end. - -Module Export Identity. -Set Universe Polymorphism. - -Set Implicit Arguments. -Local Open Scope morphism_scope. - -Local Open Scope path_scope. -Section identity. - - Variable C : PreCategory. - Variable D : PreCategory. - - Section generalized. - - Variables F G : Functor C D. - Hypothesis HO : object_of F = object_of G. - Hypothesis HM : transport (fun GO => forall s d, - morphism C s d - -> morphism D (GO s) (GO d)) - HO - (morphism_of F) - = morphism_of G. - Local Notation CO c := (transport (fun GO => morphism D (F c) (GO c)) - HO - (identity (F c))). - - Definition generalized_identity_commutes s d (m : morphism C s d) - : CO d o morphism_of F m = morphism_of G m o CO s. - - Proof. - case HM. -case HO. - exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^). - Defined. - Definition generalized_identity_commutes_sym s d (m : morphism C s d) - : morphism_of G m o CO s = CO d o morphism_of F m. - -admit. -Defined. - Definition generalized_identity - : NaturalTransformation F G - := Build_NaturalTransformation' - F G - (fun c => CO c) - generalized_identity_commutes - generalized_identity_commutes_sym. - - End generalized. - Definition identity (F : Functor C D) - : NaturalTransformation F F - := Eval simpl in @generalized_identity F F 1 1. - -End identity. -Module Export NaturalTransformationIdentityNotations. - - Notation "1" := (identity _) : natural_transformation_scope. -End NaturalTransformationIdentityNotations. -End Identity. - -Module Export Laws. -Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories. -Set Universe Polymorphism. - -Local Open Scope natural_transformation_scope. -Section natural_transformation_identity. - - Context `{fs : Funext}. - Variable C : PreCategory. - - Variable D : PreCategory. - - Lemma left_identity (F F' : Functor C D) - (T : NaturalTransformation F F') - : 1 o T = T. - - Proof. - path_natural_transformation; auto with morphism. - Qed. - - Lemma right_identity (F F' : Functor C D) - (T : NaturalTransformation F F') - : T o 1 = T. - - Proof. - path_natural_transformation; auto with morphism. - Qed. -End natural_transformation_identity. -Section associativity. - - Section nt. - - Context `{fs : Funext}. - Definition associativity - C D F G H I - (V : @NaturalTransformation C D F G) - (U : @NaturalTransformation C D G H) - (T : @NaturalTransformation C D H I) - : (T o U) o V = T o (U o V). - - Proof. - path_natural_transformation. - apply associativity. - Qed. - End nt. -End associativity. -End Laws. - -Module Export FunctorCategory. -Module Export Core. -Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories. -Set Universe Polymorphism. - -Section functor_category. - - Context `{Funext}. - Variable C : PreCategory. - - Variable D : PreCategory. - - Definition functor_category : PreCategory - := @Build_PreCategory (Functor C D) - (@NaturalTransformation C D) - (@identity C D) - (@compose C D) - (@associativity _ C D) - (@left_identity _ C D) - (@right_identity _ C D) - _. - -End functor_category. -Module Export FunctorCategoryCoreNotations. - - Notation "C -> D" := (functor_category C D) : category_scope. -End FunctorCategoryCoreNotations. -End Core. - -End FunctorCategory. - -Module Export Morphisms. -Set Universe Polymorphism. - -Set Implicit Arguments. - -Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G := - @Isomorphic (C -> D) F G. - -Module Export FunctorCategoryMorphismsNotations. - - Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope. -End FunctorCategoryMorphismsNotations. -End Morphisms. - -Module Export HSet. -Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. - -Global Existing Instance iss. -End HSet. - -Module Export Core. -Set Universe Polymorphism. - -Notation cat_of obj := - (@Build_PreCategory obj - (fun x y => x -> y) - (fun _ x => x) - (fun _ _ _ f g => f o g)%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - _). - -Definition set_cat `{Funext} : PreCategory := cat_of hSet. -Set Universe Polymorphism. - -Local Open Scope morphism_scope. - -Section hom_functor. - - Context `{Funext}. - Variable C : PreCategory. - Local Notation obj_of c'c := - (BuildhSet - (morphism - C - (fst (c'c : object (C^op * C))) - (snd (c'c : object (C^op * C)))) - _). - - Let hom_functor_morphism_of s's d'd (hf : morphism (C^op * C) s's d'd) - : morphism set_cat (obj_of s's) (obj_of d'd) - := fun g => snd hf o g o fst hf. - - Definition hom_functor : Functor (C^op * C) set_cat. - - refine (Build_Functor (C^op * C) set_cat - (fun c'c => obj_of c'c) - hom_functor_morphism_of - _ - _); - subst hom_functor_morphism_of; - simpl; admit. - Defined. -End hom_functor. -Set Universe Polymorphism. - -Import Category.Dual Functor.Dual. -Import Category.Prod Functor.Prod. -Import Functor.Composition.Core. -Import Functor.Identity. -Set Universe Polymorphism. - -Local Open Scope functor_scope. -Local Open Scope natural_transformation_scope. -Section Adjunction. - - Context `{Funext}. - Variable C : PreCategory. - Variable D : PreCategory. - Variable F : Functor C D. - Variable G : Functor D C. - Let Adjunction_Type := Eval simpl in hom_functor D o (F^op, 1) <~=~> hom_functor C o (1, G). - -End Adjunction. -Undo. - - Record AdjunctionHom := - { - mate_of : @NaturalIsomorphism - H - (Category.Prod.prod (Category.Dual.opposite C) D) - (@Core.set_cat H) - (@compose - (Category.Prod.prod (Category.Dual.opposite C) D) - (Category.Prod.prod (Category.Dual.opposite D) D) - (@Core.set_cat H) (@hom_functor H D) - (@pair (Category.Dual.opposite C) - (Category.Dual.opposite D) D D - (@opposite C D F) (identity D))) - (@compose - (Category.Prod.prod (Category.Dual.opposite C) D) - (Category.Prod.prod (Category.Dual.opposite C) C) - (@Core.set_cat H) (@hom_functor H C) - (@pair (Category.Dual.opposite C) - (Category.Dual.opposite C) D C - (identity (Category.Dual.opposite C)) G)) - }. -Fail End Adjunction. -(* Error: Illegal application: -The term "NaturalIsomorphism" of type - "forall (H : Funext) (C D : PreCategory), - (C -> D)%category -> (C -> D)%category -> Type" -cannot be applied to the terms - "H" : "Funext" - "(C ^op * D)%category" : "PreCategory" - "set_cat" : "PreCategory" - "hom_functor D o (F ^op, 1)" : "Functor (C ^op * D) set_cat" - "hom_functor C o (1, G)" : "Functor (C ^op * D) set_cat" -The 5th term has type "Functor (C ^op * D) set_cat" -which should be coercible to "object (C ^op * D -> set_cat)". -*) diff --git a/test-suite/bugs/opened/3331.v b/test-suite/bugs/opened/3331.v deleted file mode 100644 index 07504aed7c..0000000000 --- a/test-suite/bugs/opened/3331.v +++ /dev/null @@ -1,36 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *) -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (x = y :>_) : type_scope. -Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. -Inductive trunc_index : Type := -| minus_two : trunc_index -| trunc_S : trunc_index -> trunc_index. -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | minus_two => Contr_internal A - | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) - end. -Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. -Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y) := H x y. -Notation Contr := (IsTrunc minus_two). -Section groupoid_category. - Variable X : Type. - Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}. - Goal X -> True. - intro d. - pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *) - clear H'. - compute in H. - change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H. - assert (H' := H). - pose proof (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as X0. (* success *) - clear H' X0. - Fail pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* Toplevel input, characters 21-22: -Error: -Cannot infer this placeholder. -Could not find an instance for "Contr (idpath = idpath)" in environment: - -X : Type -H : forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s) -d : X *) -- cgit v1.2.3