Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topics:

• 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)
• Backus Naur, Python (9 messages, latest: Aug 13 2023 at 16:02)
• 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)