From 0a51137f7ff80afdcf216d85cd8be25a531bc39b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 15 Jun 2014 13:24:41 +0200 Subject: - Fix xml plugin treatment of inductives. - Move HoTT bug #30 to closed --- plugins/xml/xmlcommand.ml | 15 ++- test-suite/bugs/closed/HoTT_coq_030.v | 241 ++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/HoTT_coq_032.v | 22 ++++ test-suite/bugs/opened/HoTT_coq_027.v | 5 +- test-suite/bugs/opened/HoTT_coq_030.v | 241 ---------------------------------- test-suite/bugs/opened/HoTT_coq_032.v | 22 ---- 6 files changed, 273 insertions(+), 273 deletions(-) create mode 100644 test-suite/bugs/closed/HoTT_coq_030.v create mode 100644 test-suite/bugs/closed/HoTT_coq_032.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_030.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_032.v diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 8f47859da..ef5e18201 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -244,15 +244,16 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let {Declarations.mind_consnames=consnames ; Declarations.mind_typename=typename } = p in - let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in - let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in - let cons = + let inst = Univ.UContext.instance mib.Declarations.mind_universes in + let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),inst) in + let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),inst) in + let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) - (Array.mapi - (fun j x ->(x,Unshare.unshare lc.(j))) consnames) - [] + (Array.mapi + (fun j x ->(x,Unshare.unshare lc.(j))) consnames) + [] ) - in + in (typename,finite,Unshare.unshare arity,cons)::i ) packs [] in diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v new file mode 100644 index 000000000..fa5ee25ca --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_030.v @@ -0,0 +1,241 @@ +Set Implicit Arguments. +Generalizable All Variables. +Set Asymmetric Patterns. +Set Universe Polymorphism. + +Delimit Scope object_scope with object. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope functor_scope with functor. + +Local Open Scope category_scope. + +Record SpecializedCategory (obj : Type) := + { + Object :> _ := obj; + Morphism : obj -> obj -> Type; + + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' + }. + +Bind Scope category_scope with SpecializedCategory. +Bind Scope object_scope with Object. +Bind Scope morphism_scope with Morphism. + +Arguments Object {obj%type} C%category / : rename. +Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *) +Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Record Category := { + CObject : Type; + + UnderlyingCategory :> @SpecializedCategory CObject +}. + +Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category. + refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *) +Defined. + +Coercion GeneralizeCategory : SpecializedCategory >-> Category. + +Record SpecializedFunctor + `(C : @SpecializedCategory objC) + `(D : @SpecializedCategory objD) + := { + ObjectOf :> objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) + }. + +Section Functor. + Context (C D : Category). + + Definition Functor := SpecializedFunctor C D. +End Functor. + +Bind Scope functor_scope with SpecializedFunctor. +Bind Scope functor_scope with Functor. + +Arguments SpecializedFunctor {objC} C {objD} D. +Arguments Functor C D. +Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch. +Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +Section FunctorComposition. + Context `(B : @SpecializedCategory objB). + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(E : @SpecializedCategory objE). + + Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E + := Build_SpecializedFunctor C E + (fun c => G (F c)) + (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)). +End FunctorComposition. + +Record SpecializedNaturalTransformation + `{C : @SpecializedCategory objC} + `{D : @SpecializedCategory objD} + (F G : SpecializedFunctor C D) + := { + ComponentsOf :> forall c, D.(Morphism) (F c) (G c) + }. + +Definition ProductCategory + `(C : @SpecializedCategory objC) + `(D : @SpecializedCategory objD) +: @SpecializedCategory (objC * objD)%type + := @Build_SpecializedCategory _ + (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type) + (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))). + +Infix "*" := ProductCategory : category_scope. + +Section ProductCategoryFunctors. + Context `{C : @SpecializedCategory objC}. + Context `{D : @SpecializedCategory objD}. + + Definition fst_Functor : SpecializedFunctor (C * D) C + := Build_SpecializedFunctor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _). + + Definition snd_Functor : SpecializedFunctor (C * D) D + := Build_SpecializedFunctor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _). +End ProductCategoryFunctors. + + +Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC := + @Build_SpecializedCategory objC + (fun s d => Morphism C d s) + (fun _ _ _ m1 m2 => Compose m2 m1). + +Section OppositeFunctor. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Variable F : SpecializedFunctor C D. + Let COp := OppositeCategory C. + Let DOp := OppositeCategory D. + + Definition OppositeFunctor : SpecializedFunctor COp DOp + := Build_SpecializedFunctor COp DOp + (fun c : COp => F c : DOp) + (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m). +End OppositeFunctor. + +Section FunctorProduct. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(D' : @SpecializedCategory objD'). + + Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D'). + match goal with + | [ |- SpecializedFunctor ?C0 ?D0 ] => + refine (Build_SpecializedFunctor + C0 D0 + (fun c => (F c, F' c)) + (fun s d m => (MorphismOf F m, MorphismOf F' m))) + end. + Defined. +End FunctorProduct. + +Section FunctorProduct'. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(C' : @SpecializedCategory objC'). + Context `(D' : @SpecializedCategory objD'). + Variable F : Functor C D. + Variable F' : Functor C' D'. + + Definition FunctorProduct' : SpecializedFunctor (C * C') (D * D') + := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor). +End FunctorProduct'. + +(** XXX TODO(jgross): Change this to [FunctorProduct]. *) +Infix "*" := FunctorProduct' : functor_scope. + +Definition TypeCat : @SpecializedCategory Type := + (@Build_SpecializedCategory Type + (fun s d => s -> d) + (fun _ _ _ f g => (fun x => f (g x)))). + +Section HomFunctor. + Context `(C : @SpecializedCategory objC). + Let COp := OppositeCategory C. + + Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat + := Build_SpecializedFunctor C TypeCat + (fun X : C => C.(Morphism) A X : TypeCat) + (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)). + + Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat. + + Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) : + TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd). + unfold hom_functor_object_of in *. + destruct s's as [ s' s ], d'd as [ d' d ]. + destruct hf as [ h f ]. + intro g. + exact (Compose f (Compose g h)). + Defined. + + Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat + := Build_SpecializedFunctor (COp * C) TypeCat + (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat) + (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf). +End HomFunctor. + +Section FullFaithful. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Variable F : SpecializedFunctor C D. + Let COp := OppositeCategory C. + Let DOp := OppositeCategory D. + Let FOp := OppositeFunctor F. + + Definition InducedHomNaturalTransformation : + SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) + := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) + (fun sd : (COp * C) => + MorphismOf F (s := _) (d := _))). +End FullFaithful. + +Definition FunctorCategory + `(C : @SpecializedCategory objC) + `(D : @SpecializedCategory objD) +: @SpecializedCategory (SpecializedFunctor C D). + refine (@Build_SpecializedCategory _ + (SpecializedNaturalTransformation (C := C) (D := D)) + _); + admit. +Defined. + +Notation "C ^ D" := (FunctorCategory D C) : category_scope. + +Section Yoneda. + Context `(C : @SpecializedCategory objC). + Let COp := OppositeCategory C. + + Section Yoneda. + Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d) + := Build_SpecializedNaturalTransformation + (CovariantHomFunctor C s) + (CovariantHomFunctor C d) + (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)). + + Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C) + := Build_SpecializedFunctor COp (TypeCat ^ C) + (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C) + (fun s d (f : Morphism COp s d) => Yoneda_NT s d f). + End Yoneda. +End Yoneda. + +Section FullyFaithful. + Context `(C : @SpecializedCategory objC). + + Set Printing Universes. + Check InducedHomNaturalTransformation (Yoneda C). + (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because +Top.851 < Top.869 <= Top.864 <= Top.865). *) +End FullyFaithful. diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v new file mode 100644 index 000000000..3f5d7b021 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_032.v @@ -0,0 +1,22 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *) +Set Implicit Arguments. +Generalizable All Variables. +Set Asymmetric Patterns. +Set Universe Polymorphism. + +Delimit Scope object_scope with object. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope functor_scope with functor. + +Local Open Scope category_scope. + +Record SpecializedCategory (obj : Type) := + { + Object :> _ := obj; + Morphism : obj -> obj -> Type; + + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' + }. +(* Anomaly: Mismatched instance and context when building universe substitution. +Please report. *) diff --git a/test-suite/bugs/opened/HoTT_coq_027.v b/test-suite/bugs/opened/HoTT_coq_027.v index e58092eb6..7f283237a 100644 --- a/test-suite/bugs/opened/HoTT_coq_027.v +++ b/test-suite/bugs/opened/HoTT_coq_027.v @@ -20,8 +20,8 @@ Identity Coercion FunctorToType_Id : FunctorToType >-> Functor. Set Printing Universes. Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C) -: FunctorToType C. - Fail refine (@Build_Functor _ C _ TypeCat +: FunctorToType@{Type Type Type Set} C. + refine (@Build_Functor _ C _ TypeCat (fun x => F.(ObjectOf) x) (fun s d m => F.(MorphismOf) _ _ m)). (* ??? Toplevel input, characters 8-148: @@ -40,7 +40,6 @@ The term "FunctorToType@{Top.100 Top.101 Top.102 Top.103} C" (Universe inconsistency: Cannot enforce Set = Top.103)). *) -admit. Defined. (* Toplevel input, characters 0-8: Error: The term diff --git a/test-suite/bugs/opened/HoTT_coq_030.v b/test-suite/bugs/opened/HoTT_coq_030.v deleted file mode 100644 index 934fcd5d8..000000000 --- a/test-suite/bugs/opened/HoTT_coq_030.v +++ /dev/null @@ -1,241 +0,0 @@ -Set Implicit Arguments. -Generalizable All Variables. -Set Asymmetric Patterns. -Set Universe Polymorphism. - -Delimit Scope object_scope with object. -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope functor_scope with functor. - -Local Open Scope category_scope. - -Record SpecializedCategory (obj : Type) := - { - Object :> _ := obj; - Morphism : obj -> obj -> Type; - - Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' - }. - -Bind Scope category_scope with SpecializedCategory. -Bind Scope object_scope with Object. -Bind Scope morphism_scope with Morphism. - -Arguments Object {obj%type} C%category / : rename. -Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *) -Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Record Category := { - CObject : Type; - - UnderlyingCategory :> @SpecializedCategory CObject -}. - -Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category. - refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *) -Defined. - -Coercion GeneralizeCategory : SpecializedCategory >-> Category. - -Record SpecializedFunctor - `(C : @SpecializedCategory objC) - `(D : @SpecializedCategory objD) - := { - ObjectOf :> objC -> objD; - MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) - }. - -Section Functor. - Variable C D : Category. - - Definition Functor := SpecializedFunctor C D. -End Functor. - -Bind Scope functor_scope with SpecializedFunctor. -Bind Scope functor_scope with Functor. - -Arguments SpecializedFunctor {objC} C {objD} D. -Arguments Functor C D. -Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch. -Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Section FunctorComposition. - Context `(B : @SpecializedCategory objB). - Context `(C : @SpecializedCategory objC). - Context `(D : @SpecializedCategory objD). - Context `(E : @SpecializedCategory objE). - - Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E - := Build_SpecializedFunctor C E - (fun c => G (F c)) - (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)). -End FunctorComposition. - -Record SpecializedNaturalTransformation - `{C : @SpecializedCategory objC} - `{D : @SpecializedCategory objD} - (F G : SpecializedFunctor C D) - := { - ComponentsOf :> forall c, D.(Morphism) (F c) (G c) - }. - -Definition ProductCategory - `(C : @SpecializedCategory objC) - `(D : @SpecializedCategory objD) -: @SpecializedCategory (objC * objD)%type - := @Build_SpecializedCategory _ - (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type) - (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))). - -Infix "*" := ProductCategory : category_scope. - -Section ProductCategoryFunctors. - Context `{C : @SpecializedCategory objC}. - Context `{D : @SpecializedCategory objD}. - - Definition fst_Functor : SpecializedFunctor (C * D) C - := Build_SpecializedFunctor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _). - - Definition snd_Functor : SpecializedFunctor (C * D) D - := Build_SpecializedFunctor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _). -End ProductCategoryFunctors. - - -Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC := - @Build_SpecializedCategory objC - (fun s d => Morphism C d s) - (fun _ _ _ m1 m2 => Compose m2 m1). - -Section OppositeFunctor. - Context `(C : @SpecializedCategory objC). - Context `(D : @SpecializedCategory objD). - Variable F : SpecializedFunctor C D. - Let COp := OppositeCategory C. - Let DOp := OppositeCategory D. - - Definition OppositeFunctor : SpecializedFunctor COp DOp - := Build_SpecializedFunctor COp DOp - (fun c : COp => F c : DOp) - (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m). -End OppositeFunctor. - -Section FunctorProduct. - Context `(C : @SpecializedCategory objC). - Context `(D : @SpecializedCategory objD). - Context `(D' : @SpecializedCategory objD'). - - Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D'). - match goal with - | [ |- SpecializedFunctor ?C0 ?D0 ] => - refine (Build_SpecializedFunctor - C0 D0 - (fun c => (F c, F' c)) - (fun s d m => (MorphismOf F m, MorphismOf F' m))) - end. - Defined. -End FunctorProduct. - -Section FunctorProduct'. - Context `(C : @SpecializedCategory objC). - Context `(D : @SpecializedCategory objD). - Context `(C' : @SpecializedCategory objC'). - Context `(D' : @SpecializedCategory objD'). - Variable F : Functor C D. - Variable F' : Functor C' D'. - - Definition FunctorProduct' : SpecializedFunctor (C * C') (D * D') - := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor). -End FunctorProduct'. - -(** XXX TODO(jgross): Change this to [FunctorProduct]. *) -Infix "*" := FunctorProduct' : functor_scope. - -Definition TypeCat : @SpecializedCategory Type := - (@Build_SpecializedCategory Type - (fun s d => s -> d) - (fun _ _ _ f g => (fun x => f (g x)))). - -Section HomFunctor. - Context `(C : @SpecializedCategory objC). - Let COp := OppositeCategory C. - - Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat - := Build_SpecializedFunctor C TypeCat - (fun X : C => C.(Morphism) A X : TypeCat) - (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)). - - Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat. - - Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) : - TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd). - unfold hom_functor_object_of in *. - destruct s's as [ s' s ], d'd as [ d' d ]. - destruct hf as [ h f ]. - intro g. - exact (Compose f (Compose g h)). - Defined. - - Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat - := Build_SpecializedFunctor (COp * C) TypeCat - (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat) - (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf). -End HomFunctor. - -Section FullFaithful. - Context `(C : @SpecializedCategory objC). - Context `(D : @SpecializedCategory objD). - Variable F : SpecializedFunctor C D. - Let COp := OppositeCategory C. - Let DOp := OppositeCategory D. - Let FOp := OppositeFunctor F. - - Definition InducedHomNaturalTransformation : - SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) - := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) - (fun sd : (COp * C) => - MorphismOf F (s := _) (d := _))). -End FullFaithful. - -Definition FunctorCategory - `(C : @SpecializedCategory objC) - `(D : @SpecializedCategory objD) -: @SpecializedCategory (SpecializedFunctor C D). - refine (@Build_SpecializedCategory _ - (SpecializedNaturalTransformation (C := C) (D := D)) - _); - admit. -Defined. - -Notation "C ^ D" := (FunctorCategory D C) : category_scope. - -Section Yoneda. - Context `(C : @SpecializedCategory objC). - Let COp := OppositeCategory C. - - Section Yoneda. - Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d) - := Build_SpecializedNaturalTransformation - (CovariantHomFunctor C s) - (CovariantHomFunctor C d) - (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)). - - Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C) - := Build_SpecializedFunctor COp (TypeCat ^ C) - (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C) - (fun s d (f : Morphism COp s d) => Yoneda_NT s d f). - End Yoneda. -End Yoneda. - -Section FullyFaithful. - Context `(C : @SpecializedCategory objC). - - Set Printing Universes. - Fail Check InducedHomNaturalTransformation (Yoneda C). - (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because -Top.851 < Top.869 <= Top.864 <= Top.865). *) -End FullyFaithful. diff --git a/test-suite/bugs/opened/HoTT_coq_032.v b/test-suite/bugs/opened/HoTT_coq_032.v deleted file mode 100644 index e6ae8a0c4..000000000 --- a/test-suite/bugs/opened/HoTT_coq_032.v +++ /dev/null @@ -1,22 +0,0 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *) -Set Implicit Arguments. -Generalizable All Variables. -Set Asymmetric Patterns. -Set Universe Polymorphism. - -Delimit Scope object_scope with object. -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope functor_scope with functor. - -Local Open Scope category_scope. - -Fail Record SpecializedCategory (obj : Type) := - { - Object :> _ := obj; - Morphism : obj -> obj -> Type; - - Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' - }. -(* Anomaly: Mismatched instance and context when building universe substitution. -Please report. *) -- cgit v1.2.3