scientific article; zbMATH DE number 1420793
From MaRDI portal
Publication:4944857
Recommendations
- Type theory in type theory using quotient inductive types
- Constructing infinitary quotient-inductive types
- Quotients over Minimal Type Theory
- Extensional quotients for type theory and the consistency problem for NF
- Quotient topologies in constructive set theory and type theory
- Quotients, inductive types, and quotient inductive types
- An effective theory of type refinements
- scientific article; zbMATH DE number 1927427
- Quotient inductive-inductive types
- A type theoretic interpretation of constructive domain theory
Cited in
(16)- A minimalist two-level foundation for constructive mathematics
- Inductively generated formal topologies.
- Some points in formal topology.
- Unique existence, approximate solutions, and countable choice.
- A cartesian closed category in Martin-Löf's intuitionistic type theory
- Quotient topologies in constructive set theory and type theory
- Formal Zariski topology: Positivity and points
- Type theory in type theory using quotient inductive types
- A minimalist foundation at work
- Equalisers of frames in constructive set theory
- scientific article; zbMATH DE number 2003152 (Why is no real title available?)
- Quotients by idempotent functions in Cedille
- The law of excluded middle in the simplicial model of type theory
- Quotients over Minimal Type Theory
- Division by two, in homotopy type theory
- The Zariski spectrum as a formal geometry
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4944857)
