scientific article; zbMATH DE number 7566071
From MaRDI portal
Publication:5094144
zbMath1502.18046arXiv2101.02994MaRDI QIDQ5094144
Andrew M. Pitts, S. C. Steenkamp, Marcelo P. Fiore
Publication date: 2 August 2022
Full work available at URL: https://arxiv.org/abs/2101.02994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
topos theorydependent type theoryhigher inductive typesquotient typeswell-founded relationweakly initial set of covers
Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The weak choice principle WISC may fail in the category of sets
- On the construction of free algebras for equational systems
- All uncountable cardinals can be singular
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Wellfounded trees in categories
- Quotient inductive-inductive types
- An algorithm for type-checking dependent types
- Finitary higher inductive types in the groupoid model
- Constructing infinitary quotient-inductive types
- Containers: Constructing strictly positive types
- Higher Inductive Types as Homotopy-Initial Algebras
- Type theory in type theory using quotient inductive types
- An Equational Metalogic for Monadic Equational Systems
- The axiom of multiple choice and models for constructive set theory
- Words, free algebras, and coequalizers
- A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
- Type Theory based on Dependent Inductive and Coinductive Types
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Semantics of higher inductive types
- A Syntax for Higher Inductive-Inductive Types
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Large and Infinitary Quotient Inductive-Inductive Types
- Indexed containers
- Embedding orders into the cardinals with \mathsf DCκ
- Heterogeneous algebras
- Intuitionistic sets and ordinals
- Types for Proofs and Programs
- Type theories, toposes and constructive set theory: Predicative aspects of AST
This page was built for publication:
