nLab
higher-order set theory

Contents

Context

Foundations

2-category theory

Contents

Idea

Various concepts from logic have corresponding concepts from structural set theory: propositions and predicates correspond to sets and families, true and false correspond to singleton and empty set, conjunction and disjunction correspond to to cartesian product and disjoint union, and so on. The same should be true of higher-order predicates in higher-order logic, which should have a corresponding concept of higher-order families in some notion of higher-order set theory.

Thus, a higher-order set theory is any structural set theory which features higher-order families, which are families of families. If we think of a family of sets as a functor to Set, then a higher-order family is a functor on a functor groupoid with target Set.

Just as intuitionistic higher-order logic is the internal logic of an elementary topos, constructive higher-order set theory is the internal set theory of an elementary (2,1)-topos?.

Last revised on March 3, 2021 at 00:25:48. See the history of this page for a list of all contributions to it.