coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Declare a morphism in a module type

From: Jean-Christophe Léchenet <jean-christophe.lechenet AT cea.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Declare a morphism in a module type
Date: Thu, 12 May 2016 18:01:16 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jean-christophe.lechenet AT cea.fr; spf=None smtp.mailfrom=jean-christophe.lechenet AT cea.fr; spf=None smtp.helo=postmaster AT oxalide-out.extra.cea.fr
Ironport-phdr: 9a23:t5PJCRb1aymjFDaTHZ58+K7/LSx+4OfEezUN459isYplN5qZpcmzbnLW6fgltlLVR4KTs6sC0LqH9fmxEj1aqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7H0osyYMl8ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JcGgflF9jAxLE9w39Rpf8hQ97vepw3iSGdZn0QLkyHD+i9aZwVBjwiCpBMzMy8GzRh9BYh69S5hy78U8si7XIaZ2YYaItNpjWeskXEDJM

Hi coq-club,

I would like to insert a morphism in a module type, but in the same way "Declare Instance" does it for typeclasses, i.e. as a field to be instantiated by the modules of that signature.
Thus, I am looking for something like "Declare Parametric Morphism ...".

The former syntax "Add Morphism R : R_m" happens to work, but I would like to avoid the old syntax and do not know how to specify the signature of the morphism with that syntax.
Moreover, in the particular case I am studying, the command fails with something looking like a universe constraint problem ('This term has type "Type@{Top.1}" which should be coercible to "Type@{Coq.Init.Logic.8}" '), but since I did not specify the signature, I cannot figure what Coq is really trying to do.

Is it possible to do what I want without manipulating the typeclasses under the morphism system ?

Best regards,

Jean-Christophe Léchenet

[Coq-Club] Declare a morphism in a module type, Jean-Christophe Léchenet, 05/12/2016