# Zulip Chat Archive

## Stream: new members

### Topic: Uniqueness of inductive types

#### Patrick Johnson (Nov 15 2021 at 15:04):

Given two definitions of inductive types, can we prove that the types are distinct? For example:

```
inductive A : Type
| mk1 : A
inductive B : Type
| mk1 : B
| mk2 : B
```

Can we always prove something like `lemma a_ne_b : A ≠ B`

? In this particular case it can be proved using heterogeneous equality, because they have different cardinalities. But is it possible in general?

#### Reid Barton (Nov 15 2021 at 15:07):

You can only prove it if they have different cardinalities

#### Kyle Miller (Nov 15 2021 at 16:22):

The mental model I have is that Lean is only promising that it's able to implement the type for you in some way. Since everything is typechecked, elements don't need to know what type they're from, so in principle it could reuse representations between different types.

For example, it wouldn't be wrong for Lean to take

```
inductive my_list (α : Type*)
| nil : my_list
| cons : α → my_list → my_list
```

and compile it like this:

```
def my_list (α : Type*) := list α
def my_list.nil {α : Type*} : my_list α := list.nil
def my_list.cons {α : Type*} (x : α) (xs : my_list α) : my_list α := list.cons x xs
def my_list.rec ...
...
```

Lean only lets you prove things that are independent of how it might be implementing things behind the scenes, which is why `list α = my_list α`

is neither provable nor disprovable.

#### Kyle Miller (Nov 15 2021 at 16:28):

Also, it turns out that even if the arguments to a type constructor are different, the resulting types might be the same. In fact, there must be cases where this happens by a diagonalization argument: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/disjointness.20of.20inductive.20type.20constructors.2C.20heq/near/204877510

#### Stuart Presnell (Nov 15 2021 at 16:54):

Could we prove a weaker relation between `list`

and `my_list`

in this case? Is there a suitable notion of isomorphism or equivalence?

#### Kyle Miller (Nov 15 2021 at 17:06):

You could create an docs#equiv and show it carries `my_list.nil`

to `list.nil`

and `my_list.cons`

to `list.cons`

(i.e., show it's an isomorphism)

#### Stuart Presnell (Nov 15 2021 at 17:09):

Ok. And since we don't have univalence we couldn't derive from this isomorphism that they're equal. :)

#### Kyle Miller (Nov 15 2021 at 17:12):

Just to be completely explicit:

```
import tactic
inductive my_list (α : Type*)
| nil : my_list
| cons : α → my_list → my_list
variables {α : Type*}
def my_list.to_list : my_list α → list α
| my_list.nil := list.nil
| (my_list.cons x xs) := list.cons x xs.to_list
def list.to_my_list : list α → my_list α
| list.nil := my_list.nil
| (list.cons x xs) := my_list.cons x xs.to_my_list
def my_list_equiv : my_list α ≃ list α :=
{ to_fun := my_list.to_list,
inv_fun := list.to_my_list,
left_inv :=
begin
intro l,
induction l with x xs ih,
{ refl },
{ simp! [ih], },
end,
right_inv :=
begin
intro l,
induction l with x xs ih,
{ refl },
{ simp! [ih], },
end }
lemma my_list_equiv.nil : my_list_equiv (my_list.nil : my_list α) = list.nil := rfl
lemma my_list_equiv.cons (x : α) (xs : my_list α) :
my_list_equiv (my_list.cons x xs) = list.cons x (my_list_equiv xs) := rfl
-- Forgetting the definition of `my_list_equiv`, similar lemmas for `my_list_equiv.symm` follow.
```

Last updated: Dec 20 2023 at 11:08 UTC