Cover Image

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Gratzer, Daniel, Gylterud, Håkon, Mörtberg, Anders, Stenholm, Elisabeth
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Logic
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2020)

Univalent Material Set Theory
by: Gylterud, Håkon Robbestad, et al.
Published: (2023)

On Planarity of Graphs in Homotopy Type Theory
by: Prieto-Cubides, Jonathan, et al.
Published: (2021)

Computational Synthetic Cohomology Theory in Homotopy Type Theory
by: Ljungström, Axel, et al.
Published: (2024)

(Pointed) Univalence in Universe Category Models of Type Theory
by: Kapulkin, Chris, et al.
Published: (2025)

On Small Types in Univalent Foundations
by: de Jong, Tom, et al.
Published: (2021)

Internalizing Representation Independence with Univalence
by: Angiuli, Carlo, et al.
Published: (2020)

A Univalent Formalization of Constructive Affine Schemes
by: Zeuner, Max, et al.
Published: (2022)

Automating Boundary Filling in Cubical Type Theories
by: Doré, Maximilian, et al.
Published: (2024)

Formalising and Computing the Fourth Homotopy Group of the $3$-Sphere in Cubical Agda
by: Ljungström, Axel, et al.
Published: (2023)

Coslice Colimits in Homotopy Type Theory
by: Hart, Perry, et al.
Published: (2024)

Univalence without function extensionality
by: Cavallo, Evan, et al.
Published: (2026)

Univalent Double Categories
by: van der Weide, Niels, et al.
Published: (2023)

Derivatives for Containers in Univalent Foundations
by: Joram, Philipp, et al.
Published: (2025)

Normalization for multimodal type theory
by: Gratzer, Daniel
Published: (2023)

Strict universes for Grothendieck topoi
by: Gratzer, Daniel, et al.
Published: (2022)

Univalent Enriched Categories and the Enriched Rezk Completion
by: van der Weide, Niels
Published: (2024)

Epimorphisms and Acyclic Types in Univalent Foundations
by: Buchholtz, Ulrik, et al.
Published: (2024)

Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
by: Takahashi, Yuta
Published: (2024)

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
by: Brough, Jackson
Published: (2026)

The Formal Theory of Monads, Univalently
by: van der Weide, Niels
Published: (2022)

The Patch Topology in Univalent Foundations
by: Arrieta, Igor, et al.
Published: (2024)

Arboreal Categories: An Axiomatic Theory of Resources
by: Abramsky, Samson, et al.
Published: (2021)

Characterizing Sets of Theories That Can Be Disjointly Combined
by: Przybocki, Benjamin, et al.
Published: (2025)

Primitive Recursive Dependent Type Theory
by: Buchholtz, Ulrik, et al.
Published: (2024)

Constructive and Predicative Locale Theory in Univalent Foundations
by: Tosun, Ayberk
Published: (2026)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

Non-Derivability Results in Polymorphic Dependent Type Theory
by: Geuvers, Herman
Published: (2026)

A Naive Encoding of Russell's Paradox in Type Theory
by: Qu, Zhuoyuan
Published: (2025)

Are Dependent Types in Set Theory Feasible?
by: Yang, Yunsong, et al.
Published: (2026)

Symmetric Monoidal Smash Products in Homotopy Type Theory
by: Ljungström, Axel
Published: (2024)

A topological reading of inductive and coinductive definitions in Dependent Type Theory
by: Sabelli, Pietro
Published: (2024)

The Groupoid-Syntax of Type Theory is a Set
by: Altenkirch, Thorsten, et al.
Published: (2025)

Controlling unfolding in type theory
by: Gratzer, Daniel, et al.
Published: (2022)

Unifying cubical and multimodal type theory
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2022)

Exact Real Search: Formalised Optimisation and Regression in Constructive Univalent Mathematics
by: Ambridge, Todd Waugh
Published: (2024)

Extending Action Logic with Omega Iteration
by: Pshenitsyn, Tikhon
Published: (2025)

Solving Homotopy Domain Equations
by: Martínez-Rivillas, Daniel O., et al.
Published: (2021)

The $\infty$-category of $\infty$-categories in simplicial type theory
by: Gratzer, Daniel, et al.
Published: (2026)

Homotopy type theory as a language for diagrams of $\infty$-logoses
by: Uemura, Taichi
Published: (2022)