Is an inductive type fully specified by its`.rec`?

Stream: general

[nrs]

Am trying to get better at thinking about the difference between parameters and indexes, so I've been toying around with .rec. Is an inductive type fully specified by its .rec? i.e., do we have, if an inductive type is identical to another, they will have identical and interchangeable .rec functions?

[Henrik Böving]

 if an inductive type is identical to another, they will have identical and interchangeable .rec functions?

yes, but I don't see how that relates to your "fully specified by its rec" question. If you have a procedure for deriving recursors f and you give that procedure x and y with x = y then of course f x = f y.

[nrs]

Henrik Böving said:

 if an inductive type is identical to another, they will have identical and interchangeable .rec functions?

yes, but I don't see how that relates to your "fully specified by its rec" question. If you have a procedure for deriving recursors f and you give that procedure x and y with x = y then of course f x = f y.

hm you're right that we need both directions. I meant, do we have:

1. If an inductive type is identical to another, we have identical and interchangeable .rec functions, and
2. If two inductive types have identical and interchangeable .rec functions, they are identical

[Floris van Doorn]

Warning: if you define two inductive types that are the same apart from their name and the name of the constructors, you cannot prove in Lean that they are equal as types. They will be equivalent as types.

[nrs]

Floris van Doorn said:

Warning: if you define two inductive types that are the same apart from their name and the name of the constructors, you cannot prove in Lean that they are equal as types. They will be equivalent as types.

is this what is referred to as propositional vs. judgmental (= definitional) equality? they will be propositionally but not definitionally = judgmentally equal?

[Floris van Doorn]

nope, it's independent of Lean whether they are propositionally equal.

inductive Empty1 : Type
inductive Empty2 : Type

example : Empty1 = Empty2 := sorry -- independent of Lean

[Sébastien Gouëzel]

No, they won't even be propositionally equal. Everything depends on what you mean by "equal", but in Lean it has a precise definition and under your definition your types won't be equal (in the sense that you can't construct a proof of equality).

[Floris van Doorn]

With equivalence I mean a bijection, i.e. docs#Equiv

[nrs]

I see, thank you for answers!!