Zulip Chat Archive

Stream: Type theory

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