The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

Here’s an issue which I’ve run into in several different developments recently, when working with either setoids or categories, and maps/functors between them considered as a setoid/category themselves.  I’m hoping that others may have come across similar issues before, and found better workarounds than I have so far.

The short version is that I have two coercions, which *look* like they’re of the form [ c1 : A >-> B ], [ c2 : B >-> C ], so I expect to be able to use a term of type A as a term of type C.  However, the domain of the second coercion is actually not B itself but B', where B reduces to B'; and so the coercions do not quite compose.

The following MWE is closely based on a true story; names have not been changed, but in the original, all these record types of course have further fields:

---8<---

Record setoid := { setoid_base :> Type }.

Record setoidmap_internal (X Y : setoid)

  := { setoidmap_function :> X -> Y }.

(* Setoid maps themselves form a setoid: *) 

Definition setoidmap (X Y : setoid) : setoid

  := Build_setoid (setoidmap_internal X Y).

(* Only [setoidmap] is used from here on, for a long time;

  [setoidmap_internal] never appears explicitly,

  and we have the illusion of a coercion [setoidmap >-> Funclass]: *)

Definition test1 (X Y : setoid) (f : setoidmap X Y) (x : X) : Y

  := f x. 

Record monoid := { monoid_carrier :> setoid }.

Record monoidmap (X Y : monoid)

  := { monoidmap_function :> setoidmap X Y }.

(* We also appear to have a coercion [ monoidmap >-> setoidmap ].*)

(* However, we don’t get a composite coercion [ monoidmap >-> Funclass ]: *)

Definition test2 (X Y : monoid) (f : monoidmap X Y) (x : X) : Y.

Proof.

  try exact (f x). (* fails! *)

  exact ((f : setoidmap X Y) x). (* succeeds *)

Defined.

---8<----

The problem (if I’m understanding it right) is that the first coercion really goes [ setoidmap_internal >-> Funclass ], whereas the second really goes [ monoidmap >-> setoid_base ], and so they are not composable.  The illusion of composability comes from the reduction [ setoid_base (setoidmap X Y) ~~> setoidmap_internal X Y ], and is reinforced by the fact that [ setoid_base ] is itself a coercion.

The two main solutions I have found are changing the type of [ monoidmap_function ] to [ setoidmap_internal X Y ] in the definition of [ monoidmap ], or else explicitly giving the “midpoint” of the coercion composition at the point of use, as in the successful proof of [ test2 ] in the MWE.  However, both of these break the nice abstraction/illusion provided by the coercion [ setoid_base : setoid >-> Sortclass ], which otherwise allows us to never mention [ setoidmap_internal ] explicitly.

Does anyone have a way of setting the definitions up that allows this abstraction/illusion to be preserved?

Best,

–Peter.