@@ -23,11 +23,11 @@ namespace Builtins
23 ||| UniqueTypes.
23 ||| UniqueTypes.
24 ||| @A the type of the left elements in the pair
24 ||| @A the type of the left elements in the pair
25 ||| @B the type of the left elements in the pair
25 ||| @B the type of the left elements in the pair
26− data UPair : (A : Type*) -> (B : Type*) -> Type where
26+ data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
27 ||| A pair of elements
27 ||| A pair of elements
28 ||| @a the left element of the pair
28 ||| @a the left element of the pair
29 ||| @b the right element of the pair
29 ||| @b the right element of the pair
30− MkUPair : {A, B : Type*} -> (a : A) -> (b : B) -> UPair A B
30+ MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
32 ||| Dependent pairs
32 ||| Dependent pairs