<p>You can just use <code>replace</code> with the identity function as the motive to transport along an equality of types.</p>
<p>In Martin-Löf type theory, the standard way to prove that e.g. <span class="math-container">$0 \neq 1$</span> is to define a type family <span class="math-container">$T : \mathbb{N} \to \mathcal{U}$</span> such that <span class="math-container">$T(0) = \top$</span> and <span class="math-container">$T(n + 1) = \bot$</span>, then transport <span class="math-container">$\star : \top$</span> along the equality <span class="math-container">$0 = 1$</span> in <span class="math-container">$T$</span> to get an inhabitant of <span class="math-container">$\bot$</span>. In fact you <em>have</em> to use <span class="math-container">$\mathcal{U}$</span>: see <a href="https://www.cse.chalmers.se/%7Esmith/JSLPeano.pdf" rel="nofollow noreferrer">The Independence of Peano's Fourth Axiom from
Martin-Löf's Type Theory without Universes</a>.</p>
<p>EDIT by Suraaj: The following is a minimal reproducible Pie example:</p>
<pre><code>(claim transport (Pi ((A U) (B U) (eq (= U A B)) (a A)) B))
(define transport 
  (lambda (A B eq a) (replace eq (lambda (x) x) a))
)
</code></pre>

CC BY-SA 4.0
2024-10-07T13:42:22.737Z
Just to be clear - the Peano Axiom in question is "there is no number such that 0 is its sucessor", right?
Suraaj K S
CC BY-SA 4.0
2024-10-07T13:53:32.907Z
Yes, that's the one.
Naïm Favier
CC BY-SA 4.0
2024-10-07T08:59:19.180Z
2024-10-07T15:40:20.153Z
2024-10-07T15:40:20.153Z
Naïm Favier
<p>Usually one proves equality in order to prove another equality or to prove correct typing of something else. If you showed that <span class="math-container">$T_1 \equiv T_2$</span> then you should be able to derive the isomorphism functions   <span class="math-container">$f:T_1\to T_2$</span> and <span class="math-container">$g:T_2\to T_1$</span>. The function <span class="math-container">$f$</span> should be able to get you a typechecking judgment <span class="math-container">$f x : T_2$</span> if you have <span class="math-container">$x : T_1$</span>.</p>
<p>It is another question how to write all this in the syntax of Pie. That I am not sure about.</p>

CC BY-SA 4.0
2024-10-07T09:41:19.193Z
2024-10-07T09:41:19.193Z
winitzki
<p>I was reading &quot;The Little Typer&quot; book, to understand dependent types. I was wondering about the following question.</p>
<p>Suppose you have a proof that <code>T1</code> and <code>T2</code> are equal. That is, you can construct a <code>(the (= U T1 T2) Proof)</code> expression. <strong>How can you use it?</strong>. For example, if you have <code>(the X xexpr)</code> and <code>(the (= U X Y) Proof</code>, can you say <code>(the Y xexpr)</code> in Pie?</p>
<p>I understand that if you prove two non-type expressions of a type equal, then you can use <code>replace</code> to use that fact. I'm not sure how I could do this with types...</p>
<hr />
<p>A little more context. I was playing around with the Pie language, and I did this:</p>
<pre><code>(claim subtract (-&gt; Nat Nat Nat))
(define subtract  
   (lambda (y x) 
     (rec-Nat x ;Target
              y ;When x is zero
              (lambda (x-1 almost_ans) 
                (which-Nat almost_ans 0 (lambda (almost_ans-1) almost_ans-1))
              )
     )
   )
)

(claim eq (-&gt; Nat Nat Nat))
(define eq (lambda (x y)
             (which-Nat (subtract x y) (which-Nat (subtract y x) 1 (lambda (_) 0)) (lambda (_) 0))
           )
)

;'Proposition generator'. If x and y are equal, return Trivial. Otherwise return Absurd
(claim prop_gen (-&gt; Nat Nat U))
(define prop_gen (lambda (x y) 
                        (which-Nat (eq x y) Absurd (lambda (_) Trivial))
))

(claim final_lemma (Pi ((x Nat))  (prop_gen x x) ))
; How do I prove this? I think that it might be possible for me to prove `(= U Trivial (prop_gen x x))` for all x. I was then thinking how I could use that.
</code></pre>
<p>And finally, the reason <strong>why I wanted to do the whole thing above</strong> was to see if I could prove <code>¬ (1 = 2)</code>, in a slightly different way that was done in chapter 15 of the book. I think that if I could define <code>prop_gen</code>, I could use <code>replace</code> to prove the absurdity.</p>

<dependent-type><proofs><program-verification><proof-assistants>
Type Equality in Pie (The Little Typer)
Suraaj K S
# Type Equality in Pie (The Little Typer)

(Asked by: username_0 on 2024-10-07)

I was reading "The Little Typer" book, to understand dependent types. I was wondering about the following question.
Suppose you have a proof that T1 and T2 are equal. That is, you can construct a (the (= U T1 T2) Proof) expression. How can you use it?. For example, if you have (the X xexpr) and (the (= U X Y) Proof, can you say (the Y xexpr) in Pie?
I understand that if you prove two non-type expressions of a type equal, then you can use replace to use that fact. I'm not sure how I could do this with types...

A little more context. I was playing around with the Pie language, and I did this:
(claim subtract (-> Nat Nat Nat))
(define subtract  
   (lambda (y x) 
     (rec-Nat x ;Target
              y ;When x is zero
              (lambda (x-1 almost_ans) 
                (which-Nat almost_ans 0 (lambda (almost_ans-1) almost_ans-1))
              )
     )
   )
)

(claim eq (-> Nat Nat Nat))
(define eq (lambda (x y)
             (which-Nat (subtract x y) (which-Nat (subtract y x) 1 (lambda (_) 0)) (lambda (_) 0))
           )
)

;'Proposition generator'. If x and y are equal, return Trivial. Otherwise return Absurd
(claim prop_gen (-> Nat Nat U))
(define prop_gen (lambda (x y) 
                        (which-Nat (eq x y) Absurd (lambda (_) Trivial))
))

(claim final_lemma (Pi ((x Nat))  (prop_gen x x) ))
; How do I prove this? I think that it might be possible for me to prove `(= U Trivial (prop_gen x x))` for all x. I was then thinking how I could use that.

And finally, the reason why I wanted to do the whole thing above was to see if I could prove ¬ (1 = 2), in a slightly different way that was done in chapter 15 of the book. I think that if I could define prop_gen, I could use replace to prove the absurdity.

**Tags:** dependent-type, proofs, program-verification, proof-assistants


---

## 2 answers

### Answer by username_1 on 2024-10-07. Score: 4 | Accepted answer

You can just use replace with the identity function as the motive to transport along an equality of types.
In Martin-Löf type theory, the standard way to prove that e.g. $0 \neq 1$ is to define a type family $T : \mathbb{N} \to \mathcal{U}$ such that $T(0) = \top$ and $T(n + 1) = \bot$, then transport $\star : \top$ along the equality $0 = 1$ in $T$ to get an inhabitant of $\bot$. In fact you have to use $\mathcal{U}$: see The Independence of Peano's Fourth Axiom from
Martin-Löf's Type Theory without Universes.
EDIT by Suraaj: The following is a minimal reproducible Pie example:
(claim transport (Pi ((A U) (B U) (eq (= U A B)) (a A)) B))
(define transport 
  (lambda (A B eq a) (replace eq (lambda (x) x) a))
)

> **Comments:**
> **username_0**: Just to be clear - the Peano Axiom in question is "there is no number such that 0 is its sucessor", right?  
> **username_1**: Yes, that's the one.  

---

### Answer by username_2 on 2024-10-07. Score: -2

Usually one proves equality in order to prove another equality or to prove correct typing of something else. If you showed that $T\_1 \equiv T\_2$ then you should be able to derive the isomorphism functions $f:T\_1\to T\_2$ and $g:T\_2\to T\_1$. The function $f$ should be able to get you a typechecking judgment $f x : T\_2$ if you have $x : T\_1$.

It is another question how to write all this in the syntax of Pie. That I am not sure about.


---

