Zulip Chat Archive
Stream: Type theory
Topics:
- Are these “type erasure” axioms consistent? (5 messages, latest: Dec 17 2023 at 10:13)
- ✔ Terms of terms and the universe hierarchy (12 messages, latest: Dec 14 2023 at 01:00)
- ✔ Intro constructor (6 messages, latest: Dec 12 2023 at 16:44)
- And.rec (34 messages, latest: Nov 30 2023 at 22:55)
- Logics and lambda calculi (20 messages, latest: Nov 24 2023 at 16:58)
- Iota-reduction and rfl issues (7 messages, latest: Nov 12 2023 at 19:37)
- Models of lean 4 (11 messages, latest: Oct 18 2023 at 20:34)
- kernel is_def_eq confusion (6 messages, latest: Aug 16 2023 at 20:21)
- ✔ Defeq without funext (42 messages, latest: Jun 26 2023 at 19:33)
- Functions on an inductive type (14 messages, latest: Jun 10 2023 at 12:27)
- Type theory in classical logic? (76 messages, latest: May 30 2023 at 14:50)
- You need UIP for lambda calculus (2 messages, latest: May 19 2023 at 14:20)
- Expressiveness of inductive types (28 messages, latest: May 04 2023 at 13:09)
- Proving funext using quotients (11 messages, latest: Apr 16 2023 at 11:46)
- ✔ Pattern Matching to Eliminators (18 messages, latest: Mar 10 2023 at 12:14)
- Propext necessary in
Quotient.exact? (6 messages, latest: Feb 20 2023 at 06:02) - Is there mutually recursive classes? (30 messages, latest: Feb 03 2023 at 03:13)
- Why is Kripke semantics so effective? (3 messages, latest: Dec 02 2022 at 16:11)
- Type mismatch with dependent types (5 messages, latest: Aug 18 2022 at 06:59)
- Resources on type inference for dependent types (4 messages, latest: Aug 14 2022 at 19:24)
- ✔ Resources on type inference for dependent types (4 messages, latest: Jul 10 2022 at 02:52)
- Universe Polymorphism (10 messages, latest: Jun 14 2022 at 11:33)
- Double negation translations in DTT (9 messages, latest: Jun 10 2022 at 19:10)
- Substitution in Untyped Lambda Calculus (5 messages, latest: May 03 2022 at 18:32)
- second order encoding (10 messages, latest: Apr 01 2022 at 16:10)
- When does DTT fail capturing things as intended? (9 messages, latest: Feb 23 2022 at 00:18)
- lambda mu calculus (7 messages, latest: Feb 19 2022 at 02:55)
- North American Universities in Type Theory? (2 messages, latest: Feb 10 2022 at 08:40)
- Exists elimination (21 messages, latest: Jan 31 2022 at 23:05)
- Comparison with Coq (43 messages, latest: Nov 02 2021 at 23:17)
- Practical Types (656 messages, latest: Oct 22 2021 at 12:06)
- effective epimorphisms (20 messages, latest: Oct 12 2021 at 00:07)
- Noncomputable vs crisp variables (14 messages, latest: Oct 05 2021 at 23:16)
- stlc terms (338 messages, latest: Jul 30 2021 at 01:20)
- ✔ Well-founded recursion (1 message, latest: Jul 26 2021 at 02:59)
- Well-founded recursion (3 messages, latest: Jul 25 2021 at 21:37)
- Type theory w/ custom reduction rules in inductive types (21 messages, latest: Jul 17 2021 at 00:41)
- Making change to type judgement according to assumptions (34 messages, latest: Jul 02 2021 at 03:53)
- Linear Logic (162 messages, latest: Jun 29 2021 at 13:09)
- HOAS (8 messages, latest: Jun 25 2021 at 13:28)
- Definitional reduction issues in lean (2 messages, latest: Jun 03 2021 at 14:19)
- Why use propositions as types? (42 messages, latest: May 22 2021 at 17:44)
- HoTT exercises in Lean (6 messages, latest: May 22 2021 at 17:04)
- Metamathematics in lean 4 (699 messages, latest: May 03 2021 at 18:36)
- 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) - 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: Dec 20 2023 at 11:08 UTC