A group blog on math, physics and philosophy

- What is a Formal Proof? (Aug 8, 2016)
- Is decidable type-checking necessary for a notion of formal proof?
- Castles in the Air (May 20, 2016)
- Some thoughts on the value of nonrigorous mathematics.
- On Digital Mathematics and Drive-By Contributors (Jan 10, 2016)
- Slides from a talk about my experiences with digital mathematics.
- Internal Languages of Higher Categories (Jul 28, 2015)
- A summary of what we know and don’t know about intensional type theory (HoTT) as an internal language for higher categories (guest post by Chris Kapulkin).
- What is a Reedy Category? (Jun 29, 2015)
- A new preprint explains Reedy categories from a category-theoretic point of view, as certain iterated collages of profunctor diagrams.
- What's so HoTT about Formalization? (Jun 21, 2015)
- What is the relationship between homotopy type theory and computer formalization of mathematics?
- The Revolution Will Not Be Formalized (May 18, 2015)
- My opinion about the future of computer-verified proof.
- A Synthetic Approach to Higher Equalities (Apr 24, 2015)
- An introduction to homotopy type theory for philosophers
- HITs and the Erlangen Program (Mar 9, 2015)
- Bishop sets and Klein geometries are both quotient constructions, and can both be realized by HITs, in contrast to the univalence/extensionality based approach common in set theory.
- Introduction to Synthetic Mathematics (part 1) (Feb 26, 2015)
- A draft of an introduction to synthetic mathematics
- The Univalent Perspective on Classifying Spaces (Jan 19, 2015)
- Defining classifying spaces as full sub-groupoids of a universe can give an easier way to define morphisms between them.
- Pullbacks That Preserve Weak Equivalences (Jul 21, 2014)
- On morphisms pullback along which preserves weak equivalences, and their name(s).
- The Linearity of Traces (Jul 1, 2014)
- A success story for applied category theory: formal results about bicategorical trace imply the linearity of traces under absolute colimits.
- What is a Spectral Sequence? (Aug 4, 2013)
- Spectral sequences are to long exact sequences as iterated extensions are to extensions.
- Cohomology Detects Failures of Classical Mathematics (Jul 28, 2013)
- The axiom of choice (including the law of excluded middle) is equivalent to the statement that H^1 of all discrete sets with values in all groups vanishes.
- Higher Compactness (Jul 24, 2013)
- Compactness and local compactness are the first rungs on infinite hierarchies of conditions that can be defined using higher toposes.
- Synthetic ∞-Groupoid Theory (Jul 10, 2013)
- Homotopy type theory can be viewed as a synthetic theory of infinity-groupoids.
- The HoTT Book (Jun 20, 2013)
- The HoTT Book is out!
- The Propositional Fracture Theorem (May 16, 2013)
- The gluing construction on topological spaces and topoi seems like a “propositional” version of the fracture theorems from algebraic topology.
- Scones, Logical Relations, and Parametricity (Apr 17, 2013)
- The category-theoretic scone or “gluing construction” packages the type-theorist’s method of “logical relations” to prove canonicity and parametricity properties of type theory.
- Category Theory in Homotopy Type Theory (Mar 5, 2013)
- Doing category theory in homotopy type theory allows us to satisfy the principle of equivalence automatically.
- Presentations and Representations in Foundations (Feb 4, 2013)
- With a type-theoretic foundational system, we can describe constructions on objects with internalized universal properties, including the hom-functors of higher groupoids.
- The Universal Property of Categories (Jan 16, 2013)
- Using the theory of enriched bicategories, we can exhibit the construction of enriched categories as a free cocompletion in a world of equipments.
- Two Dimensional Monadicity (Jan 11, 2013)
- An extension of the monadicity theorem using F-categories to detect lax, pseudo, and colax morphisms provides new insight into the fundamental nature of such weak morphisms.
- From Set Theory to Type Theory (Jan 7, 2013)
- Starting from set theories like ZFC and ETCS, trying to take the best of both worlds leads us naturally to univalent type theory.
- Names For Equivalences (Dec 20, 2012)
- What names would you give to all these equivalent notions of “equivalence”?
- Enriched Indexed Categories (Dec 18, 2012)
- Enriched indexed categories, indexed over a base category and enriched over an indexed monoidal category, simultaneously generalize indexed categories, internal categories, and enriched categories.
- The Additivity of Traces in Stable Monoidal Derivators (Dec 14, 2012)
- Stable monoidal derivators give a new, easier, and more flexible context for proving the additivity of traces and generalizing it.
- Universe Polymorphism and Typical Ambiguity (Dec 9, 2012)
- “Universe polymorphism” and “typical ambiguity” are fancy words for simple language.
- Freedom From Logic (Nov 9, 2012)
- Towards a way of doing homotopy type theory informally, and a new opinion regarding propositions as types.
- Object Classifiers and (∞,1)-Quasitoposes (Oct 18, 2012)
- A preprint by Gepner and Kock about object classifiers in (infinity,1)-toposes and (infinity,1)-quasitoposes.
- Gauge Spaces and the Stone-Cech Compactification (Sep 14, 2012)
- Some expository notes developing the Stone-Cech compactification using gauge spaces instead of topological spaces.
- Every Functor is a (Co)Reflection (Sep 10, 2012)
- Every functor can be made into a reflection or coreflection by changing its domain. There is a formal and unenlightening proof, but for some examples we can find “natural” proofs which are actually informative.
- Brown representability (Aug 24, 2012)
- Surprisingly enough, Brown’s representability theorem is false for nonconnected or unpointed spaces.
- Zero-Determinant Strategies in the Iterated Prisoner's Dilemma (Jul 19, 2012)
- A revolutionary paper by Press and Dyson describes surprising and exciting new strategies for the Iterated Prisoner’s Dilemma – but they don’t “beat” TIT FOR TAT unless we change the way we measure victory.
- The Gamification of Higher Category Theory (Jun 18, 2012)
- Coq, meet DragonBox.
- Directed Homotopy Type Theory (Jun 7, 2012)
- The internal homotopy type theory of the (infinity,1)-topos of simplicial objects gives us a “directed homotopy type theory” to talk about (infinity,1)-categories.
- Superextensive Sites (May 21, 2012)
- “Superextensive sites” allow us to replace covering families by singleton covers… sometimes.
- Postulated Colimits and Absolute Colimits (May 14, 2012)
- Absolute colimits, those which are preserved by any functor, are a special case of Anders Kock’s notion of “postulated colimit.”
- The Mysterious Nature of Right Properness (May 7, 2012)
- What does right properness of a model category mean?
- PSSL 93 trip report (Apr 25, 2012)
- A report on several talks from the PSSL 93 in Cambridge.
- Exact completions and small sheaves (Mar 21, 2012)
- Most kinds of exact completion, including categories of sheaves, are a special case of a reflection from certain sites into higher-ary exact categories.
- The Multiplicativity of Fixed-Point Invariants (Mar 6, 2012)
- A bicategorical point of view on fixed-point invariants implies a general multiplicativity theorem.
- Propositions as Some Types and Algebraic Nonalgebraicity (Jan 12, 2012)
- Different ways to relate proofs with constructions in foundational theories, and why homotopy type theory makes the choice it does.
- Cellularity in Algebraic Model Structures (Dec 9, 2011)
- Constructing algebraic versions of model structures, Quillen adjunctions, and monoidal model structures using cellularity of the generators.
- Reflective Subfibrations, Factorization Systems, and Stable Units (Dec 6, 2011)
- When can a reflective subcategory be extended to a reflective subfibration or a stable factorization system?
- Internalizing the External, or The Joys of Codiscreteness (Nov 29, 2011)
- An internal axiomatization of factorization systems, subtoposes, local toposes, and cohesive toposes in homotopy type theory, using “higher modality” and codiscreteness.
- Discreteness, Concreteness, Fibrations, and Scones (Nov 22, 2011)
- Categories of spaces with discrete and codiscrete objects are closely related to fibrations and opfibrations; the “scone” freely adds both codiscrete objects and cartesian arrows.
- Productive Homotopy Pullbacks (Nov 7, 2011)
- Certain squares built out of cartesian products are always homotopy pullbacks, in any derivator.
- Traces in Indexed Monoidal Categories (Nov 4, 2011)
- Indexed monoidal categories and their string diagrams provide a nice framework for generalized fixed point theory.
- Fixed Point Indices for Groupoids (Aug 20, 2011)
- Can you define the fixed-point index for finitely generated free groupoids in a purely categorical way?
- Coinductive Definitions (Jul 30, 2011)
- Coinductive definitions are just as basic as inductive ones, and are an important tool for working with ω-categories.
- Flat Functors and Morphisms of Sites (Jun 19, 2011)
- Two classical notions of flat functor have a common generalization, leading to a better category of sites.
- Homotopy Type Theory, VI (Apr 24, 2011)
- A homotopical extension of the notion of “inductive definition” allows us to construct CW complexes and mimic other constructions from homotopy theory in type theory.
- Enhanced 2-categories and Limits for Lax Morphisms (Apr 13, 2011)
- What 2-categorical limits are there in the 2-category of algebras and lax morphisms for a 2-monad?
- Homotopy Type Theory, V (Apr 12, 2011)
- What’s still missing to make homotopy type theory into a complete internal language for (∞,1)-topoi?
- Homotopy Type Theory, IV (Apr 5, 2011)
- Voevodsky’s “univalence axiom” for universes in homotopy type theory, and the equivalent principle of “equivalence induction.”
- Homotopy Type Theory, III (Mar 24, 2011)
- Some more discussion of the notions of “equivalence” in homotopy type theory.
- Homotopy Type Theory, II (Mar 18, 2011)
- Continuing from last time, we define sets and logic in terms of homotopy type theory.
- Homotopy Type Theory, I (Mar 11, 2011)
- An overview of the correspondence between homotopical structures and intensional type theory.
- Concrete ∞-Categories (Feb 16, 2011)
- Is there a notion of “concrete ∞-category”?
- Punctual Local Connectedness (Feb 11, 2011)
- A new paper by Peter Johnstone shows that Lawvere’s “pieces have points” axiom has some surprisingly strong consequences.
- Topos Theory Can Make You a Predicativist (Jan 23, 2011)
- Working with higher topoi, and being used to negative thinking, can make predicative mathematics seem both more appealing and more feasible.
- Internal Categories, Anafunctors and Localisations (Nov 29, 2010)
- guest post by David Roberts This post is about my forthcoming paper, extracted from chapter 1 of my thesis: Internal categories, anafunctors and localisations and is also a bit of a call for examples from nn-category cafe visitors (see…
- Locally Constant Sheaves (Nov 25, 2010)
- What is the right definition of a locally constant sheaf on a non-locally-connected space?
- Universe Enlargement (Nov 23, 2010)
- Ways to enlarge a category to live in a different universe.
- Petit (∞,1)-Toposes (Oct 26, 2010)
- (∞,1)-toposes, regarded as generalized spaces, provide a context in which to relate spaces to ∞-groupoids in a universal way.
- Structure-Like Stuff (Oct 4, 2010)
- The notion of ‘property-like structure’ suggests a categorified version of ‘structure-like stuff’ – are there any examples?
- Grothendieck-Maltsiniotis ∞-categories (Sep 15, 2010)
- Georges Maltsiniotis has posted a new definition of ∞-category, whose groupoidal version is said to be due to Grothendieck.
- The Geometry of Monoidal Fibrations? (Aug 26, 2010)
- Does it exist?
- LaTeX Overflow (Aug 4, 2010)
- A new question+answer site for TeX questions
- Ternary Factorization Systems (Jul 24, 2010)
- Defining ternary factorization systems in terms of binary ones.
- What is a Theory? (Jul 14, 2010)
- Is a syntactically presented theory as important as its walking model?
- Exact Squares (Jun 21, 2010)
- The calculus of exact squares for computing with Kan extensions isn’t well-known in some circles, but it has the advantage of generalizing well to derivators and (∞,1)-categories.
- Tensor Categories in Fredericton (Jun 7, 2010)
- Some highlights from the Tensor Categories session at the CMS 2010 summer meeting in Fredericton.
- Squeezing Higher Categories out of Lower Categories (May 18, 2010)
- By using homotopy 2-categories and derivators, we can squeeze a lot of information out of (infinity,1)-categories using only comparatively easy 2-categorical machinery.
- Understanding the Homotopy Coherent Nerve (Apr 29, 2010)
- An easier-to-understand description of the left adjoint to the homotopy coherent nerve, due to Dugger and Spivak, enables us to make explicit computations of its hom-spaces, and better understand the relationship between quasicategories and simplicial categories.
- Confessions of a Higher Category Theorist (Apr 29, 2010)
- Why might we continue to search for more models for higher categories, aside from the simplicial ones that have proven so useful?
- Symmetric Monoidal Bicategories and (n×k)-categories (Apr 8, 2010)
- Monoidal bicategories can be constructed easily from “fibrant” monoidal double categories, and likewise for higher n-categories.
- Extraordinary 2-Multicategories (Mar 30, 2010)
- The still-hypothetical notion of “extraordinary 2-multicategory” generalizes a 2-category just enough to include extraordinary natural transformations.
- Stack Semantics (Mar 23, 2010)
- The stack semantics extends the internal logic of a topos to handle unbounded quantifiers in a category-theoretic way.
- In Praise of Dependent Types (Mar 3, 2010)
- Dependent types should be everyone’s friend!
- Equivariant Stable Homotopy Theory (Jan 24, 2010)
- Trying to understand equivariant stable homotopy theory from a higher-categorical perspective.
- Generalized Multicategories (Jan 4, 2010)
- A brief introduction to generalized multicategories, in honor of a new draft of a paper about them.
- The Problem With Lax Functors (Dec 12, 2009)
- There is no 3-category which includes 2-categories, lax functors, and any of the usual sorts of transformations.
- Syntax, Semantics, and Structuralism II (Dec 8, 2009)
- Structural set theories such as ETCS provide an alternate foundation for mathematics, which is arguably closer to mathematical practice than ZF-like “material” set theories.
- Size, Yoneda, and Limits of Algebras (Dec 2, 2009)
- A clever Yoneda argument shows that modulo size concerns, if completeness lifts to categories of algebras, then so do all individual limits. It’s interesting to compare how different approaches to size deal with this.
- Feferman Set Theory (Nov 30, 2009)
- (Strong) Feferman set theory provides a set-theoretic foundation for category theory that avoids many of the problems with other approaches such as Grothendieck universes.
- Equipments (Nov 23, 2009)
- An enhanced structure on a 2-category, called a “proarrow equipment,” lets us define weighted limits and develop a good deal of “formal category theory.”
- Combinatorial-Game Categories (Nov 16, 2009)
- Joyal’s category of Conway games is the initial “combinatorial-game category.” What is the terminal one?
- Generalized Operads in Classical Algebraic Topology (Oct 30, 2009)
- Two obscure-seeming kinds of generalized operad help make categorical sense out of two constructions in classical algebraic topology.
- Aesthetics of Commutative Diagrams (Oct 21, 2009)
- How to lay out a large commutative diagram aesthetically?
- Syntax, Semantics, and Structuralism, I (Oct 19, 2009)
- A brief summary of syntax and semantics of type theory and logic, as a basis for continuing discussions about structural and material foundations.
- Associativity Data in an (∞,1)-Category (Oct 8, 2009)
- Guest post by Emily Riehl A popular slogan is that (∞,1)(\infty,1)-categories (also called quasi-categories or ∞\infty-categories) sit somewhere between categories and spaces, combining some of the features of both. The analogy with spaces is fairly clear, at least to…

- 0
- Accessibility Statement
- 1
- Main Page
- 2
- Skip to Content
- 3
- List of Posts
- 4
- Search
- p
- Previous (individual/monthly archive page)
- n
- Next (individual/monthly archive page)