Homotopy Type Theory Category — redirected to nlab

Overview

The Homotopy Type Theory wiki has 544 pages in this category.

Pages

• 2-poset > history
• 2-poset of partial maps > history
• 2-preorder > history
• A Cubical Approach to Synthetic Homotopy Theory > history
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory > history
• A3-space > history
• abelian group > history
• abelian group homomorphism > history
• about > history
• action > history
• Agda > history
• algebra (module theory) > history
• algebra (ring theory) > history
• Algebra > history
• algebraic formulation of dependent type theory > history
• algebraic limit field > history
• Ali Caglayan > history
• an axiomatization of the real numbers > history
• Analysis > history
• analytic Markov's principle > history
• Anders Mörtberg > history
• Andrea Vezzosi > history
• Andrej Bauer > history
• Andrew M. Pitts > history
• Anthony Bordg > history
• antiderivative > history
• antitonic function > history
• apartness relation > history
• Archimedean ordered abelian group > history
• Archimedean ordered field > history
• Archimedean ordered integral domain > history
• axiom of replacement > history
• axiom R-flat > history
• axioms > history
• Bas Spitters > history
• Benedikt Ahrens > history
• Benno van den Berg > history
• biaction > history
• bidirectional sequence > history
• bilinear function > history
• bimodule > history
• bimodule homomorphism > history
• Bonn2018 > history
• book homotopy type theory > history
• Book HoTT > history
• Boolean dagger 2-poset > history
• Boolean topical dagger 2-poset > history
• Boolean W-topical dagger 2-poset > history
• booleans > history
• braided monoidal dagger category > history
• Calculating the fundamental group of the circle in homotopy type theory > history
• cancellation ring > history
• cancellation Z-algebra > history
• Carlo Angiuli > history
• cartesian dagger 2-poset > history
• cartesian monoidal dagger category > history
• Categorical Homotopy Type Theory > history
• Categorical SEAR > history
• category > history
• category of maps > history
• category of monic maps > history
• category of partial functions in a set > history
• category theory > history
• Cauchy approximation > history
• Cauchy complete Archimedean ordered field > history
• Cauchy net > history
• Cauchy real numbers (disambiguation) > history
• Cauchy sequence > history
• Cauchy structure > history
• Cellular Cohomology in Homotopy Type Theory > history
• Cesare Gallozzi > history
• characteristic > history
• choice dagger 2-poset > history
• choice topical dagger 2-poset > history
• Chris Kapulkin > history
• circle > history
• Clifford algebra > history
• closed interval > history
• CMU local activities > history
• cocartesian monoidal dagger category > history
• coherent dagger 2-poset > history
• cohesive homotopy type theory > history
• cohomology > history
• commutant > history
• commutative A3-space > history
• commutative algebra (ring theory) > history
• commutative cancellation ring > history
• commutative discrete cancellation ring > history
• commutative discrete division ring > history
• commutative discrete reciprocal ring > history
• commutative division ring > history
• commutative Heyting cancellation ring > history
• commutative Heyting division ring > history
• commutative Heyting reciprocal ring > history
• commutative monoid > history
• commutative reciprocal ring > history
• commutative ring > history
• compact closed dagger category > history
• compact connected space > history
• computable real numbers > history
• concrete category > history
• concrete H-precategory > history
• concrete precategory > history
• cone type > history
• conjunctive dagger 2-poset > history
• continuous mapping > history
• contractibility of Dedekind real numbers > history
• contractible type > history
• Covering Spaces in Homotopy Type Theory > history
• dagger 2-poset > history
• dagger 2-poset with elements > history
• dagger 2-preorder > history
• dagger category > history
• dagger epimorphism in a dagger precategory > history
• dagger monomorphism in a dagger precategory > history
• dagger precategory > history
• Dan Grayson > history
• Dan Licata > history
• Daniel Christensen > history
• David Roberts > history
• de Morgan's law > history
• decidable directed graph > history
• decidable existential quantifier > history
• decidable open interval > history
• decidable preordered type > history
• decidable set > history
• decidable setoid > history
• decidable strict order > history
• decidable subset > history
• decidable universal quantifier > history
• decimal interval coalgebra > history
• decimal numbers > history
• decimal numeral representations of the natural numbers > history
• Dedekind complete Archimedean ordered field > history
• Dedekind complete Archimedean ordered integral domain > history
• Dedekind cut (disambiguation) > history
• Dedekind cut > history
• Dedekind cut structure > history
• Dedekind cut structure real numbers > history
• Dedekind real closed intervals > history
• Dedekind real numbers (disambiguation) > history
• Dedekind real numbers > history
• Dedekind real unit interval > history
• definitional equality > history
• Denis-Charles Cisinski > history
• dense relation > history
• dense strict order > history
• dependent type > history
• dependent type theory > history
• desired articles > history
• diagonal > history
• difference quotient > history
• differentiable function > history
• differential cohesive homotopy type theory > history
• Differential geometry > history
• Dimitris Tsementzis > history
• directed graph > history
• directed type > history
• directed-complete poset > history
• directional derivative > history
• directionally differentiable function > history
• discrete cancellation ring > history
• discrete cancellation Z-algebra > history
• discrete division ring > history
• discrete division Z-algebra > history
• discrete domain > history
• discrete field > history
• discrete GCD domain > history
• discrete integral domain > history
• Discrete mathematics > history
• discrete reciprocal ring > history
• discrete reciprocal Z-algebra > history
• discrete skewfield > history
• distributive lattice > history
• divisible group > history
• division dagger 2-poset > history
• division ring > history
• division Z-algebra > history
• divison ring > history
• DMV2015 > history
• domain (ring theory) > history
• double negation > history
• dyadic interval coalgebra > history
• Ed Morehouse > history
• effective epic function > history
• Egbert Rijke > history
• Eilenberg-MacLane space > history
• Eilenberg-MacLane Spaces in Homotopy Type Theory > history
• elementarily topical dagger 2-poset > history
• elementary (infinity,1)-topos > history
• Emily Riehl > history
• empty type > history
• enriched poset > history
• entire dagger morphism in a dagger 2-poset > history
• entire relation > history
• equivalence > history
• equivalence of precategories > history
• Eric Finster > history
• Eric Finster, Towards Higher Universal Algebra in Type Theory > history
• essentially small type > history
• essentially surjective > history
• ETCR > history
• ETCS as a dependent type theory > history
• ETCS with elements > history
• Eudoxus real numbers > history
• evaluational category > history
• Evan Cavallo > history
• Events > history
• excluded middle > history
• extended Dedekind cut > history
• extensional category > history
• extensional dagger 2-poset > history
• family of objects in a concrete H-precategory > history
• family of objects in a concrete precategory > history
• fiber > history
• field (ring theory) > history
• filter > history
• filtered algebra > history
• finite type > history
• Floris van Doorn > history
• Formalized Homotopy Theory > history
• frame > history
• fully faithful > history
• function algebra > history
• function extensionality > history
• function limit space > history
• function type > history
• functional dagger morphism in a dagger 2-poset > history
• functional relation > history
• functor > history
• functor precategory > history
• GCD domain > history
• generalized Cauchy real numbers > history
• geometric algebra > history
• geometric dagger 2-poset > history
• geometrically contractible space > history
• graded module > history
• Grothendieck (infinity,1)-topos > history
• group > history
• grouplike A3-space > history
• groupoid > history
• groupoid enriched in monoids > history
• Guillaume Brunerie > history
• H-magmoid > history
• H-precategory > history
• H-space > history
• H-spaceoid > history
• halving group > history
• Hausdorff ring > history
• Hausdorff space > history
• Heyting algebra > history
• Heyting cancellation ring > history
• Heyting cancellation Z-algebra > history
• Heyting dagger 2-poset > history
• Heyting division ring > history
• Heyting division Z-algebra > history
• Heyting domain > history
• Heyting field > history
• Heyting GCD domain > history
• Heyting integral domain > history
• Heyting reciprocal ring > history
• Heyting reciprocal Z-algebra > history
• Heyting skewfield > history
• Higher algebra > history
• Higher Groups in Homotopy Type Theory > history
• higher inductive type > history
• higher observational type theory > history
• Higher-Dimensional Types in the Mechanization of Homotopy Theory > history
• HilbR > history
• hom functor > history
• HomePage
• homotopy > history
• homotopy equivalence > history
• homotopy groups of spheres > history
• homotopy level > history
• Homotopy limits in type theory > history
• homotopy type > history
• Homotopy Type System > history
• homotopy type theory > history
• Hopf construction > history
• HoTT book > history
• HoTT book real numbers > history
• HoTT Mini-Course > history
• HoTT2019 Summer School open problems list > history
• Ian Orton > history
• ideal (ring theory) > history
• identity system > history
• identity type > history
• image > history
• inductive-inductive type > history
• inductive-recursive type > history
• infinite decimal representation of a unit interval > history
• infinitely iterated inverse image > history
• infinitesimal shape > history
• infinitesimally thickened point > history
• infinity-group > history
• injective dagger morphism in a dagger 2-poset > history
• integers > history
• integral domain > history
• intermediate value theorem > history
• interval cut > history
• interval-complete strict order > history
• inverse image > history
• inverse series operator > history
• irrational numbers > history
• isomorphism in a precategory > history
• iterated differentiable function > history
• iterated inverse image > history
• James construction > history
• James Ladyman > history
• Jason Gross > history
• Jeremy Avigad > history
• join > history
• join-semilattice > history
• Kristina Sojakova > history
• Kuen-Bang Hou (Favonia) > history
• Large types > history
• lattice > history
• left adjoint > history
• left shift operator > history
• limit of a binary function approaching a diagonal > history
• limit of a function > history
• limit of a net > history
• limit of a sequence > history
• limited principle of omniscience > history
• locale of open intervals > history
• localization > history
• Localization in Homotopy Type Theory > history
• locally Heyting-algebraic 2-poset > history
• locally small type > history
• locator > history
• Logic > history
• loop space > history
• loop space of a wedge of circles > history
• lower bounded open interval > history
• lower type > history
• Luis Scoccola > history
• magma > history
• map in a dagger 2-poset > history
• map-evaluational dagger 2-poset > history
• map-extensional dagger 2-poset > history
• Martin-Loef type theory > history
• Martin-Löf Type Theory > history
• Martín Escardó > history
• Matthieu Sozeau > history
• measure > history
• meet-semilattice > history
• Michael Shulman > history
• Michael Warren > history
• Modalities in homotopy type theory > history
• model invariance problem > history
• model of type theory in an (infinity,1)-topos > history
• modulated Cauchy real numbers > history
• module > history
• modulus of Cauchy convergence > history
• monic function > history
• monic map in a dagger 2-poset > history
• monoid > history
• monoidal dagger category > history
• monotonic function > history
• Morgan Opie > history
• multivalued function > history
• natural model > history
• natural numbers > history
• natural transformation > history
• net > history
• Newton-Leibniz operator > history
• Nicola Gambino > history
• Nicolai Kraus > history
• nlab
• Number theory > history
• omega-complete poset > history
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory > history
• On the homotopy groups of spheres in homotopy type theory > history
• onto dagger morphism in a dagger 2-poset > history
• open interval > history
• open problems > history
• opposite precategory > history
• opposite preorder > history
• order > history
• Order theory > history
• ordered abelian group > history
• ordered field > history
• ordered integral domain > history
• Paige North > history
• Paolo Capriotti > history
• partial derivative > history
• partial function > history
• partial function classifier > history
• partial order > history
• Per Martin-Löf > history
• Peter Arndt > history
• Peter LeFanu Lumsdaine > history
• Pieter Hofstra > history
• pointed connected groupoid > history
• pointed type > history
• pointwise continuous function > history
• polynomial function > history
• polynomial ring > history
• power dagger 2-poset > history
• power function > history
• power-associative magma > history
• pre-algebra real numbers > history
• precategory > history
• preconvergence space > history
• predicate > history
• premetric space > history
• preorder > history
• prespectrum > history
• probability measure > history
• probability valuation > history
• product precategory > history
• Proof Assistants > history
• proof theoretic strength of univalent type theory plus HITs > history
• proposition > history
• propositional logic > history
• pushout > history
• Q-algebra > history
• quadratic form > history
• quadratic function > history
• quiver > history
• quotient set > history
• rational function > history
• Rational homotopy theory > history
• rational homotopy type > history
• rational interval coalgebra > history
• rational numbers > history
• rational root theorem > history
• rationalization of a simply connected type > history
• rationalization of an abelian group > history
• real Clifford algebra > history
• real geometric algebra > history
• real numbers > history
• real vector space > history
• realizability > history
• reciprocal function > history
• reciprocal ring > history
• reciprocal Z-algebra > history
• reduction > history
• References > history
• Rel > history
• relation > history
• relational dagger 2-poset > history
• representable functor > history
• representably concrete category > history
• Resources > history
• Rezk completion > history
• Richard Garner > history
• right shift operator > history
• ring > history
• Robert Harper > history
• SEAR > history
• Seifert-van Kampen theorem > history
• semantics > history
• semi-simplicial types > history
• semiadditive dagger 2-poset > history
• semiadditive dagger category > history
• SEPS > history
• sequence > history
• sequential antiderivative > history
• sequential convergence space > history
• sequential derivative > history
• sequential polynomial > history
• sequentially Cauchy complete Archimedean ordered field > history
• sequentially Hausdorff space > history
• series operator > history
• set > history
• setoid > history
• shape > history
• Sierpinski space > history
• sigma-complete lattice > history
• sigma-continuous probability valuation > history
• sigma-continuous valuation > history
• sigma-frame > history
• Simon Huber > history
• simplex category > history
• simplicial type > history
• skewfield > history
• smash product > history
• smooth function > history
• smooth space > history
• spectral sequence > history
• spectrum > history
• spheres > history
• square function > history
• Steve Awodey > history
• strict order > history
• strongly extensional function > history
• Stuart Presnell > history
• suplattice > history
• suspension > history
• symmetric monoidal dagger category > history
• Synthetic Cohomology in Homotopy Type Theory > history
• Synthetic homotopy theory > history
• tabular dagger 2-poset > history
• Taichi Uemura > history
• Tarski universe > history
• The join construction > history
• The real projective spaces in homotopy type theory > history
• Thierry Coquand > history
• Thorsten Altenkirch > history
• Toby Bartels > history
• Topology > history
• topos > history
• torsion-free divisible group > history
• torsion-free halving group > history
• transport > history
• trilinear function > history
• type > history
• type family > history
• type theories > history
• type theory > history
• type theory over logic > history
• Ulrik Buchholtz > history
• uniformly continuous function > history
• Uniqueness of Identity Proofs > history
• unit interval > history
• unital dagger 2-poset > history
• unital Z-algebra > history
• unitary isomorphism in a dagger precategory > history
• Univalent categories and the Rezk completion > history
• univalent Martin-Loef type theory > history
• univalent type theory > history
• univalent universe > history
• univariate polynomial ring > history
• univariate rational expressions > history
• universe > history
• upper bounded open interval > history
• upper type > history
• Urs Schreiber > history
• valuation (measure theory) > history
• Vladimir Voevodsky > history
• W-topical dagger 2-poset > history
• weak equivalence of precategories > history
• wedge sum > history
• well-pointed dagger 2-poset > history
• Whitehead product > history
• Whitehead's principle > history
• wild category > history
• Yoneda lemma > history
• Z-algebra > history
• ZF > history
• Álvaro Pelayo > history
• πn(Sn) in Homotopy Type Theory > history