## Minutes

Meeting:

- Thorsten should type:
`darcs get http://sneezy.cs.nott.ac.uk/darcs/term`

`cd term`

`chmod +x Setup.hs`

`./Setup.hs configure --prefix=$HOME`

`./Setup.hs build`

`./Setup.hs install --user`

- (and providing $HOME/bin is in your path:)
`epigram`

- The next job in term is to build equality in these steps:
- Propositional equality

coersions between equal types (and the proof that these are coherant)

and the structural rule for application

- Proof-irrelevance for equality, to do this right we need to decide equality during evaluation (if we do not have a proof of an equation but it’s homogeneous, then we win anyway). The upshot is Equality.lhs and
`eval`

from Term.lhs need to be in the same file. - Observational equavalence, at some point (sooner rather than later) we’ll include the structural rule for :

Thorsten pointed out that is rule can be derived from substution of equals for equals plus the more primitive:

Having this gives OTT a simpler core, but Conor prefers the first version because it is easier to program with.

- Propositional equality