11.13. Tuples🔗

Planned Content

Describe Prod and PProd, their syntax and API

Tracked at issue #171

structure

Prod.{u, v} (α : Type u) (β : Type v)
    : Type (max u v)

Product type (aka pair). You can use α × β as notation for Prod α β. Given a : α and b : β, Prod.mk a b : Prod α β. You can use (a, b) as notation for Prod.mk a b. Moreover, (a, b, c) is notation for Prod.mk a (Prod.mk b c). Given p : Prod α β, p.1 : α and p.2 : β. They are short for Prod.fst p and Prod.snd p respectively. You can also write p.fst and p.snd. For more information: Constructors with Arguments

Constructor

Prod.mk.{u, v}

Constructs a pair from two terms.

Fields

`fst`	`:`	`α`
		The first projection out of a pair. if `p : α × β` then `p.1 : α`.
`snd`	`:`	`β`
		The second projection out of a pair. if `p : α × β` then `p.2 : β`.

structure

PProd.{u, v} (α : Sort u) (β : Sort v)
    : Sort (max (max 1 u) v)

Similar to Prod, but α and β can be propositions. You can use α ×' β as notation for PProd α β. We use this type internally to automatically generate the brecOn recursor.

Constructor

PProd.mk.{u, v}

Fields

`fst`	`:`	`α`
		The first projection out of a pair. if `p : PProd α β` then `p.1 : α`.
`snd`	`:`	`β`
		The second projection out of a pair. if `p : PProd α β` then `p.2 : β`.

structure

MProd.{u} (α β : Type u) : Type u

Similar to Prod, but α and β are in the same universe. We say MProd is the universe monomorphic product type.

Constructor

MProd.mk.{u}

Fields

`fst`	`:`	`α`
		The first projection out of a pair. if `p : MProd α β` then `p.1 : α`.
`snd`	`:`	`β`
		The second projection out of a pair. if `p : MProd α β` then `p.2 : β`.