@article{Brown1967,
  author = {Brown, Ronald},
  title = {Groupoids and {Van Kampen}'s Theorem},
  journal = {Proceedings of the London Mathematical Society (3)},
  volume = {17},
  number = {3},
  year = {1967},
  pages = {385--401},
  doi = {10.1112/plms/s3-17.3.385},
  note = {\url{https://doi.org/10.1112/plms/s3-17.3.385}}
}
@inproceedings{BasoldBruinLawson2024,
  author = {Basold, Henning and Bruin, Peter and Lawson, Dominique},
  title = {The Directed {Van Kampen} Theorem in {Lean}},
  booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
  editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  series = {Leibniz International Proceedings in Informatics},
  volume = {309},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  year = {2024},
  pages = {8:1--8:18},
  doi = {10.4230/LIPIcs.ITP.2024.8},
  note = {\url{https://doi.org/10.4230/LIPIcs.ITP.2024.8}}
}
@misc{ClassicalArtifact,
  author = {Ramos, Arthur Freitas},
  title = {Classical {Seifert--van Kampen} theorem for the fundamental groupoid},
  year = {2026},
  howpublished = {Lean repository, registered commit
    \nolinkurl{874680e16db88b4a41daadf56eafbac79fd2f748}},
  note = {\url{https://github.com/Arthur742Ramos/classical-svk-lean/tree/874680e16db88b4a41daadf56eafbac79fd2f748}. Accessed September 30, 2026}
}
@misc{PalomarSVK,
  author = {{Palomar Registry}},
  title = {Classical {Seifert--van Kampen} theorem for the fundamental groupoid},
  year = {2026},
  howpublished = {Immutable registry record PALOMAR-2026-09-25-000004, version 1},
  note = {Registered September 25, 2026.
    \url{https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000004-v1.json}. Accessed September 30, 2026}
}
@misc{MathlibPinned,
  author = {{Mathlib Contributors}},
  title = {{Mathlib} fundamental groupoid and categorical infrastructure},
  year = {2026},
  howpublished = {Source repository, commit
    \nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55}},
  note = {\url{https://github.com/leanprover-community/mathlib4/tree/065356127b1dc0016f66b7283ce0ce2c4055aa55}. In particular, \nolinkurl{Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean}. Accessed September 30, 2026}
}
@misc{DirectedArtifact,
  author = {Lawson, Dominique},
  title = {Directed-Topology-{Lean}-4},
  year = {2024},
  howpublished = {Source repository, pinned commit
    \nolinkurl{009529606c66d37ef93b4b81b8587f71ce4d2c56}},
  note = {Attribution and baseline specified by the registered artifact's vendor manifest.
    \url{https://github.com/Dominique-Lawson/Directed-Topology-Lean-4/tree/009529606c66d37ef93b4b81b8587f71ce4d2c56}. Accessed September 30, 2026}
}
@misc{ComputationalPathsArtifact,
  author = {Ramos, Arthur Freitas},
  title = {{ComputationalPathsLean}},
  year = {2026},
  howpublished = {Related source repository, snapshot
    \nolinkurl{257c659b7973aeda900d86a5da73b208712c7523}},
  note = {\url{https://github.com/Arthur742Ramos/ComputationalPathsLean/tree/257c659b7973aeda900d86a5da73b208712c7523}. Relationship described in the registered artifact's provenance record. Accessed September 30, 2026}
}
@misc{IsabelleSVK,
  author = {Ramos, Arthur Freitas and Hulak, David Barros and de Queiroz, Ruy Jose Guerra Barretto},
  title = {The Classical {Seifert--van Kampen} Theorem},
  howpublished = {Archive of Formal Proofs},
  year = {2026},
  month = may,
  note = {Entry dated May 9, 2026.
    \url{https://isa-afp.org/entries/Seifert-Van-Kampen.html}. Accessed September 30, 2026}
}