Artifact

PHart3/colimits-agda Software

Author Perry Hart

Part of: Collection: Supplementary Materials
License: Mozilla Public License 2.0
Publication Date: 2026-02-18

Document Identifiers

DOI: 10.4230/artifacts.25210
URN: urn:nbn:de:0030-drops-252104

Author Details

Perry Hart

Department of Computer Science and Engineering, University of Minnesota, Minneapolis, MN, USA

Content

Software (Agda): https://github.com/PHart3/colimits-agda/tree/lapc

Version/Status

Content created at: 2025-11-06

Cite As Get BibTex

Perry Hart. PHart3/colimits-agda (Software, Agda). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/artifacts.25210

Description

Formal proofs related to coslice colimits and 2-coherent left adjoints

Subject Classification

Keywords

agda
category-theory
homotopy-type-theory
synthetic-homotopy-theory

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata

0

Downloads

Any Issues?

X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail

© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact