Setoids in type theory

DOI10.1017/S0956796802004501zbMATH Open1060.03030OpenAlexW1988136938WikidataQ56430943 ScholiaQ56430943MaRDI QIDQ4457833FDOQ4457833

Gilles Barthe, Olivier Pons, Venanzio Capretta

Publication date: 17 March 2004

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796802004501

Recommendations

• Setoids and universes
• Constructing categories and setoids of setoids in type theory
• W-types in setoids
• scientific article; zbMATH DE number 2003151
• Category theoretic structure of setoids

zbMATH Keywords

dependent type theorypartial setoidrepresentation of sets as setoidstotal setoid

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (36)

• A minimalist two-level foundation for constructive mathematics
• Unifying exact completions
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Normalization by evaluation and algebraic effects
• Quotient completion for the foundation of constructive mathematics
• Title not available (Why is that?)
• Formalization of universal algebra in Agda
• Type classes for mathematics in type theory
• Finite Groups Representation Theory with Coq
• Topological quantum gates in homotopy type theory
• Setoid type theory -- a syntactic translation
• Towards Measurable Types for Dynamical Process Modeling Languages
• STS: a structural theory of sets
• Title not available (Why is that?)
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Type inference for set theory
• Title not available (Why is that?)
• Types in class set theory and inaccessible cardinals
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Logic Programming
• W-types in setoids
• Invariants for the FoCaL language
• Formalizing complex plane geometry
• Packaging Mathematical Structures
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Coalgebras in functional programming and type theory
• Extending Sledgehammer with SMT solvers
• Meaning explanations at higher dimension
• Title not available (Why is that?)
• Proof-Relevant Logical Relations for Name Generation
• A Unified Formal Description of Arithmetic and Set Theoretical Data Types
• A computer-verified monadic functional implementation of the integral
• Constructions of categories of setoids from proof-irrelevant families
• Point-Free, Set-Free Concrete Linear Algebra
• Type decomposition in posets
• Sets, types and type-checking

This page was built for publication: Setoids in type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4457833)