The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Agda accepts these types, but only in this declaration order:

mutual

  data B : Set where
    BIntro : forall b (a : A b) -> B

  data A (b : B) : Set where
    AIntro : A b

B has to be defined first to check the type signature of A : B -> Set.

I do not see a reason why this should be a source of inconsistency. 
Types like those are discussed in the work on "inductive-inductive 
definitions" by Anton Setzer, Frederic Forsberg et al.


On 05.10.12 4:42 PM, Arthur Azevedo de Amorim wrote:
> Dear list,
>
> Coq rejects the following definition
>
> Inductive A : B -> Type :=
> | AIntro : forall b, A b
>
> with B : Type :=
> | BIntro : forall b (a : A b), B.
>
> Is there any metatheoretical reason for this? Does anyone have an
> example showing that it would make the logic inconsistent?
>
> Thanks

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/