Meaning explanations at higher dimension (Q1688954): Difference between revisions

@@ Property / describes a project that uses @@
+Lean
@@ Property / describes a project that uses: Lean / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+UniMath
@@ Property / describes a project that uses: UniMath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+RedPRL
@@ Property / describes a project that uses: RedPRL / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.indag.2017.07.010
+Normal rank
@@ Property / OpenAlex ID @@
+W2765255795
@@ Property / OpenAlex ID: W2765255795 / rank @@
+Normal rank
@@ Property / cites work @@
+Computational higher-dimensional type theory
@@ Property / cites work: Computational higher-dimensional type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy theoretic models of identity types
@@ Property / cites work: Homotopy theoretic models of identity types / rank @@
+Normal rank
@@ Property / cites work @@
+Setoids in type theory
@@ Property / cites work: Setoids in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+Cubical Type Theory: a constructive interpretation of the univalence axiom
+Normal rank
@@ Property / cites work @@
+Computational foundations of basic recursive function theory
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+Q4133603
@@ Property / cites work: Q4133603 / rank @@
+Normal rank
@@ Property / cites work @@
+The identity type weak factorisation system
@@ Property / cites work: The identity type weak factorisation system / rank @@
+Normal rank
@@ Property / cites work @@
+Practical Foundations for Programming Languages
@@ Property / cites work: Practical Foundations for Programming Languages / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247303
@@ Property / cites work: Q4247303 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4490719
@@ Property / cites work: Q4490719 / rank @@
+Normal rank
@@ Property / cites work @@
+ABSTRACT HOMOTOPY
@@ Property / cites work: ABSTRACT HOMOTOPY / rank @@
+Normal rank
@@ Property / cites work @@
+Q5812175
@@ Property / cites work: Q5812175 / rank @@
+Normal rank
@@ Property / cites work @@
+A Cubical Approach to Synthetic Homotopy Theory
@@ Property / cites work: A Cubical Approach to Synthetic Homotopy Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity for 2-dimensional type theory
@@ Property / cites work: Canonicity for 2-dimensional type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Weak ω-Categories from Intensional Type Theory
@@ Property / cites work: Weak ω-Categories from Intensional Type Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3886868
@@ Property / cites work: Q3886868 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructions, proofs and the meaning of logical constants
+Normal rank
@@ Property / cites work @@
+Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume II
+Normal rank
@@ Property / cites work @@
+Types are weak <i>ω</i> -groupoids
@@ Property / cites work: Types are weak <i>ω</i> -groupoids / rank @@
+Normal rank
@@ Property / cites work @@
+Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18--20, 2011. Proceedings
+Normal rank