# Which inductive schemes can encode the following Agda definition?

Which induction schemes (e.g. induction-recursion by Dybjer and Setzer, "Irish" induction-recursion by McBride or induction-induction by Forsberg and Setzer or perhaps some simpler ones) allow one to encode the following Agda definition

  data A : Set where
a : Maybe (List A) → A


I can think of some tricks to reformulate List in this definition so that induction-recursion becomes applicable, but are there any schemes that would allow me to first say what a list is and then refer to this information to say what A is the way it's done in Agda?

Edit: As follows from András Kovács's answer, this particular definition can be reformulated as an inductive family. Here is how to do it:

data Three : Set where one two three : Three

data AG : Three → Set where
a'       : AG three → AG one
nil'     : AG two
cons'    : AG one → AG two → AG two
nothing' : AG three
just'    : AG two → AG three

A = AG one
ListA = AG two
MaybeListA = AG three

a : MaybeListA → A
a = a'

nil : ListA
nil = nil'

cons : A → ListA → ListA
cons = cons'

nothing : MaybeListA
nothing = nothing'

just : ListA → MaybeListA
just = just'


No scheme that I know of directly encodes that type. Sometimes it's called a "nested" inductive definition. The complication here is that Maybe and List are type constructors which are external to the signature, and we have to formalize strict positivity for external type operators in general, if we want to allow such definitions.

In other words, the consistency of A depends on the definition on Maybe and List. Some external type operators are not positive, as in:

data Neg (A : Set) : Set where
neg : (A -> Bool) -> Neg A

data B : Set where
b : Neg B -> B


Agda does look into all the external definitions and tries to determine the variance of type parameters. While I don't know a reference for a direct formal specification of this, an easy way to reformulate nested definitions as non-nested is to include the external type operators into a mutual inductive signature. For example:

data A : Set
data ListA : Set
data MaybeListA : Set

data A where
a : MaybeListA -> A

data ListA where
nil : ListA
cons : A -> ListA -> ListA

data MaybeListA where
nothing : MaybeListA
just : ListA -> MaybeListA


This is an ordinary mutual inductive type, which is covered (modulo cosmetic details) by Dybjer's inductive families.

• Thanks. I assume, the conversion to inductive families is done by introducing a parameter of a three-valued type, "labelling" constructors with corresponding values of that type and then constructing A one instead of A, corrent? Feb 17 '20 at 13:48
• @PrimaryKey that's correct. Feb 17 '20 at 14:03