Species of Structures: Type-Theoretical Development

Abstract

  Methodology of conceptual design (S. P. Nikanorov et al) is based on the theory of species of structures by N. Bourbaki. It uses classical set theory and predicate logic. Meanwhile, various proof assistants built on intuitionistic type
theory (Coq, Agda, Lean and others) and possessing great capabilities in computation, proof checking etc. became  successful recently in the area of mathematics. Combining the approaches of species of structures and type theory may be instrumental for both. The article presents a formalization of the theory of species of structures in terms of type theory (Cubucal Agda, a variant of homotopy type theory). General notion of species of structure, steps, M-graph, as well as operations on steps terms and species of structures are examined. The formalization leads to two conclusions: 1) in spite of differences in philosophical foundations and in the utilized concepts of sets both approaches have similar formal structure and are connected through carrying and uncurrying; 2) theory of species of structures may serve as a metatheory to type theory. Both approaches can be considered complimentary. While the former describes the general architecture of theories, theirs interaction and genesis, the latter brings in computational and proof capabilities.