I am a relatively new user to Coq with a decent understanding of the basics of dependent type theory and am midway through chapter 2 of the Software Foundations Series of books. I want to start writing projects at a larger scale, and as such have stumbled upon the problem of how to properly package the mathematical theories and structures at scale.

In part of my research into this problem I found this promising paper Packaging Mathematical Structures that claims to give methodology for doing just that. The methodology it uses defines structures in three Layers:

  1. First is to define a bunch of mixins of type (M:Type -> Type) that implement certain substructures M s of a mathematical structure for a given sort/carrier type s :Type. (for example in the text one examines mix-ins for a equality structure and that of a Z-module).

2.These are then bundled together to form "classes" which are (C:Type -> Type) which packages together for any sort s:Type a structure type/record of the form {M1 s; M2 s;....} for Mi mix-ins that encodes all the extra structure over s.

  1. Finaly there are "types" which represent the complete packaged mathematical structure in question which consists of a record type of the form {sort :> Type; class :> C sort; _:Type} that gives the underlying sort plus the "class" structure adorned atop it as the first two projections. Together these two projections can define the formalization of an algebraic structure (or perhaps more generally some kind of analogue to an object of concrete category), which is what we wanted. The third anonymous projection is what my question is about. It is not well explained in the text, at least from my point of view.

For context heree is the main example structure layed out as per the text which defines a Z-module structure based on that of a class that defines an equality structure by reflection:

Record mixin_of (T : Type) : Type := ...
Record class_of (T : Type) : Type :=
Class {base :> Equality.class_of T; ext :> mixin_of T}.
Structure type : Type :=
Pack {sort :> Type; class : class_of sort; _ : Type}.

Definition unpack K (k : forall T (c : class_of T), K T c) cT :=
let: Pack T c _ := cT return K _ (class cT) in k _ c.
Definition pack :=
let k T c m := Pack (Class c m) T in Equality.unpack k.
Coercion eqType cT := Equality.Pack (class cT) cT.
End Zmodule.
Notation zmodType := Zmodule.type.
Notation ZmodType := Zmodule.pack.
Canonical Structure Zmodule.eqType.


What is the purpose of this third projection? Reading through the text I see that is maybe meant to represent something refereed to by or linked with the text as a a "head" constant - or at least related to the problem of type coercion. The text introduces the notion of head constant when taking about packaging structures by "telescoping" (of which the packaging structure laid out above is seen as a refinement / generalization of) where it discusses such a notion. Before looking into this packaging problem I had not come upon the concept of a "head constant" in the vernacular surrounding algebraic-structures / universal algebra so I assume that the notion of a "head constant" is something that is domain specific to formalizing mathematics electronically. Alternatively it could be used for something completely different and I have gotten the wrong end of the stick. The text makes no explicit inference to the nature of this projection and I am left to try and figure out from inferring from the surrounding context.

To try to figure out what is going on I dove into one of the referenced texts on "telescoping" Telescopic Mappings in Typed Lambda Calculus, but I could not intuitively relate the formalism laid down there with the context of the original paper - and so this was no help to me. I went one step further and looked at texts referenced in that paper, also to no avail.

Currently, from my (admittedly extremely ignorant) point of view this third projection seems like a useless spandrel that serves no purpose and just adds an arbitrary type into the mix of ones considerations. This is further evidenced by the fact that unpack, which is meant to be used as a dependent destructor for type essentially works by simply throwing away this hidden third argument! Also in all the examples given this third type is always given to that of the same type of the sort - so I see no generalizing benefit either. Being that taxonomising structures is an important design decision in any large scale formalization project I assume that some of the members here may have insight into why this design decision was made?

P.S. I realize the problem that I am trying to solve / methodology I am trying to understand is to do with the specific problem of doing "the plumbing" of concepts in a proof assistant, but trying to find the answer to my question has lead me to look over some nontrivial mathematics. I'm posting here and not, say, maths-stackexchange because I'm coming at it from a proof assistant usage point-of-view and not a mathematical theory point-of-view. the What topics can I ask about here? section of the wiki is currently a stub and it seems according to the Meta that the exact boundires of what questions can be asked here are still being felt out. I understand if this needs to get moved elsewhere.

  • 1
    $\begingroup$ I'm new here, but this looks relevant to this site. Also, the hierarchy-builder project may be of interest. github.com/math-comp/hierarchy-builder $\endgroup$
    – J...S
    Commented Apr 6 at 6:47
  • 1
    $\begingroup$ The answer may depend on what "large scale" means for you, and what sort of structures are you defining? IPv4 stack, modules over a ring? $\endgroup$ Commented Apr 6 at 8:07
  • $\begingroup$ J .. S i stumbled across that but have no experience in elpi / prolog so am not sure if it is worth my time to learn those things before being able to learn from that resource Bauer - the short / medium term is just to get "the usual" algebraic structures of mathematics codified - but I eventually in the longer term want to model structures in the WASM spec (which I've yet to dive into) and potentially explore writing formalisms for the constructs in the WEBGPU spec $\endgroup$ Commented Apr 6 at 13:35
  • 1
    $\begingroup$ Are you familiar with arxiv.org/abs/2311.07223? $\endgroup$ Commented Apr 6 at 15:19
  • 1
    $\begingroup$ The whole point of Hierarchy Builder is that it should help you by automating the complex boilerplate used in MathComp-style libraries. Elpi/Prolog are used under the hood to implement it, but as a user you should not have to understand that, instead you should just use the various new commands HB.xxx defined by the tool. $\endgroup$ Commented Apr 8 at 8:22

1 Answer 1


It seems like this projection is not an intrinsic part of the paradigm of packed classes

Looking at two further developments using packed classes (all of which cite the original paper as their ur-reference), one sees that their third "type" layer does not include this mystery projection.

  1. Validating Mathematical Structures by Kazuhiko Sakaguchi
  2. A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning

This leads me to believe that adding such a projection is unnecessary for this paradigm or domain specific to the original authors needs. This however does not answer the question of the original papers intent but satisfies me enough for me to be able to continue work / research in this area.

I'm making this answer community wiki so if anyone has any more insights to add and does not want to make a standalone answer they are welcome and encouraged to add it here.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.