Signatures and Induction Principles for Higher Inductive-Inductive Types
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher ind...
Збережено в:
| Автори: | , |
|---|---|
| Формат: | Artigo |
| Мова: | Inglês |
| Опубліковано: |
Logical Methods in Computer Science e.V.
2020-02-01
|
| Серія: | Logical Methods in Computer Science |
| Предмети: | |
| Онлайн доступ: | https://lmcs.episciences.org/5173/pdf |
| Теги: |
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|