Pages that link to "Item:Q5420262"

The following pages link to Homotopy Type Theory: Univalent Foundations of Mathematics (Q5420262):

Displaying 50 items.

• Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
• Canonicity of weak \(\omega\)-groupoid laws using parametricity theory (Q283766) (← links)
• A constructive manifestation of the Kleene-Kreisel continuous functionals (Q290639) (← links)
• The intrinsic topology of Martin-Löf universes (Q290640) (← links)
• The categorical imperative: category theory as a foundation for deontic logic (Q472796) (← links)
• The category of equilogical spaces and the effective topos as homotopical quotients (Q504545) (← links)
• Univalence in locally Cartesian closed categories (Q524707) (← links)
• A dependent type theory with abstractable names (Q530845) (← links)
• Isomorphism is equality (Q740487) (← links)
• The future of mathematics in economics: a philosophically grounded proposal (Q1616105) (← links)
• Aligning concepts across proof assistant libraries (Q1640642) (← links)
• Game semantics for dependent types (Q1641014) (← links)
• Decomposition spaces, incidence algebras and Möbius inversion. I: Basic theory (Q1647403) (← links)
• Univalent completion (Q1659918) (← links)
• Homotopy type theory in Lean (Q1687770) (← links)
• Constructive knowledge and the justified true belief paradigm (Q1688952) (← links)
• To be or not to be constructive, that is not the question (Q1688964) (← links)
• Klein-Weyl's program and the ontology of gauge and quantum systems (Q1705891) (← links)
• Carnap and the invariance of logical truth (Q1708751) (← links)
• Bousfield localisation and colocalisation of one-dimensional model structures (Q1732877) (← links)
• Fibrational modal type theory (Q1744413) (← links)
• The homotopy theory of type theories (Q1785779) (← links)
• Univalence as a principle of logic (Q1788330) (← links)
• Combinatorial topology and constructive mathematics (Q1788338) (← links)
• New perspectives on the hole argument (Q1985874) (← links)
• The hole argument in homotopy type theory (Q1985880) (← links)
• The hole argument, take \(n\) (Q1985882) (← links)
• Univalent polymorphism (Q1987219) (← links)
• Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
• Construction of the circle in \textit{UniMath} (Q2031555) (← links)
• The simplicial model of univalent foundations (after Voevodsky) (Q2031691) (← links)
• A constructive approach to Freyd categories (Q2035866) (← links)
• Filter quotients and non-presentable \((\infty,1)\)-toposes (Q2040521) (← links)
• A meaning explanation for HoTT (Q2054122) (← links)
• The structuralist mathematical style: Bourbaki as a case study (Q2080585) (← links)
• Predicativity and constructive mathematics (Q2080590) (← links)
• Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
• Univalence and completeness of Segal objects (Q2104885) (← links)
• Constructive mathematics, Church's thesis, and free choice sequences (Q2117809) (← links)
• On representations of intended structures in foundational theories (Q2121479) (← links)
• Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves (Q2125994) (← links)
• From reversible programs to univalent universes and back (Q2130579) (← links)
• Finitary higher inductive types in the groupoid model (Q2130587) (← links)
• A characterisation of elementary fibrations (Q2131276) (← links)
• The construction of set-truncated higher inductive types (Q2133178) (← links)
• Homotopical inverse diagrams in categories with attributes (Q2207273) (← links)
• Graph theory in Coq: minors, treewidth, and isomorphisms (Q2209536) (← links)
• What inductive explanations could not be (Q2219138) (← links)
• Composition of deductions within the propositions-as-types paradigm (Q2228351) (← links)
• Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes (Q2229273) (← links)