Three equivalent ordinal notation systems in cubical Agda

Fredrik Nordvall Forsberg; Chuangjie Xu; Neil Ghani

doi:10.1145/3372885.3373835

Three equivalent ordinal notation systems in cubical Agda

Fredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

2 Citations (Scopus)

22 Downloads (Pure)

Abstract

We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

Original language	English
Title of host publication	CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors	Jasmin Blanchette, Catalin Hritcu
Place of Publication	New York
Pages	172–185
Number of pages	14
DOIs	https://doi.org/10.1145/3372885.3373835
Publication status	Published - 24 Jan 2020

Keywords

theory of computation
proof theory
type theory
ordinal notation
cantor normal form
inductive-inductive definitions
higher inductive types
cubical Agda
programming

Access to Document

10.1145/3372885.3373835

Forsberg-etal-SIGPLAN-2020-Three-equivalent-ordinal-notation-systems-in-cubical-agdaAccepted author manuscript, 840 KB

Fredrik Nordvall Forsberg
- fredrik.nordvall-forsberg@strath.ac.uk
- Computer And Information Sciences - Lecturer B
- SICSA
Person: Academic, Research Only

1 Finished

Homotopy Type Theory: Programming and Verification
Ghani, N. & McBride, C.
EPSRC (Engineering and Physical Sciences Research Council)
1/04/15 → 30/09/19
Project: Research

Cite this

@inproceedings{36ebef40e5b1492184cce76e81981dd8,

title = "Three equivalent ordinal notation systems in cubical Agda",

abstract = "We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.",

keywords = "theory of computation, proof theory, type theory, ordinal notation, cantor normal form, inductive-inductive definitions, higher inductive types, cubical Agda, programming",

author = "{Nordvall Forsberg}, Fredrik and Chuangjie Xu and Neil Ghani",

year = "2020",

month = jan,

day = "24",

doi = "10.1145/3372885.3373835",

language = "English",

isbn = "9781450370974",

pages = "172–185",

editor = "Jasmin Blanchette and Catalin Hritcu",

booktitle = "CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs",

}

Three equivalent ordinal notation systems in cubical Agda. / Nordvall Forsberg, Fredrik; Xu, Chuangjie; Ghani, Neil.

CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ed. / Jasmin Blanchette; Catalin Hritcu. New York, 2020. p. 172–185.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Three equivalent ordinal notation systems in cubical Agda

AU - Nordvall Forsberg, Fredrik

AU - Xu, Chuangjie

AU - Ghani, Neil

PY - 2020/1/24

Y1 - 2020/1/24

N2 - We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

AB - We present three ordinal notation systems representing ordinals below epsilon zero in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

KW - theory of computation

KW - proof theory

KW - type theory

KW - ordinal notation

KW - cantor normal form

KW - inductive-inductive definitions

KW - higher inductive types

KW - cubical Agda

KW - programming

U2 - 10.1145/3372885.3373835

DO - 10.1145/3372885.3373835

M3 - Conference contribution book

SN - 9781450370974

SP - 172

EP - 185

BT - CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

A2 - Blanchette, Jasmin

A2 - Hritcu, Catalin

CY - New York

ER -

Three equivalent ordinal notation systems in cubical Agda

Abstract

Keywords

Access to Document

Fredrik Nordvall Forsberg

Homotopy Type Theory: Programming and Verification

Cite this