1
$\begingroup$

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)))))
$\endgroup$

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ You're right. I've implemented your solution and added it to the question as an update. Out of curiosity, can you point me towards the definition of "large elimination" and towards an "on paper" presentation of type theory? $\endgroup$
    – CrabMan
    Sep 15 at 0:46
  • 1
    $\begingroup$ @CrabMan Large elimination is simply elimination into $\mathcal U$. You can look up Martin--Lof type theory or the lambda cube for rigorous presentations of type theories. $\endgroup$
    – Trebor
    Sep 16 at 11:32
  • $\begingroup$ Martin-löf type theory is what I was thinking of in particular. Here is one of his presentations of it. It's not totally obvious that it works the way I said, because the 'is set' judgments on the eliminators are implied by the other premises. The lambda cube is probably not the best example, because 1) it doesn't have (axiomatized) inductive types and 2) it's actually more organized around sorts/universes the way Pie/Agda/etc. are. $\endgroup$
    – Dan Doel
    Sep 16 at 15:54
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.