Timeline for What's the effect of imposing the following restriction on inductive type families?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 17, 2016 at 10:13 | comment | added | Andrej Bauer |
No, you need both $\prod$-types and inductive typed (data) to get identity types.
|
|
| Jun 17, 2016 at 1:44 | vote | accept | isekaijin | ||
| Jun 16, 2016 at 16:59 | comment | added | isekaijin | So, basically, if you have $\Pi$-types, identity types are “already there”, and it doesn't make sense to constrain how identity types can be used without constraining how $\Pi$-types can be used? | |
| Jun 16, 2016 at 10:15 | review | First posts | |||
| Jun 17, 2016 at 4:47 | |||||
| Jun 16, 2016 at 10:14 | history | answered | Jesper | CC BY-SA 3.0 |