All Questions
Tagged with category-theory natural-numbers
1
question
1
vote
1
answer
85
views
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
- 345