Constructive Notions of Ordinals in Homotopy Type Theory

de Jong, Tom; Kraus, Nicolai; Mohammadzadeh, Aref; Nordvall Forsberg, Fredrik; Xu, Chuangjie

doi:10.4230/artifacts.26786

Artifact

Constructive Notions of Ordinals in Homotopy Type Theory Software

Authors Tom de Jong , Nicolai Kraus , Aref Mohammadzadeh , Fredrik Nordvall Forsberg , Chuangjie Xu

Part of: Collection: Supplementary Materials
License: Creative Commons Attribution 4.0 International
Publication Date: 2026-07-09

Document Identifiers

DOI: 10.4230/artifacts.26786
URN: urn:nbn:de:0030-drops-267865

Author Details

Tom de Jong

University of Nottingham

Nicolai Kraus

University of Nottingham

Aref Mohammadzadeh

University of Nottingham

Fredrik Nordvall Forsberg

University of Strathclyde

Chuangjie Xu

Content

Software (Repository): https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott.git
archived version

Version/Status

Content created at: 2019-05-31
Status: Active (at the time of publication 2026-07-09)

Cite As Get BibTex

Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg, Chuangjie Xu. Constructive Notions of Ordinals in Homotopy Type Theory (Software, Repository). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/artifacts.26786

Description

Git repository with cubical Agda formalizations, available at https://bitbucket.org/nicolaikraus/constructive-ordinals-in-hott/

Subject Classification

Keywords

cubical Agda

Programming Languages

Agda

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata

0

Downloads

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail