W-types in setoids

zbMath1505.03029arXiv1809.02375MaRDI QIDQ5155691

Jacopo Emmenegger

Publication date: 8 October 2021

Full work available at URL: https://arxiv.org/abs/1809.02375

zbMATH Keywords

Martin-Löf type theorypolynomial functorsW-typessetoids

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Type theory (03B38)

Uses Software

• Coq
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quotient completion for the foundation of constructive mathematics
• Inductive types and exact completion
• Proof-relevance of families of setoids and identity in type theory
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• A minimalist two-level foundation for constructive mathematics
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Wellfounded trees in categories
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Constructing categories and setoids of setoids in type theory
• Homotopy-Initial Algebras in Type Theory
• Setoids in type theory
• Polynomial functors and polynomial monads
• A set constructor for inductive sets in Martin-Löf's type theory
• EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS
• Relating Quotient Completions via Categorical Logic
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Types for Proofs and Programs
• Sets in homotopy type theory

This page was built for publication: W-types in setoids