Narya
Contents:
Installation
Top level interface
Built-in types
Names and notations
Imports and scoping
Typechecking details
Interactive proof
Record types and tuples
Inductive datatypes and matching
Codatatypes and comatching
Canonical types defined by case trees
Mutual definitions
Observational higher dimensions
Parametricity
Higher datatypes and codatatypes
Higher Observational Type Theory
Displayed type theory
Nominal type theory
Remarks on implementation
Support and community
Contributing to Narya
Narya
Index
Index