The connection from Coq source files to the relevant sections in the paper are as follows: Coq file Section Contents MyBasics.v all General properties on functions Names.v 3.1.4.4,3.1.4.5 and 3.1.5 An infinite, decidable set for names (and subsets of it) MathCompAddings.v all Useful lemmas for MathComp types SignatureBig.v 3.1.4.4,3.1.4.5 and 3.1.5 Definition of bigraph's signature (or controls) AbstractBigraphs.v 3.1.3,4.2.3.3,4.5.1and 4.6.3 Main bigraph type, and some elementary bigraphs Bijections.v 3.2.2 Properties and definitions of bijective functions SupportEquivalence.v 3.2.4 Definition of the support-equivalence relation between bigraphs LeanSupportEquivalence.v 3.2.5 Definition of the lean-support-equivalence relation between bigraphs eqnatc.v 4.2.2 A class for equality on natural numbers Composition.v 4.2.2 Definition of the composition and its properties TensorProduct.v 4.3.2 Definition of the tensor product and its properties Symmetries.v 4.5 and 4.6.4 Verification of properties of symmetries as bigraphs LinkAxioms.v 4.6.1 Verification of the link axioms PlaceAxioms.v 4.6.2 Verification of the place axioms NodeAxioms.v 4.6.3 Verification of the place axioms UnionPossible.v 5.2.2 Definition and lemmas of the iToO requirement ParallelProduct.v 5.2.2 Definition of the parallel product operator and its properties MergeProduct.v 5.3.2 Definition of the merge product operator and its properties Nesting.v 5.4.2 Definition of the nesting operator and its properties

An implementation of Robin Milner's bigraphs using the Rocq Prover.