Stream: general

Topic: mutual inductives

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


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


Of course.

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


Kenny Lau (Nov 03 2018 at 23:37):

you can write one

Last updated: May 13 2021 at 06:15 UTC