Timeline for What are the differences between MLTT and CIC?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 10, 2022 at 21:16 | comment | added | user833970 | I'm not sure "Introduction to the Calculus of Inductive Constructions" is a good citation for CIC, since that document does not formalize the system. | |
| Feb 16, 2022 at 11:16 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 34 characters in body
|
| Feb 14, 2022 at 22:20 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 209 characters in body
|
| Feb 14, 2022 at 22:14 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 209 characters in body
|
| Feb 10, 2022 at 21:01 | comment | added | Loïc Pujet | Let us continue this discussion in chat. | |
| Feb 10, 2022 at 20:38 | comment | added | Namdak Tönpa | Sure! I see you love discussing :-) | |
| Feb 10, 2022 at 17:52 | comment | added | Loïc Pujet | Anyway, if you plan on continuing this discussion further, I suggest moving to some other place, for instance the chatroom. | |
| Feb 10, 2022 at 17:51 | comment | added | Loïc Pujet | Isn't this precisely the point of the paper by Jasper Hugunin that you cited? I quote from the abstract: "In this paper, we show how to refine the standard construction of inductive types such that the induction principle is provable and computes as expected in intensional type theory without using function extensionality." | |
| Feb 10, 2022 at 17:41 | comment | added | Namdak Tönpa | Evryone says this is easy to construct induction of Nat in MLTT having W, 0, 1, 2. If you say so show me your code! (I have mine to compare). This reminds me more like PTS programming not like MLTT programming. In HoTT also you will need transport. | |
| Feb 10, 2022 at 17:36 | comment | added | Namdak Tönpa | I can add literature if you want: 1) Fredrik Nordvall Forsberg and Anton Setzer. A finite axiomatisation of inductive-inductive definitions; 2) Jasper Hugunin. Why not W? 3) Steve Awodey, Nicola Gambino, Kristina Sojakova. Inductive Types in Homotopy Type Theory. | |
| Feb 10, 2022 at 17:34 | comment | added | Namdak Tönpa | You shouldn't equate them. W-types from MLTT are different thing that W-types in this paper. These are special kind of W-types addressed exactly described problem with mutual recursivity. They are neither W-types nor part of MLTT. | |
| Feb 10, 2022 at 17:31 | comment | added | Loïc Pujet | The paper "A Syntax for Mutual Inductive Families" by Kaposi and Raumer explains the folklore fact that mutual inductive definitions can be encoded with indexed W types. Some reduction rules are not preserved by the encoding, but since they are propositionally derivable, this does not change the logical expressivity. | |
| Feb 10, 2022 at 17:25 | comment | added | Namdak Tönpa | As I said you can add $\mathcal{Prop}$ to MLTT but won't have tremendous amount of computational and logical power to express even mutual recursive even-odd. | |
| Feb 10, 2022 at 17:19 | comment | added | Namdak Tönpa | You can't express mutual recursive types neither in MLTT-80 nor in MLTT-73. Also you will have all induction rules for free (definitional $\beta$) in inductive schemes. | |
| Feb 10, 2022 at 17:17 | comment | added | Loïc Pujet | IIUC, the general inductive scheme is not responsible for the increased logical power of CIC (as general inductive types can pretty much be encoded with Sigma, Nat, and Id). However Prop, along with its singleton elimination rule, does add a tremendous amount of computational and logical power. | |
| Feb 10, 2022 at 14:25 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 124 characters in body
|
| Feb 10, 2022 at 14:16 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 1 character in body
|
| Feb 10, 2022 at 13:23 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
[Edit removed during grace period]; added 77 characters in body
|
| Feb 10, 2022 at 13:18 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
[Edit removed during grace period]; added 77 characters in body
|
| Feb 10, 2022 at 13:09 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 15 characters in body
|
| Feb 10, 2022 at 13:03 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 118 characters in body
|
| Feb 10, 2022 at 12:54 | history | edited | Namdak Tönpa | CC BY-SA 4.0 |
added 2 characters in body
|
| Feb 10, 2022 at 12:48 | history | answered | Namdak Tönpa | CC BY-SA 4.0 |