Newest at the top
| 2025-01-10 11:33:59 +0100 | <geekosaur> | types are sets, (mathematical) functions are relations between sets/types |
| 2025-01-10 11:31:17 +0100 | <alist> | *values, not elements |
| 2025-01-10 11:31:08 +0100 | <alist> | i thought they were relations, at first. i thought the author was saying that because just naively modeling types as sets of their elements didn't work out, so we are going to use relations |
| 2025-01-10 11:30:35 +0100 | <alist> | so, what are the targets of this isomorphism you mention? what are the types mapped to? |
| 2025-01-10 11:30:11 +0100 | <alist> | sorry i was just trying to understand what you wrote and what the author wrote |
| 2025-01-10 11:28:53 +0100 | <merijn> | What is the source of confusion? |
| 2025-01-10 11:27:42 +0100 | <alist> | lol |
| 2025-01-10 11:26:07 +0100 | <merijn> | That sounds about right for reading type theory papers :D |
| 2025-01-10 11:24:57 +0100 | <alist> | ok now i am confused |
| 2025-01-10 11:23:36 +0100 | <merijn> | i.e. types as sets of elements and functions as relations between their input set and output set |
| 2025-01-10 11:22:57 +0100 | <merijn> | alist: In section 2, on the bottom of page 4 the example is basically explaining an isomorphism between "types and functions" and "sets and relations" |
| 2025-01-10 11:21:32 +0100 | <merijn> | Not that everything is built in term of those |
| 2025-01-10 11:21:26 +0100 | <merijn> | alist: The identity type is only mentioned as a special relation |
| 2025-01-10 11:21:03 +0100 | <alist> | i see i see |
| 2025-01-10 11:20:47 +0100 | <merijn> | I don't think that's intended anywhere in the paper |
| 2025-01-10 11:20:22 +0100 | <merijn> | from the constant types, which are represented as identity relations |
| 2025-01-10 11:20:15 +0100 | <merijn> | alist: "i thought the relations we are quantifying over are inductively built |
| 2025-01-10 11:19:56 +0100 | <merijn> | alist: ah, I think you misinterpreted part of the intro stuff |
| 2025-01-10 11:11:47 +0100 | <alist> | it begins with the phrase "This can be further expanded in terms of the definition[...]" |
| 2025-01-10 11:11:03 +0100 | <alist> | in the paragraph preceding the fifth block of latex in section 3.1, the author says they are "specializing to the case where the relation[...]" |
| 2025-01-10 11:09:51 +0100 | <alist> | ah no worries |
| 2025-01-10 11:09:34 +0100 | <merijn> | I'm not really sure which part of the section you're referring too (and also, it's been a while since I read this xD) |
| 2025-01-10 11:05:06 +0100 | <alist> | i will add that although the identity relations are functions, on page 1 the author says that the result holds for "all total functions" with the proper (co)domain |
| 2025-01-10 11:02:57 +0100 | <alist> | oh it is on page 5. sorry, it's 4am here |
| 2025-01-10 11:02:25 +0100 | <merijn> | Link? Because my copy has section 3.1 on page 5 :p |
| 2025-01-10 11:00:39 +0100 | <alist> | any thoughts are appreciated |
| 2025-01-10 10:58:54 +0100 | <alist> | so, then, is the author really is quantifying over all possible relations? i am just confused |
| 2025-01-10 10:57:26 +0100 | <alist> | as far as i can tell, none of the type constructors' relation analogs will give rise to relations which are also set-theoretic functions |
| 2025-01-10 10:56:58 +0100 | <alist> | however, i'm confused, because i thought the relations we are quantifying over are inductively built from the constant types, which are represented as identity relations |
| 2025-01-10 10:55:55 +0100 | <alist> | in the parametricity demonstration in section 3.1 on page 8, the author uses their trick of specializing the quantified relations to the case of set-theoretic functions |
| 2025-01-10 10:54:24 +0100 | <alist> | i have another question about the paper "theorems for free" |
| 2025-01-10 10:52:49 +0100 | alist | (~alist@user/alist) alist |
| 2025-01-10 10:51:08 +0100 | xff0x | (~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp) (Ping timeout: 252 seconds) |
| 2025-01-10 10:48:00 +0100 | mari-estel | (~mari-este@user/mari-estel) mari-estel |
| 2025-01-10 10:47:33 +0100 | forell | (~forell@user/forell) forell |
| 2025-01-10 10:45:01 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) |
| 2025-01-10 10:44:40 +0100 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2025-01-10 10:42:23 +0100 | Smiles | (uid551636@id-551636.lymington.irccloud.com) Smiles |
| 2025-01-10 10:39:00 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) lxsameer |
| 2025-01-10 10:35:44 +0100 | mari-estel | (~mari-este@user/mari-estel) (Ping timeout: 252 seconds) |
| 2025-01-10 10:27:29 +0100 | Angelz | (Angelz@Angelz.oddprotocol.org) |
| 2025-01-10 10:26:28 +0100 | mange | (~user@user/mange) mange |
| 2025-01-10 10:23:21 +0100 | Angelz | (Angelz@2605:6400:30:fc15:d55b:fa6c:bd14:9973) (Remote host closed the connection) |
| 2025-01-10 10:23:09 +0100 | Angelz | (Angelz@2605:6400:30:fc15:d55b:fa6c:bd14:9973) |
| 2025-01-10 10:21:31 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-01-10 10:19:57 +0100 | eL_Bart0 | (eL_Bart0@dietunichtguten.org) (Ping timeout: 252 seconds) |
| 2025-01-10 10:17:58 +0100 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) (Remote host closed the connection) |
| 2025-01-10 10:16:30 +0100 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2025-01-10 10:11:40 +0100 | Angelz | (Angelz@2605:6400:30:fc15:9bd1:2217:41cd:bb15) |
| 2025-01-10 10:10:51 +0100 | vanishingideal | (~vanishing@user/vanishingideal) vanishingideal |