Setoids in type theory

DOI10.1017/S0956796802004501MaRDI QIDQ4457833zbMATH OpenOpenAlexWikidataFDO

Authors Gilles Barthe, Venanzio Capretta, Olivier Pons

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

zbMATH Keywords

dependent type theorypartial setoidrepresentation of sets as setoidstotal setoid

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(39)

• A minimalist two-level foundation for constructive mathematics
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Meaning explanations at higher dimension
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Types in class set theory and inaccessible cardinals
• Setoid type theory -- a syntactic translation
• Category theoretic structure of setoids
• Unifying exact completions
• Formalization of universal algebra in Agda
• Extending Sledgehammer with SMT solvers
• Formalizing complex plane geometry
• Invariants for the FoCaL language
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Normalization by evaluation and algebraic effects
• Constructing categories and setoids of setoids in type theory
• Type decomposition in posets
• Point-free, set-free concrete linear algebra
• Type classes for mathematics in type theory
• Towards measurable types for dynamical process modeling languages
• Packaging Mathematical Structures
• A Unified Formal Description of Arithmetic and Set Theoretical Data Types
• Setoids and universes
• Finite Groups Representation Theory with Coq
• Quotient completion for the foundation of constructive mathematics
• scientific article; zbMATH DE number 1104367 (Why is no real title available?)
• STS: a structural theory of sets
• Sets, types and type-checking
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• Constructions of categories of setoids from proof-irrelevant families
• W-types in setoids
• Logic Programming
• A formal proof of the irrationality of (3)
• Type inference for set theory
• On equality of objects in categories in constructive type theory
• Coalgebras in functional programming and type theory
• Topological quantum gates in homotopy type theory
• The relational quotient completion
• A computer-verified monadic functional implementation of the integral

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)