Set-theoretic and type-theoretic ordinals coincide

Tom de Jong; Nicolai Kraus; Fredrik Nordvall Forsberg; Chuangjie Xu

Set-theoretic and type-theoretic ordinals coincide

Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

Research output: Contribution to conference › Paper › peer-review

44 Downloads (Pure)

Abstract

In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel’s interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel’s interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the typetheoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.

Original language	English
Number of pages	13
Publication status	E-pub ahead of print - 29 Jun 2023
Event	Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science - Boston, United States Duration: 26 Jun 2023 → 29 Jun 2023 Conference number: 38 https://lics.siglog.org/lics23/

Conference

Conference	Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS
Country/Territory	United States
City	Boston
Period	26/06/23 → 29/06/23
Internet address	https://lics.siglog.org/lics23/

Keywords

set-theoretic
type-theoretic
ordinals
homotopy type theory (HoTT)
Aczel's interpretation

Access to Document

de-Jong-etal-LICS-2023-Set-theoretic-and-type-theoretic-ordinals-coincideAccepted author manuscript, 786 KBLicence: Strath_1

Cite this

@conference{e44fb9bbd4d44ca2ba9e782cb9e77a1d,

title = "Set-theoretic and type-theoretic ordinals coincide",

abstract = "In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel{\textquoteright}s interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel{\textquoteright}s interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the typetheoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.",

keywords = "set-theoretic, type-theoretic, ordinals, homotopy type theory (HoTT), Aczel's interpretation",

author = "{de Jong}, Tom and Nicolai Kraus and {Nordvall Forsberg}, Fredrik and Chuangjie Xu",

year = "2023",

month = jun,

day = "29",

language = "English",

note = "Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ; Conference date: 26-06-2023 Through 29-06-2023",

url = "https://lics.siglog.org/lics23/",

}

TY - CONF

T1 - Set-theoretic and type-theoretic ordinals coincide

AU - de Jong, Tom

AU - Kraus, Nicolai

AU - Nordvall Forsberg, Fredrik

AU - Xu, Chuangjie

N1 - Conference code: 38

PY - 2023/6/29

Y1 - 2023/6/29

N2 - In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel’s interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel’s interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the typetheoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.

AB - In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel’s interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel’s interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the typetheoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.

KW - set-theoretic

KW - type-theoretic

KW - ordinals

KW - homotopy type theory (HoTT)

KW - Aczel's interpretation

UR - https://doi.org/10.48550/arXiv.2301.10696

M3 - Paper

T2 - Thirty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 26 June 2023 through 29 June 2023

ER -

Set-theoretic and type-theoretic ordinals coincide

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this