Zulip Chat Archive

Stream: general

Topic: mutual inductives


view this post on Zulip Chris Hughes (Nov 03 2018 at 23:23):

What's the "canonical" proof that the Types A and B are empty. I proved it by reference to the auxiliary A._mut_. Is there a nicer way?

mutual inductive A, B
with A : Type
| mk : B  A
with B : Type
| mk : A  B

view this post on Zulip Kenny Lau (Nov 03 2018 at 23:28):

mutual inductive A, B
with A : Type
| mk : B  A
with B : Type
| mk : A  B

def A.to_sort (l : Sort*) : A  l
| (A.mk (B.mk x)) := A.to_sort x

view this post on Zulip Chris Hughes (Nov 03 2018 at 23:28):

Of course.

view this post on Zulip Chris Hughes (Nov 03 2018 at 23:35):

Are there any recursors that look a bit like this?

def AB.reca : Π {Ca : A  Sort*} {Cb : B  Sort*}
  (ha : Π a : A, Ca a  Cb (B.mk a))
  (hb : Π b : B, Cb b  Ca (A.mk b))
  (a : A), Ca a

view this post on Zulip Kenny Lau (Nov 03 2018 at 23:37):

you can write one


Last updated: May 13 2021 at 06:15 UTC