Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
intuitionistic_propositional_logic [2016/04/13 11:17] nikolaj |
intuitionistic_propositional_logic [2016/04/13 11:17] nikolaj |
||
|---|---|---|---|
| Line 313: | Line 313: | ||
| Under the BHK interpretation (Curry-Howard), this reads" | Under the BHK interpretation (Curry-Howard), this reads" | ||
| - | "Given any 'function to $B$', that we may call $f$, as well as a function $F$ from a 'functions to B' to $B$, you can construct an element $F(f)$ of $B$. | + | "Given any 'function to $B$', that we may call $f$, as well as a function $F$ from a 'functions to $B$' to $B$, you can construct an element $F(f)$ of $B$. |
| In type theory, the judgement is | In type theory, the judgement is | ||
