@@ -33,6 +33,14 @@ namespace Builtins
33 ||| @b the right element of the pair
33 ||| @b the right element of the pair
34 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
34 MkUniquePair : {A, B : AnyType} -> (a : A) -> (b : B) -> UniquePair A B
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`"
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`"
36 ||| Dependent pairs aid in the construction of dependent types by
44 ||| Dependent pairs aid in the construction of dependent types by
37 ||| providing evidence that some value resides in the type.
45 ||| providing evidence that some value resides in the type.