Bas Spitters has contributed to 136 nLab pages.

convenient category of topological spaces | 15:43:03, March 13 2021 |

countable choice | 12:59:32, March 13 2021 |

M-type | 18:21:08, February 11 2020 |

modal type theory | 12:42:41, February 01 2020 |

topological site | 08:32:58, November 15 2019 |

Johnstone's topological topos | 14:22:37, September 26 2019 |

topological site | 09:14:54, September 26 2019 |

eta-conversion | 11:39:24, September 23 2019 |

inductive-inductive type | 14:39:57, May 16 2019 |

categorical semantics of dependent type theory | 13:09:20, April 23 2019 |

geometric homotopy type theory | 12:27:39, April 19 2019 |

geometric type theory | 12:26:30, April 19 2019 |

cartesian logic | 12:30:54, April 18 2019 |

cubical type theory | 15:35:51, April 15 2019 |

M-type | 14:23:59, February 17 2019 |

cubical type theory | 11:24:19, February 15 2019 |

cubical-type model category | 10:37:13, February 15 2019 |

cubical type theory | 08:36:32, February 15 2019 |

cubical-type model category | 08:35:09, February 15 2019 |

cubical type theory | 17:34:55, February 06 2019 |

Johnstone's topological topos | 09:16:55, January 29 2019 |

(infinity,1)-topos | 12:08:57, January 16 2019 |

valuation (measure theory) | 15:21:18, January 15 2019 |

free topos | 14:58:27, January 09 2019 |

synthetic probability theory | 12:49:17, October 30 2018 |

measurable locale | 12:45:19, October 30 2018 |

essentially algebraic theory | 09:24:34, October 12 2018 |

higher inductive type | 11:57:30, October 10 2018 |

double-negation shift | 14:14:59, July 17 2018 |

monoidal topos | 14:28:18, July 07 2018 |

- (infinity,1)-topos
- Agda
- algebraic set theory
- algebraic weak factorization system
- AQFT
- Artin gluing
- Automath
- axiom of choice
- axiom of multiple choice
- Banach-Alaoglu theorem
- beable
- big and little toposes
- Bishop set
- Bishop's constructive mathematics
- Blakers-Massey theorem
- bunched logic
- cartesian logic
- categorical semantics of dependent type theory
- category of fibrant objects
- co-Heyting algebra
- Como
- computable physics
- constructive set theory
- continuous truth
- continuum mechanics
- convenient category of topological spaces
- convergence space
- Coq
- countable choice
- Crans-Gray tensor product
- cubical set
- cubical type theory
- cubical-type model category
- cyclic set
- dagger category
- dependent type theoretic methods in natural language semantics
- Diaconescu's theorem
- direct image
- directed homotopy type theory
- double-negation shift
- Döring-Harding-Hamhalter theorem
- effect algebra
- effective topological space
- elegant Reedy category
- elementary (infinity,1)-topos
- essential geometric morphism
- essentially algebraic theory
- eta-conversion
- ETCS
- fan theorem
- Fell bundle
- filter space
- flabby sheaf
- formally étale morphism
- free monad
- free topos
- Galois topos
- generalized algebraic theory
- geometric homotopy type theory
- geometric type theory
- guarded recursion
- higher inductive type
- homotopy type theory
- homotopy type theory FAQ
- Hurewicz fibration
- hypercomputation
- ideal completion
- idempotent (infinity,1)-monad
- idempotent monad
- inductive family
- inductive-inductive type
- internal diagram
- internal logic
- internal type theory
- intuitionistic mathematics
- Isbell duality
- Johnstone's topological topos
- Jordan-Banach algebra
- Kleene's second algebra
- Kochen-Specker theorem
- Kripke-Joyal semantics
- Lawvere theory
- localizable measure
- locally cartesian closed functor
- locally connected topos
- M-type
- Markov's principle
- measurable locale
- modal type
- modal type theory
- modality
- model structure on cubical sets
- monoidal topos
- Olivia Caramello
- partial map classifier
- path category
- Penrose singularity theorem
- plus construction on presheaves
- poset of commutative subalgebras
- predicative mathematics
- pseudotopological space
- Pursuing Stacks
- quasitopos
- realizability
- realizability topos
- Reedy model structure
- reflective subuniverse
- regular extension axiom
- relation between type theory and category theory
- reverse mathematics
- SEAR
- semi-simplicial set
- SimpSet
- sober topological space
- species
- stack
- structural set theory
- subsequential space
- symmetric set
- synthetic mathematics
- synthetic probability theory
- synthetic topology
- test category
- tiny object
- topological site
- topos of coalgebras over a comonad
- type refinement
- type universe
- univalence axiom
- universe in a topos
- valuation (measure theory)
- von Neumann algebra
- W-type
- WISC
- ZFC
- étale algebra