# Re: [Epigram] Definitional equality in observational type theory

```Hi Robin,

```

```
```
```I've been reading "Towards Observational Type Theory". I'm new to type
theory, so I have not been able to understand big chunks of the paper;
hopefully as I read wider I'll understand more of it.
```
```
We should certainly strive to fix this...

```
```
```
However, one rule which jumped out at me is this, on page 9, because it
```seems silly (apologies if my email client mangles this even after I've
```
tried to fix it up - I've never tried pasting type rules from PDFs into
```it before):

Γ |- S≡T  Γ |- Q:S=T  Γ |- s:S
------------------------------
T
Γ |- s[Q>S ≡ s : T

```
It seems silly to include a definitional equality as a premise, because I _thought_ the whole point of definitional equality was that S≡T means
```that S and T are freely co-substitutable, and type-checking will
automatically substitute S for T or T for S _whenever_ required. (For
example, it is often noted that Coq will automatically reduce (i.e.
substitute) n+0 to n in a dependent type - but only if you write n+0
```
the "right" way round! I can't remember offhand which way round works.)
```
```
```
```
You are right to say that this rule is unusual. In the implementation it creates a dependency between defintional equaliy and reduction which doesn't appear in conventional systems.
```
```
It can be justified by observing that in intensional Type Theory we have tat
```
s [refl S> ≡ s

```
where refl S : S=S. However, due to proof-irrelevance any term Q : S = S will be definitionally equal to refl S, hence if p:S=S then
```
s [p> ≡ s

```
```So anyway, surely any derivation which needed that rule could also

Γ |- Q:S=S  Γ |- s:S
------------------------------
S
Γ |- s[Q>S ≡ s : S

(which is trivial), substituting S for T before applying it, and
substituting Ts for some of the Ss afterwards.

```
```
```
You are right - your rule is equivalent and more concise. However, a type checker will have to implement the first rule. To check whether s [Q> reduces to s you have to verify whether the types in the type of Q:S = T are definitionally equal, i.e. whether S ≡ T.
```
```
```Where have I gone wrong?

```
```
Indeed nowhere.

```
There is some discussion of related issues in the Epigram developers blog:
```
http://www.e-pig.org/epilogue/

is particular in the Epigram 2 design doc.

Cheers,
Thorsten
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

```