- 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 right 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

- Sigma : (a : Type) -> (P : a -> Type) -> Type
- 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 right elements in the pair

- MkSigma : (x : a) -> (prf : P x) -> DPair a P
- data DPair : (a : Type) -> (P : a -> Type) -> Type
Dependent pairs aid in the construction of dependent types by

providing evidence that some value resides in the type.Formally, speaking, dependent pairs represent existential

quantification - they consist of a witness for the existential

claim and a proof that the property holds for it.- a
the value to place in the type.

- P
the dependent type that requires the value.

- MkDPair : (x : a) -> (pf : P x) -> DPair a P