An exact proof term for the current goal is (λx : set ⇒ UPairI1 x x).