Tuple represented as a single, not product, Type

Stream: new members

[Luis Enrique Muñoz Martín]

Hi, I would expect a tuple (i.e (Nat, Int)) to be a Type. Of course, it's a Type x Type, but should also not be able to be represented as a single Type?

In other words, is there any way to express the following as a single Type?

abbrev Foo : Type := (Nat, Int)  -- error expecting Type x Type

[Yaël Dillies]

abbrev Foo : Type := Nat × Int

is what you mean probably

[Luis Enrique Muñoz Martín]

Ouch! You're right! I'm creating a value :man_facepalming: Thanks!

[Yaël Dillies]

Doesn't help that Haskell conflates both notations!

[Edward van de Meent]

i'm curious, is there a reason why this cannot be equality?

[Edward van de Meent]

does it lead to a contradiction in the type theory?

[Edward van de Meent]

i suppose you'd have to have Type = Type x Type

[Eric Wieser]

Edward van de Meent said:

i'm curious, is there a reason why this cannot be equality?

You could achieve this with overloaded notation, but I think largely people don't want that notation anyway

[Kyle Miller]

You can also achieve it with a coercion:

instance : CoeSort (Type × Type) Type := ⟨fun p => p.1 × p.2⟩

abbrev Foo : Type := (Nat, Int)

[Kyle Miller]

@Edward van de Meent If that were an equality, then not only would every pair of types give a type (the product type), but every type would be a product of types. I think there's nothing wrong with that as an axiom it, but it's probably not what you'd want (why should Nat be a product of types?)

The coercion implements a one-directional Type x Type -> Type.

[Kevin Buzzard]

I should think that in the cardinality model of Lean, you could have Type = Type x Type. I've seen a model of ordered pairs in set theory where every set is an ordered pair :-)