Zulip Chat Archive
Stream: Type theory
Topics:
- Extending judgmental equality by hand (9 messages, latest: Mar 22 2021 at 11:27)
- Do identity types reduce to non-indexed W-types? (3 messages, latest: Mar 14 2021 at 12:19)
- De Bruijn indexing for inductive types (2 messages, latest: Mar 10 2021 at 09:25)
- Algebro-geometric model for dependent type theory (12 messages, latest: Mar 02 2021 at 22:12)
- Measuring the complexity of terms (27 messages, latest: Feb 10 2021 at 16:17)
- The
{}
annotation for inductive types (12 messages, latest: Dec 23 2020 at 02:20) - Why use propositions as types? (36 messages, latest: Nov 16 2020 at 23:44)
- externalization (10 messages, latest: Aug 27 2020 at 20:46)
- Modelling a Type Theory in Lean (637 messages, latest: Aug 07 2020 at 14:00)
- Weak Head Normalization (4 messages, latest: Jul 17 2020 at 01:47)
- coq's type theory (40 messages, latest: May 26 2020 at 11:37)
- How to get HoTT people into Lean (294 messages, latest: May 16 2020 at 20:59)
- Model structure on simplicial sets (44 messages, latest: May 16 2020 at 12:17)
- Math on lists (18 messages, latest: May 15 2020 at 16:37)
- modeling MLTT (22 messages, latest: May 14 2020 at 14:49)
- Podcast (9 messages, latest: May 13 2020 at 20:51)
- Classical logic (7 messages, latest: May 13 2020 at 08:05)
- stream events (1 message, latest: Apr 28 2020 at 13:07)
Last updated: Apr 16 2021 at 19:18 UTC