Builtins

data UPair : (A : AnyType) -> (B : AnyType) -> AnyType

The non-dependent pair type, also known as conjunction, usable with
UniqueTypes.

A

the type of the left elements in the pair

B

the type of the left elements in the pair

MkUPair : (a : A) -> (b : B) -> UPair A B

A pair of elements

a

the left element of the pair

b

the right element of the pair

data Sigma : (a : Type) -> (P : a -> Type) -> Type

Dependent pairs

Dependent pairs represent existential quantification - they consist of a
witness for the existential claim and a proof that the property holds for
it. Another way to see dependent pairs is as just data - for instance, the
length of a vector paired with that vector.

a

the type of the witness

P

the type of the proof

MkSigma : (x : a) -> (pf : P x) -> Sigma a P

data Pair : (A : Type) -> (B : Type) -> Type

The non-dependent pair type, also known as conjunction.

A

the type of the left elements in the pair

B

the type of the left elements in the pair

MkPair : (a : A) -> (b : B) -> (A, B)

A pair of elements

a

the left element of the pair

b

the right element of the pair