Induction as a special case of recursion ?

[louis...@free.fr]

The recursion principle of a type T is a special case of the induction principle, when the codomain is a simple type C:U instead of a type family C: T->U. It seems to me that, conversely, the induction principle is also a special case of the recursion principle, by applying it on the dependent pair type Sigma(x:T)C:U

Let's try to verify it on N:
Suppose we have C:Pi(x:N)U that satisfies the conditions of the induction principle:  c_0:C(0);   and c_s:Pi(x:N)Pi(y:C(x))C(succ(x))
We can verify that the type Sigma(x:N)C, which is not a type family any more, satisfies the conditions to apply the recursion principle.
We have indeed (0,c_0):Sigma(x:N)C, and we can define sig_s:Sigma(x:N)C -> Sigma(x:N)C such that sig_s((x,C(x))) := (succ(x),C(succ(x)))
Indeed, we have sig_s(z) := ( succ(pr1(z)) , c_s(pr1(z))(pr2(z)) )

By applying the recursion principle on Sigma(x:N)C, we get rec_N(Sigma(x:N)C, c_0, z.sig_s, n) : Sigma(x:N)C
such that rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, 0) := (0,c0) and rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, succ(n)) := sig_s(rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, n)))

The induction principle should then be the 2nd projection of recursion principle applied to Sigma(x:N)C.
It seems that the same construction can be done for all inductive types, except Pi types, including the identity types and HITs.

Is that correct ? If not, where is the fault ?

Louis.

[Gaëtan Gilbert]

> By applying the recursion principle on Sigma(x:N)C, we get
> rec_N(Sigma(x:N)C, c_0, z.sig_s, n) : Sigma(x:N)C

This is not the type of the induction principle, you want Pi(x:N)C(x)

In other words without using the induction principle you lack a proof
that proj1(rec_N(Sigma(x:N)C, c_0, sig_s, n)) = n

Gaëtan Gilbert

> --
> You received this message because you are subscribed to the Google
> Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to hott-cafe+...@googlegroups.com
> <mailto:hott-cafe+...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.

[Tom Jack]

However, if the eta rule for the recursor held judgmentally, then this equation would also hold judgmentally -- the function \n. proj1(rec_N(Sigma(x:N)C, c_0, sig_s, n)) satisfies the same recurrence as the identity -- and you could indeed derive induction from recursion.

I learned this from Harper's HoTT lectures.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+unsubscribe@googlegroups.com <mailto:hott-cafe+unsubscribe@googlegroups.com>.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+unsubscribe@googlegroups.com.

[louis...@free.fr]

I was not able to find what "the eta rule for the recursor" is: how does it look like here ?

I think that forall n:N, proj1(rec_N(Sigma(x:N)C, c_0, sig_s, n)) = n   can be proved by recursion again :

Let's note:
      REC(n) := rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, n)

We have by recursion on Sigma(x:N)C:
                     forall n:N,  REC(n) : Sigma(x:N)C

with REC(succ(n)) == sig_s(REC(n))             (by definition of the recursor)
                           == (succ(p1(REC(n))), _ )  (by definition of sig_s)
and therefore:
(A)             p1(REC(succ(n))) == succ(p1(REC(n)))

We can use it to prove by recursion that:
              forall n:N, p1(REC(n)) = n     (propositionally)
* for n=0: we have REC(0) == (0,c_0) and therefore p1(REC(0)) == 0
* supposing p1(REC(n)) = n, we have by (A):
             p1(REC(succ(n))) == succ(p1(REC(n))) = succ(n)

Isn't it enough to derive induction from recursion ?

Le mercredi 1 novembre 2017 23:18:35 UTC+1, Tom Jack a écrit :

However, if the eta rule for the recursor held judgmentally, then this equation would also hold judgmentally -- the function \n. proj1(rec_N(Sigma(x:N)C, c_0, sig_s, n)) satisfies the same recurrence as the identity -- and you could indeed derive induction from recursion.

I learned this from Harper's HoTT lectures.

On Nov 1, 2017 2:59 PM, "Gaëtan Gilbert" <gaetan....@skyskimmer.net> wrote:

> By applying the recursion principle on Sigma(x:N)C, we get
> rec_N(Sigma(x:N)C, c_0, z.sig_s, n) : Sigma(x:N)C

This is not the type of the induction principle, you want Pi(x:N)C(x)

In other words without using the induction principle you lack a proof that proj1(rec_N(Sigma(x:N)C, c_0, sig_s, n)) = n

Gaëtan Gilbert

On 01/11/2017 22:52, louis...@free.fr wrote:

The recursion principle of a type T is a special case of the induction principle, when the codomain is a simple type C:U instead of a type family C: T->U. It seems to me that, conversely, the induction principle is also a special case of the recursion principle, by applying it on the dependent pair type Sigma(x:T)C:U

Let's try to verify it on N:
Suppose we have C:Pi(x:N)U that satisfies the conditions of the induction principle:  c_0:C(0);   and c_s:Pi(x:N)Pi(y:C(x))C(succ(x))
We can verify that the type Sigma(x:N)C, which is not a type family any more, satisfies the conditions to apply the recursion principle.
We have indeed (0,c_0):Sigma(x:N)C, and we can define sig_s:Sigma(x:N)C -> Sigma(x:N)C such that sig_s((x,C(x))) := (succ(x),C(succ(x)))
Indeed, we have sig_s(z) := ( succ(pr1(z)) , c_s(pr1(z))(pr2(z)) )

By applying the recursion principle on Sigma(x:N)C, we get rec_N(Sigma(x:N)C, c_0, z.sig_s, n) : Sigma(x:N)C
such that rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, 0) := (0,c0) and rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, succ(n)) := sig_s(rec_N(Sigma(x:N)C, (0,c_0), z.sig_s, n)))

The induction principle should then be the 2nd projection of recursion principle applied to Sigma(x:N)C.
It seems that the same construction can be done for all inductive types, except Pi types, including the identity types and HITs.

Is that correct ? If not, where is the fault ?

Louis.

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com <mailto:hott-cafe+...@googlegroups.com>.

For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.

[Tom Jack]

> We can use it to prove by recursion that:
>               forall n:N, p1(REC(n)) = n

In this step, you use _induction_ on N, begging the question.

The 'eta' for nat recursion I referred to, the uniqueness principle, looks like this, propositionally and in Agda syntax:

    eta : ∀ {C} (c0 : C) (cs : N → C → C)

      → (f : N → C) → f zero ≡ c0 → (∀ n → f (succ n) ≡ cs n (f n))

      → (n : N) → f n ≡ rec c0 cs n

If we somehow had it, we could use it to get p1(REC(n)) = n without any N-induction.

To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+unsubscribe@googlegroups.com.