added also the example of group action structure and its specialization to torsors (here)

]]>I am wondering which authors would admit that, thereby, “mathematical structure” and “data structure” becomes essentially synonymous (at least trilogous), along the same line by which “type” is ultimately nothing but a shorthand for “data type”. Evident as this may/should be, Google doesn’t known many such authors (do you?). So far it found a single one for me, just recently:

- Thomas Kehrenberg,
*Basic building blocks of dependent type theory*(Dec. 2022) [post on LessWrong]

who writes in passing:

An example of a use case for non-binary sum types is the definition of mathematical “data structures” like a ring or a group. These data structures are usually defined as…

In fact, I would go further and suggest that the term “carrier type” often used in type-theoretic discussions of mathematical structure should be recognized for what it is: the *base* data type of a data structure, hence the underlying “data base”. This way, everything falls into place, terminologically.

added also the example of “subgroup structure”: here

]]>Ok, let’s shift to the right thread.

]]>You are probably asking about the paragraph on the structure identity principle: here.

]]>From the perspective of HOTT where laws are definitional, e.g., identity of pairs and pairs of identities (slide 3 and 13 of Mike’s slides) and this goes for dependent pair and function too (slide 40), what does one say about the structure identity principle? Won’t definitional univalence lead to structural definitional equality?

]]>now starting a new section with examples of “higher strcutures”: here.

So far just one example (delooping of pointed types)

]]>replaced the example of vector space structure with module structure (here)

]]>added the example of ring structure (here)

]]>have added also the data telescope of vector space structure: here

]]>added pointer to:

- David McAllester,
*Dependent Type Theory as Related to the Bourbaki Notions of Structure and Isomorphism*[arXiv:2104.08958]

expanded out these references (previously only hinted at):

Charles Ehresmann,

*Gattungen in Lokalen Strukturen*, Jahresbericht der Deutschen Mathematiker-Vereinigung**60**(1958) 49-77 [dml:146434]Charles Ehresmann,

*Catégories et Structures*, Séminaire Ehresmann. Topologie et géométrie différentielle**6**(1964) 1-31 [numdam:SE_1964__6__A8_0, dml:112200]

and added comment on what they are actually about (early proposal to grasp the notion of mathematical structures via category theory – specifically via forgetful functors between groupoids)

also deleted the similarly incomplete reference to a textbook on algebraic theories and instead added a general pointer:

]]>For modern accounts on mathematical structures via categorical algebra see also at

algebraic theory,monad,sketch.

added pointer to:

Leo Corry,

*Mathematical Structures from Hilbert to Bourbaki: The Evolution of an Image of Mathematics*, in:*Changing Images of Mathematics in History. From the French Revolution to the new Millenium*Harwood Academic Publishers (2001) 167-186 [ISBN:9780415868273, pdf]Leo Corry,

*Modern Algebra and the Rise of Mathematical Structures*, Springer (2004) [doi:10.1007/978-3-0348-7917-0]

added pointer to:

Jeffery Zucker,

*Formalization of Classical Mathematics in Automath*, Colloques Internationaux du Centre National de la Recherche Scientifique**249**(1975) 135-145 [web, pdf]also in: Studies in Logic and the Foundations of Mathematics

**133**(1994) 127-139 [doi:10.1016/S0049-237X(08)70202-7]Nicolaas de Bruijn,

*Telescopic mappings in typed lambda calculus*, Information and Computation**91**2 (1991) 189-204 [doi:10.1016/0890-5401(91)90066-B]

It seems that discussion between these two authors in the early 1970s is the origin of the understanding of expressing mathematical structures via iterated dependent pair types (“telescopes”).

]]>added references discussing mathematical structures via dependent type theory:

in Coq:

Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg,

*A Constructive Algebraic Hierarchy in Coq*, Journal of Symbolic Computation**34**4 (2002) 271-286 [doi:10.1006/jsco.2002.0552, pdf]Claudio Sacerdoti Coen, Enrico Tassi,

*Working with Mathematical Structures in Type Theory*, in:*Types for Proofs and Programs. TYPES 2007*, Lecture Notes in Computer Science**4941**Springer (2008) [doi:10.1007/978-3-540-68103-8_11, pdf]François Garillot, Georges Gonthier, Assia Mahboubi & Laurence Rideau,

*Packaging Mathematical Structures*, in:*Theorem Proving in Higher Order Logics. TPHOLs 2009*, Lecture Notes in Computer Science**5674**, Springer (2009) [doi:10.1007/978-3-642-03359-9_23]Bas Spitters, Eelis van der Wegen

*Type classes for mathematics in type theory*, Mathematical Structures in Computer Science**21**4 “Interactive Theorem Proving and the Formalisation of Mathematics” (2011) 795-825 [doi:10.1017/S0960129511000119]Kazuhiko Sakaguchi,

*Validating Mathematical Structures*, in*Automated Reasoning. IJCAR 2020*, Lecture Notes in Computer Science**12167**, Springer (2020) [doi:10.1007/978-3-030-51054-1_8]

in Lean:

- The mathlib Community, §4 in:
*The Lean mathematical library*, in*CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs*(2020) 367–381 [arXiv:1910.09336, doi:10.1145/3372885.3373824]

I am starting a section “In dependent type theory” (here).

So far the section consists (only) of two examples: (1.) “lens structure” on a data base type and (2.) “group structure”.

(and a brief reference to the *structure identity principle*).

Looks good!

]]>I tried to take up the distinctions made by Mike in #14 and put them in separate remarks within a structured environment. Feel free to fiddle some more with the formulations.

]]>Right, Mike, I understand, the deductive urge is here not congruent with the terminological conventions and subtleties. Thank you for your improvements.

]]>I tried to clarify a bit further. The reason I wrote what I did was because I wanted to focus on the difference between the word “structure” in category theory referring to the abstract data (roughly, what the model theorist calls the language and theory), versus to the specific model of the theory in model theory. I feel like the current paragraph is confusing because it’s trying to draw two different distinctions at once: the one I intended, and also the one between properties being subsumed by structure but a structure not being necessarily a model. However, I don’t really know how to improve it.

]]>Thanks, I like your improvements (as usual) at structure.

]]>Thanks, Zoran. I made a few more changes, mostly some slight rearranging and fixing some minor linguistic errors.

]]>I made some changes.

]]>Yes, I definitely think it is misleading:

Thus the category theorist would refer to “the structure of a group” as consisting of a multiplication, a unit, etc., while the model theorist would say that each particular group (like ℤ) is a “structure (or model) for the language (or theory) of groups.”)

Structures for a language of groups may not be models, of course. For example, you can have a nonassociative magma with unit and two sided inverses. It is a structure for the language of groups but not a model for the theory of groups. This is just the standard terminology.

]]>