Zulip Chat Archive

Stream: Type theory

Topics:

paraconsistent type theory (10 messages, latest: Feb 22 2026 at 21:51)
Equality without axioms (39 messages, latest: Feb 12 2026 at 10:40)
Ordinal notations and QPF (2 messages, latest: Jan 19 2026 at 19:39)
Can ZFC model restricted Lean? (115 messages, latest: Jan 08 2026 at 12:30)
Impossibility Theorems for Fixed-Axis Classification Systems (1 message, latest: Jan 07 2026 at 04:11)
Do Lean and Set theory prove the same arithmetic facts? (11 messages, latest: Jan 01 2026 at 20:45)
major and minor premises of a recursor (5 messages, latest: Dec 09 2025 at 04:26)
What is a Sort and how is it realted to Universes? (34 messages, latest: Dec 02 2025 at 12:20)
Simple Type Theory definitions & Theorems (6 messages, latest: Nov 28 2025 at 19:24)
Indexed QPF (1 message, latest: Nov 08 2025 at 08:58)
Lean4Lean progress (7 messages, latest: Sep 23 2025 at 23:14)
Level normalization (19 messages, latest: Sep 18 2025 at 12:01)
Paradoxes and Type Universes (17 messages, latest: Sep 06 2025 at 16:50)
why proof irrelevance? (23 messages, latest: Aug 30 2025 at 05:04)
Definitional well-founded recursion (23 messages, latest: Aug 21 2025 at 16:53)
Subject reduction failure, applications? (8 messages, latest: Aug 08 2025 at 00:12)
Structural recursion on Prop (19 messages, latest: Jul 08 2025 at 09:29)
injectivity of my own inductive (13 messages, latest: Jul 01 2025 at 12:21)
Pi as a functor (27 messages, latest: Jun 30 2025 at 02:15)
Judgemental equality underapproximation (5 messages, latest: Jun 29 2025 at 15:13)
Infinite product of types (7 messages, latest: May 25 2025 at 00:45)
Can Squash.mk x = Squash.mk y be made true by definition? (21 messages, latest: May 22 2025 at 14:29)
Recommendations to learn about type theory rigorously (5 messages, latest: Feb 17 2025 at 01:57)
Injectivity of Pi type "constructors" (19 messages, latest: Feb 11 2025 at 08:35)
Adding UIP-compatible univalence? (15 messages, latest: Feb 10 2025 at 02:30)
Why can't we reason about general recursion? (24 messages, latest: Jan 31 2025 at 10:38)
univalence and coercions (6 messages, latest: Jan 07 2025 at 16:41)
Is Lean's type theory intensional? (8 messages, latest: Jan 04 2025 at 09:55)
Debugging universe levels for minimal brecOn metatheory (2 messages, latest: Jan 01 2025 at 07:07)
Setless proof of Fin2 1 -> Fin2 1 \neq Fin2 2 -> Fin2 2 (22 messages, latest: Dec 16 2024 at 07:54)
HEq congr and inconsistency (18 messages, latest: Dec 12 2024 at 09:34)
Quot and subject reduction property (58 messages, latest: Dec 12 2024 at 09:04)
Set theory - type theory research? (17 messages, latest: Nov 22 2024 at 15:31)
Subsingleton elimination on non-props without choice (3 messages, latest: Nov 21 2024 at 21:40)
Commuting lift and dependent sums (8 messages, latest: Nov 07 2024 at 08:19)
dependent types and parametric polymorphism in lean (8 messages, latest: Oct 11 2024 at 06:50)
Emulating ML modules (23 messages, latest: Oct 02 2024 at 13:06)
Rigorous statement for Sys F cannot express ∀ w/ predicates (1 message, latest: Sep 07 2024 at 23:37)
Justifying Lean's axioms with cubical type theory (13 messages, latest: Aug 19 2024 at 12:54)
axioms and rules of inference (7 messages, latest: Jul 31 2024 at 03:38)
Hitchhikers Guide to Logical Verification: Exercises (4 messages, latest: Jul 29 2024 at 18:21)
Is the hierarchy fixed? (29 messages, latest: Jul 02 2024 at 08:13)
Cardinality of types (14 messages, latest: Feb 23 2024 at 22:41)
Logics and lambda calculi (21 messages, latest: Feb 20 2024 at 18:02)
Theory of Lean with n universes (155 messages, latest: Feb 20 2024 at 01:20)
Cardinality of universes (3 messages, latest: Feb 06 2024 at 20:39)
And.rec (35 messages, latest: Jan 23 2024 at 15:33)
✔ Terms of terms and the universe hierarchy (13 messages, latest: Jan 18 2024 at 19:09)
Are these “type erasure” axioms consistent? (5 messages, latest: Dec 17 2023 at 10:13)
✔ Intro constructor (6 messages, latest: Dec 12 2023 at 16:44)
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: Feb 28 2026 at 14:05 UTC