Cardinality of types

Stream: Type theory

[Shreyas Srinivas]

I have some basic questions about the cardinality of types. I have come across a claim from Kevin many times on zulip that one can only prove inequality of types if they have different cardinality and also that you can't prove \N \neq \Z. Firstly how is the concept of cardinality defined for types? Are types considered to have the same cardinality if they one can show some bijection between them? If so then wouldn't a proof that there is no surjective map from \N to \Z prove that the two types are not equal since they don't have a bijection?

[Damiano Testa]

There is a surjection from ℕ to ℤ: the even numbers map to their half, the odd ones to the negative of one half their predecessor.

[Shreyas Srinivas]

Oh right

[Shreyas Srinivas]

How silly of me. Both are countable sets

[Damiano Testa]

But yes, a proof of a bijection between two types is probably equivalent to the undecidability of the equality of the two types.

[Shreyas Srinivas]

I have a hunch that cardinality would be defined w.r.t some set theoretic model. Because in some models Z could very well be considered equal to N and in others, not so.

[Shreyas Srinivas]

(deleted)

[Kevin Buzzard]

Damiano Testa said:

But yes, a proof of a bijection between two types is probably equivalent to the undecidability of the equality of the two types.

It's not equivalent because sometimes they are equal (eg a type bijects with itself)

[Damiano Testa]

Kevin Buzzard said:

Damiano Testa said:

But yes, a proof of a bijection between two types is probably equivalent to the undecidability of the equality of the two types.

It's not equivalent because sometimes they are equal (eg a type bijects with itself)

:face_palm: indeed.

[Damiano Testa]

Mario explained this (the undecidability part) to me here.

[Eric Wieser]

Are you aware of docs#Cardinal in mathlib?

[Eric Wieser]

Are types considered to have the same cardinality if they one can show some bijection between them?

Because this is true by definition for Cardinal.mk

[Shreyas Srinivas]

Kevin Buzzard said:

Damiano Testa said:

But yes, a proof of a bijection between two types is probably equivalent to the undecidability of the equality of the two types.

It's not equivalent because sometimes they are equal (eg a type bijects with itself)

I understood Damiano's statement to mean that extensional equality of two types given as inputs is undecidable, as opposed to definitional equality, which a lot of type theories seem to want to keep decidable.

[Shreyas Srinivas]

Incidentally @Kevin Buzzard , since you mentioned Rustbelt a few weeks ago, that's at the heart of the rustbelt approach. Instead of dealing with types as syntactic constructs, they model types as ....(sweeping some stuff under the carpet)... basically sets and/or logically defined relations. This means they lose decidability and have to manually prove a bunch of things that a typechecker would otherwise do automatically. But it helps recover the ability to reason about safely accessing "unsafe" data constructs. Iris abstracts over this.