Topics:
- Substitution in spatial type theory (4 messages, latest: Oct 20 2025 at 09:56)
- HoTT Book (5 messages, latest: Sep 23 2025 at 15:29)
- Terry Tao on duality in logic (3 messages, latest: Jul 28 2025 at 17:21)
- Dependent function extensionality from nondependent? (23 messages, latest: Jul 16 2025 at 09:01)
- Sheafification expressed in the internal language of the top (5 messages, latest: May 23 2025 at 16:14)
- building terms, foundational considerations (12 messages, latest: May 14 2025 at 16:02)
- function application (56 messages, latest: Feb 13 2025 at 17:29)
- Backus Naur, Python (10 messages, latest: Dec 20 2024 at 14:53)
- Functions, Relations (67 messages, latest: Dec 03 2024 at 01:39)
- “Putting two things together” (5 messages, latest: Nov 29 2024 at 17:37)
- channel events (1 message, latest: Nov 20 2024 at 20:42)
- Internal logic of monoidal topos? (11 messages, latest: Sep 19 2024 at 01:02)
- APG type theory (4 messages, latest: Aug 24 2024 at 19:45)
- ✔ geometric series of types (7 messages, latest: Jun 13 2024 at 18:44)
- Displayed Type Theory (18 messages, latest: Jun 10 2024 at 15:09)
- Categorical reconstruction of separation logic? (29 messages, latest: Apr 12 2024 at 13:22)
- Curry-Howard and Machine Learning (14 messages, latest: Jan 26 2024 at 17:06)
- Type theory vs set theory (63 messages, latest: Dec 06 2023 at 16:47)
- stream events (14 messages, latest: Nov 02 2023 at 11:42)
- Trying to interpret MLTT in Cat. (8 messages, latest: Aug 19 2023 at 16:57)
- semisimplicial types (73 messages, latest: Jun 23 2023 at 16:18)
- Identity type in lower universe? (9 messages, latest: Jun 22 2023 at 19:15)
- Fuzzy Type Theory (1 message, latest: Jun 15 2023 at 23:57)
- 2-morphisms as computation (14 messages, latest: Mar 08 2023 at 10:39)
- relevant/affine monads & theories (5 messages, latest: Sep 20 2022 at 19:46)
- higher category theory with a type theory background (7 messages, latest: May 05 2022 at 06:10)
- internal language for initial algebras (4 messages, latest: Apr 28 2022 at 02:54)
- applications of category theory in computer science (6 messages, latest: Apr 15 2022 at 10:53)
- how was Martin-Löf's 'Type in Type' theory supposed to work? (7 messages, latest: Apr 05 2022 at 17:26)
- normalisation by evaluation and sheaves (52 messages, latest: Dec 04 2021 at 20:24)
- Generalizations of inductive types (4 messages, latest: Nov 20 2021 at 10:19)
- string diagrams for dependent terms (6 messages, latest: Oct 28 2021 at 20:16)
- Computing extensional equality (24 messages, latest: Oct 01 2021 at 02:50)
- Semantics of function extensionality (19 messages, latest: Sep 01 2021 at 17:05)
- type-theoretic replacement (12 messages, latest: Aug 25 2021 at 15:01)
- Semantics of TT in univalent categories (4 messages, latest: Aug 23 2021 at 03:21)
- higher inductive types (12 messages, latest: Aug 22 2021 at 14:55)
- function extensionality in ∞-categories (9 messages, latest: Aug 20 2021 at 15:47)
- inductive type (25 messages, latest: Aug 18 2021 at 19:34)
- Higher inductive types (7 messages, latest: Aug 17 2021 at 20:54)
- Inductive type (1 message, latest: Aug 12 2021 at 09:14)
- LEM in HoTT (14 messages, latest: Aug 12 2021 at 08:58)
- homotopy type theory (19 messages, latest: Aug 11 2021 at 17:13)
- NbG vs NbE (73 messages, latest: Jul 26 2021 at 17:03)
- K and UIP (29 messages, latest: Jun 28 2021 at 22:24)
- model of univalence (107 messages, latest: Jun 28 2021 at 18:10)
- presenting categorical semantics (3 messages, latest: Jun 27 2021 at 21:10)
- Presenting categorical semantics (18 messages, latest: Jun 26 2021 at 15:37)
- Model of univalence (38 messages, latest: May 12 2021 at 21:17)
- applications of categorical logic (45 messages, latest: May 10 2021 at 23:28)
- "Intuitionistic type theory" (8 messages, latest: May 04 2021 at 17:35)
- equalizers (45 messages, latest: Apr 25 2021 at 02:56)
- How was Martin-Löf's 'Type in Type' theory supposed to work? (11 messages, latest: Apr 11 2021 at 14:13)
- implications of type theory on foundations/finitism/etc. (32 messages, latest: Apr 10 2021 at 17:31)
- self-types (9 messages, latest: Mar 06 2021 at 15:08)
- generating type theories (25 messages, latest: Dec 22 2020 at 23:43)
- Normalization by Evaluation (43 messages, latest: Dec 05 2020 at 13:25)
- weak homotopy equivalence of types (13 messages, latest: Dec 04 2020 at 16:11)
- dependent types (76 messages, latest: Sep 15 2020 at 14:28)
- Do we need dependant types? (7 messages, latest: Jul 11 2020 at 15:40)
- Type Theory based on Dependent Inductive/Coindinductive Typs (28 messages, latest: Jun 27 2020 at 18:39)
- MLTT as the internal language of LCCCs (26 messages, latest: Apr 18 2020 at 00:58)
- cats in types (18 messages, latest: Apr 16 2020 at 10:14)
- substructural logics (14 messages, latest: Apr 16 2020 at 00:10)
- W-types and CFGs (11 messages, latest: Apr 02 2020 at 16:00)
