Inductive-inductive definitions
The principle of inductive-inductive definitions is a principle for defining data types in Martin-Lof Type Theory. It allows the definition of a set A, simultaneously defined w ith a family B : A → Set indexed over A. Such forms of definitions have been used by several authors in order to for exampl...
| Main Author: | |
|---|---|
| Published: |
Swansea University
2013
|
| Online Access: | https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.752308 |