Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added a link to generalized the.
And a link to definite description.
What is up with all these long lists of “rules” for things in type theory? No one doing type theory works with things defined like that. Only the primitive type-formers are specified by rules; for actually doing mathematics we just define things in terms of the primitive ones.
clarified that these rules are needed in strongly predicative mathematics where one doesn’t have general dependent function types
Anonymous
Do you have a citation for anyone doing strongly predicative mathematics in type theory in this way?
1 to 9 of 9