¿Qué es la inducción-inducción?

¿Qué es la inducción-inducción ?

Los recursos que encontré son:

• el libro de HoTT , al final del capítulo 5.7.
• Artículo de nLab
• un artículo llamado definiciones inductivas-inductivas
• esta publicación de blog también menciona tipos inductivos-inductivos

Las dos primeras referencias son demasiado breves para mí, y las dos últimas son demasiado técnicas. ¿Alguien puede explicarlo en términos simples? Sería mejor si hay código Agda.

Suplemento 2016-10-03: Mezclé inducción-inducción e inducción-recursión (¡no la primera vez que hice eso!). Mis disculpas por el desastre. Actualicé la respuesta para cubrir ambos.

Encuentro las explicaciones en el artículo de Forsberg & Setzer Una axiomatización finita de definiciones inductivo-inductivas esclarecedoras.

Inducción-recursión

Una definición inductiva-recursiva es aquella en la que definimos un tipo $A$ y una familia de tipos $B : A \to \mathsf{Type}$ simultáneamente de una manera especial:

1. $A$ se define como un tipo inductivo.
2. $B$ se define por la recursividad en$A$ .
3. Fundamentalmente, la definición de $A$ puede utilizar $B$ .

Sin el tercer requisito, primero podríamos definir $A$ y luego $B$ separado .

Aquí hay un ejemplo de bebé. Defina $A$ inductivamente para tener los siguientes constructores:

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

El tipo de familia $B$ se define por

• $B(a) = \mathtt{bool}$
• $B(\ell(x, f)) = \mathtt{nat}$

$A$

Inducción-inducción

$A$$B : A \to \mathsf{Type}$

1. $A$
2. $B$$A$
3. $A$$B$

$B$

$A$

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

$B$

• $\mathsf{Tru} : B(a)$
• $\mathsf{Fal} : B(a)$
• $x : A$$y : B(x)$$\mathsf{Zer} : B(\ell(x,y))$
• $x : A$$y : B(x)$$z : B(\ell(x,y))$$\mathsf{Suc}(z) : B(\ell(x,y))$

$B$$B(a)$$B(\ell(x,y))$