On 2 April 2015 at 11:20, Keean Schupke <[email protected]> wrote: > > Kind >> | Bool >> | | True >> | | False >> | >> | Type >> | | bool >> | | | true >> | | | false >> | | >> | | int >> | | float >> | | etc... >> > > This doesn't look like type-theory to me. >
Sorry, now I look at it more closely you have 'bool' as a type and 'Bool' as a kind. This is exactly what I had in my original table, but its just not intuitionistic type theory. Its probably fine, but the intuitionistic type-theory universes are an alternative way of formulating this, that seems bit better to me. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
