@@ -33,6 +33,14 @@ namespace Builtins
3333 ||| @b the right element of the pair
3434 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
3535
36+ UPair : (A : AnyType) -> (B : AnyType) -> AnyType
37+ UPair a b = UniquePair a b
38+ %deprecate UPair "This name is being deprecated in favour of `UniquePair`"
39+
40+ MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
41+ MkUPair a b = MkUniquePair a b
42+ %deprecate MkUPair "This name is being deprecated in favour of `MkUniquePair`"
43+
3644 ||| Dependent pairs aid in the construction of dependent types by
3745 ||| providing evidence that some value resides in the type.
3846 |||