On 2 April 2015 at 18:31, Matt Oliveri <[email protected]> wrote: > This is not an accurate statement about math in Martin-Lof type > theory, since MLTT comes with natural numbers and booleans, all > "magicked up" for you. Newer derivatives of MLTT have general > inductive types magicked up for you. In either case, you don't build > these objects out of types. How would that even work?
The Twelf logical-framework is the neatest example of this, quoting the Twelf manual: nat: type. > z: nat. > s: nat -> nat. > The first line declares that nat is a type. The second line declares z > (zero) to be an object of type nat, and the third line declars s > (successor) to be a type constructor that takes an object N of type nat and > produces another object (s N) of type nat. > plus: nat -> nat -> nat -> type. > p-z: plus z N N. > p-s: plus (s N1) N2 (s N3) > <- plus N1 N2 N3. > The first line defines the judgment, declaring plus to be a type family > indexed by three terms of type nat. > The second line declares that for any natural number N, p-z is an object > of type plus z N N, which corresponds to the axiom p-z above. The N is an > implicit parameter - it is treated as a bound variable by Twelf, which you > can see by looking at Twelf's output after checking the above code. > The third line says that p-s is a type constructor that, given an object D > of type plus N1 N2 N3 (where N1, N2, and N3 are all implicit parameters > that can be treated as metavariables), produces an object, p-s D, with type > plus (s N1) N2 (s N3). This corresponds to the rule p-s Now I realise that is says z is an object, but there is no reason we have to be operating at the bottom. z can just as easily be one level higher, and be an empty universe at the U0 level, and 'nat' is now at the U1 level. Now we don't need values at all, we can build everything from empty universes, like everything is set theory is built from empty sets. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
