The compatibility of the minimalist foundation with homotopy type theory (Q6122600): Difference between revisions

@@ Property / OpenAlex ID @@
+W4392066353
@@ Property / OpenAlex ID: W4392066353 / rank @@
+Normal rank
@@ Property / cites work @@
+Setoid type theory -- a syntactic translation
@@ Property / cites work: Setoid type theory -- a syntactic translation / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic fixed point logic
@@ Property / cites work: Intuitionistic fixed point logic / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+On Higher Inductive Types in Cubical Type Theory
@@ Property / cites work: On Higher Inductive Types in Cubical Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity and homotopy canonicity for cubical type theory
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Conservativity of equality reflection over intensional type theory
+Normal rank
@@ Property / cites work @@
+Extensional Constructs in Intensional Type Theory
@@ Property / cites work: Extensional Constructs in Intensional Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
+Normal rank
@@ Property / cites work @@
+Q4853985
@@ Property / cites work: Q4853985 / rank @@
+Normal rank
@@ Property / cites work @@
+Modular correspondence between dependent type theories and categories including pretopoi and topoi
+Normal rank
@@ Property / cites work @@
+A minimalist two-level foundation for constructive mathematics
+Normal rank
@@ Property / cites work @@
+On Choice Rules in Dependent Type Theory
@@ Property / cites work: On Choice Rules in Dependent Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4360856
@@ Property / cites work: Q4360856 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099614
@@ Property / cites work: Q4099614 / rank @@
+Normal rank
@@ Property / cites work @@
+A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
+Normal rank
@@ Property / cites work @@
+Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
+Normal rank
@@ Property / cites work @@
+Q5009707
@@ Property / cites work: Q5009707 / rank @@
+Normal rank
@@ Property / cites work @@
+Wellfounded trees in categories
@@ Property / cites work: Wellfounded trees in categories / rank @@
+Normal rank
@@ Property / cites work @@
+Elementary quotient completion
@@ Property / cites work: Elementary quotient completion / rank @@
+Normal rank
@@ Property / cites work @@
+Quotient completion for the foundation of constructive mathematics
+Normal rank
@@ Property / cites work @@
+Relating Quotient Completions via Categorical Logic
+Normal rank
@@ Property / cites work @@
+Q5718565
@@ Property / cites work: Q5718565 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Sets in homotopy type theory
@@ Property / cites work: Sets in homotopy type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Higher Inductive Types as Homotopy-Initial Algebras
+Normal rank
@@ Property / cites work @@
+Independence of the induction principle and the axiom of choice in the pure calculus of constructions
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:6122600