Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA class of higher inductive types in Zermelo-Fraenkel set theory
110
0
0.0
(
0
)
Authors
Andrew Swan
Ask ChatGPT about the research
No Arabic abstract
We define a class of higher inductive types that can be constructed in the category of sets under the assumptions of Zermelo-Fraenkel set theory without the axiom of choice or the existence of uncountable regular cardinals. This class includes the example of unordered trees of any arity.
rate research
Read More
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the synthetic development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(infty,1)$-category is presented by some model category to which our results apply.
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.
We investigate the mathematics of a model of the human mind which has been proposed by the psychologist Jens Mammen. Mathematical realizations of this model consist of so-called emph{Mammen spaces}, where a Mammen space is a triple $(U,mathcal S,mathcal C)$, where $U$ is a non-empty set (the universe), $mathcal S$ is a perfect Hausdorff topology on $U$, and $mathcal Csubseteqmathcal P(U)$ together with $mathcal S$ satisfy certain axioms. We refute a conjecture put forward by J. Hoffmann-J{o}rgensen, who conjectured that the existence of a complete Mammen space implies the Axiom of Choice, by showing that in the first Cohen model, in which ZF holds but AC fails, there is a complete Mammen space. We obtain this by proving that in the first Cohen model, every perfect topology can be extended to a maximal perfect topology. On the other hand, we also show that if all sets are Lebesgue measurable, or all sets are Baire measurable, then there are no complete Mammen spaces with a countable universe. Finally, we investigate two new cardinal invariants $mathfrak u_M$ and $mathfrak u_T$ associated with complete Mammen spaces and maximal perfect topologies, and establish some basic inequalities that are provable in ZFC. We show $mathfrak u_M=mathfrak u_T=2^{aleph_0}$ follows from Martins Axiom, and, contrastingly, we show that $aleph_1=mathfrak u_M=mathfrak u_T<2^{aleph_0}=aleph_2$ in the Baumgartner-Laver model.
This is a short introductory course to Set Theory, based on axioms of von Neumann--Bernays--Godel (briefly NBG). The text can be used as a base for a lecture course in Foundations of Mathematics, and contains a reasonable minimum which a good (post-graduate) student in Mathematics should know about foundations of this science.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
