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

(38)

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