[Agda] Induction-induction in a tricky order

[Fredrik Nordvall Forsberg]

Hi Simon,

On 15/03/16 14:06, Simon Boulier wrote:
> Is it a way to type check the following:
> 
>     data Foo  : Set
>     data Bar  : Foo → Set
>     data Bar2 : Foo → Set
> 
> [...]
>       bar'  : (x : Foo) → Bar (foo x (bar x) (bar2 x))
> [...]
>       bar2  : (x : Foo) → Bar2 x

So to summarise, you want a constructor for Bar which has a constructor
for Bar2 in its index. In this particular case, since Bar and Bar2 are
not dependent on each other, you can introduce them simultaneously by
indexing them over a two-element type, and then interleave the
constructors as you wanted to do. By defining syntactic sugar for Bar
and Bar2 early using new-style mutual blocks, we can make the definition
look quite natural:

-------------------------------------------------

open import Data.Bool

data Foo  : Set
data Bar-and-Bar2 : Foo → Bool → Set

Bar : Foo → Set
Bar x = Bar-and-Bar2 x true

Bar2 : Foo → Set
Bar2 x = Bar-and-Bar2 x false

data Foo where
  foo   : (x : Foo) → Bar x → Bar2 x → Foo

data Bar-and-Bar2 where
  bar   : (x : Foo) → Bar x
  bar2  : (x : Foo) → Bar2 x
  bar'  : (x : Foo) → Bar (foo x (bar x) (bar2 x))
  bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))

-------------------------------------------------

If you want also Bar2 to be indexed over Bar, i.e.

  data Foo  : Set
  data Bar  : Foo → Set
  data Bar2 : (x : Foo) → Bar x → Set

this encoding does not work any more (without Hickey's Very Dependent
Types). However Agda lets us work around this by simultaneously defining
an auxiliary copy of the constructor in question (I learnt about this
trick from Ulf Norell on this mailing list):

  data Foo  : Set
  data Bar  : Foo → Set
  data Bar2 : (x : Foo) → Bar x → Set
  bar2aux : (x : Foo) → (y : Bar x) → Bar2 x y

This way earlier constructors know about the existence of bar2aux, and
after the real bar2 has been introduced, we can simply define
bar2aux = bar2. Note that this is *not* an instance of
(induction-)induction-recursion, but something weirder, because the
(trivially) recursively defined function bar2aux does not have as
codomain some already defined type D.

Here is your example again in this setting:

-------------------------------------------------

data Foo  : Set
data Bar  : Foo → Set
data Bar2 : (x : Foo) → Bar x → Set
bar2aux : (x : Foo) → (y : Bar x) → Bar2 x y

data Foo where
  foo   : (x : Foo) → (y : Bar x) → Bar2 x y → Foo

data Bar where
  bar   : (x : Foo) → Bar x
  bar'  : (x : Foo) → Bar (foo x (bar x) (bar2aux x (bar x)))

data Bar2 where
  bar2  : (x : Foo) → (y : Bar x) → Bar2 x y
  bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2aux x (bar x))) (bar' x)

bar2aux = bar2

bar'-has-right-type-because-this-is-accepted
  : (x : Foo) → Bar (foo x (bar x) (bar2 x (bar x)))
bar'-has-right-type-because-this-is-accepted = bar'

also-bar2'-has-right-type
  : (x : Foo) → Bar2 (foo x (bar x) (bar2 x (bar x))) (bar' x)
also-bar2'-has-right-type = bar2'

-------------------------------------------------

Semantically, it seems like it is possible to understand the meaning of
definitions like this (without the bar2aux encoding) in the same way
that we give semantics to the mutual dependencies of higher inductive types.

Hope that helps, and cheers,
Fredrik

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.