The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Can someone explain to me why the following code generates a stack overflow, and whether or not this is a bug?

Set Implicit Arguments.

Generalizable All Variables.

Set Printing Universes.

Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {

  Object :> _ := obj;

  Morphism' : obj -> obj -> Type;

  Identity' : forall o, Morphism' o o;

  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d';

  Associativity' : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),

    Compose' (Compose' m3 m2) m1 = Compose' m3 (Compose' m2 m1);

  (* ask for [eq_sym (Associativity' ...)], so that C^{op}^{op} is convertible with C *)

  Associativity'_sym : forall o1 o2 o3 o4 (m1 : Morphism' o1 o2) (m2 : Morphism' o2 o3) (m3 : Morphism' o3 o4),

    Compose' m3 (Compose' m2 m1) = Compose' (Compose' m3 m2) m1

}.

Definition CatO : SpecializedCategory Empty_set.

  exact (@Build_SpecializedCategory' Empty_set

                                     (fun x => match x with end)

                                     (fun x => match x with end)

                                     (fun x => match x with end)

                                     (fun x => match x with end)

                                     (fun x => match x with end)).

Defined.

Thanks!

-Jason