## Connecting Constructive Notions of Ordinals in Homotopy Type Theory

by Nicolai Kraus, Fredrik Nordvall-Forsberg, and Chuangjie Xu

This repository contains an implementation of the above-named paper.
The root file is index.agda, and all files are tested with

- Agda version 2.6.2

- Cubical Agda library
     (commit: 4e9e4f7177c3c625db3fb3249e31fa81035c2d69)