The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have a goal for which [admit] succeeds, but [simpl in *; admit] fails with a type error, but [simpl in *; hnf in *; admit] succeeds.

All three used to work fine, but then I changed 

Arguments Object {obj%type} !C%category / : rename.

to

Arguments Object {obj%type} C%category / : rename.

so the problem must be with Coq unfolding an [Object] where it shouldn't.  The definition of [Object] is [Object obj _ := obj].

Does anyone have any idea what's going on?

The code can be found at commit e117135 of https://bitbucket.org/JasonGross/catdb, the one-line change that I mentioned is in SpecializedCategory.v, and the failing file is UniversalProperties.v

The error is:

Toplevel input, characters 20-25:

Error: Illegal application (Type Error): 

The term "InitialObject_Object" of type

 "forall (obj : Type) (C : SpecializedCategory obj), InitialObject C -> C"

cannot be applied to the terms

 "CommaCategory_Object (SliceCategory_Functor C X0) U" : "Type"

 "Build_SpecializedCategory (CommaCategory_Morphism (T:=U))

    (CommaCategory_Identity (T:=U)) (CommaCategory_Compose (T:=U))

    (CommaCategory_subproof (T:=U)) (CommaCategory_subproof0 (T:=U))

    (CommaCategory_subproof1 (T:=U))"

   : "SpecializedCategory

        (CommaCategory_Object (SliceCategory_Functor C X0) U)"

 "M" : "InitialMorphism"

The 3rd term has type "InitialMorphism" which should be coercible to

 "InitialObject

    (Build_SpecializedCategory (CommaCategory_Morphism (T:=U))

       (CommaCategory_Identity (T:=U)) (CommaCategory_Compose (T:=U))

       (CommaCategory_subproof (T:=U)) (CommaCategory_subproof0 (T:=U))

       (CommaCategory_subproof1 (T:=U)))".

Thanks,

Jason