bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 2: functions #22

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

Small comment about the discussion on functions.

Functions are defined in terms of binary relations, and they have a nice characterization that is dual to the concepts of "one-to-one" and "onto".

A function is a binary relation $f \subseteq A \times B$ that is also

bor0 commented 6 years ago

This is an interesting observation. However, I am wondering if it should go in the footnotes, as it may be distracting a bit.