Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?

Question

In this question, I am talking about the language Pie described in the book The Little Typer.

One can derive that $0=1$ is contradictory:

(claim 0=1->Absurd (-> (= Nat 0 1) Absurd))
(define 0=1->Absurd
  (λ (0=1) (replace 0=1
             (λ (x) (which-Nat x Trivial (λ (x-1) Absurd)))
             sole)))

When I tried to prove that left being equal to right is contradictory in a similar way, I failed:

(claim l=r->Absurd (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd))
(define l=r->Absurd
  (λ (l=r) (replace l=r
             (λ (x) (ind-Either x
                      (λ (x) U)
                      (λ (triv) Trivial)
                      (λ (triv) Absurd)))
             sole
             )))

The code snippet above fails with an error highlighting U and saying U is a type, but it does not have a type.

Either doesn't have an expression analagous to which-Nat or rec-Nat, it only has ind-Either, and ind-Either requires writing a motive, and a motive can't return U because Pie has only one universe. So, I think which-Nat and rec-Nat are cheats which allow this while Either doesn't have such a cheat and that's why it's impossible to prove (-> (= Nat 0 1) Absurd). Am I right?

---

Update. Dan Doel has explained in his answer that (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) can be proven by first mapping (Either Trivial Trivial) to 0 or 1 and then using congruence with 0=1->Absurd:

(claim EitherTrivialTrivial->Nat (-> (Either Trivial Trivial) Nat))
(define EitherTrivialTrivial->Nat (λ (x) (ind-Either x
                                           (λ (x) Nat)
                                           (λ (triv) 0)
                                           (λ (triv) 1))))

and then I can do either

(define l=r->Absurd (λ (l=r) (0=1->Absurd (cong l=r EitherTrivialTrivial->Nat))))

or

(define l=r->Absurd
  (λ (l=r)
    (0=1->Absurd (replace l=r
                   (λ (x) (= Nat 0 (EitherTrivialTrivial->Nat x)))
                   (same 0)))))

Answer 1

I think your argument is correct about being able to directly show that $\mathsf{left}\ x \neq \mathsf{right}\ y$. Traditionally the 'on paper' presentations of type theory do not require the motive to be in a universe, just be judged a type. Then you do not need a second universe to contain the first universe.

However, I think you can still prove what you want, because you can define a function that maps $\sf left$ to $0$ and $\sf right$ to 1. Then $\mathsf{left}\ x = \mathsf{right}\ y$ implies $0 = 1$ by congruence, and you can use the special cases for natural numbers. It doesn't suffice for everything, but 'large elimination' for just the booleans or naturals still lets you prove some important results.

Answer 2

You can construct a function that translates left to 0 and right to 1, therefore I believe you can still prove your point. By congruence, left x=right y implies that 0=1, and you may apply the special cases for natural numbers as a result. Large elimination for only the booleans or naturals nevertheless allows you to establish some significant findings, even though it isn't sufficient in every case.