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