00:01:13 -!- augur has joined. 00:34:07 -!- hppavilion[1] has quit (Read error: Connection reset by peer). 00:34:31 -!- hppavilion[1] has joined. 00:35:01 -!- Slereah has quit (Ping timeout: 255 seconds). 00:47:35 -!- Slereah has joined. 00:50:49 -!- Slereah__ has joined. 00:52:01 -!- Slereah has quit (Ping timeout: 248 seconds). 00:56:57 -!- Slereah has joined. 00:58:17 -!- Slereah__ has quit (Ping timeout: 260 seconds). 00:59:30 -!- Slereah__ has joined. 01:01:47 -!- Slereah has quit (Ping timeout: 260 seconds). 01:14:03 -!- Slereah has joined. 01:14:16 -!- Slereah__ has quit (Ping timeout: 260 seconds). 01:30:00 -!- xkapastel has quit (Quit: Connection closed for inactivity). 01:31:08 -!- ais523 has joined. 01:36:14 -!- Slereah__ has joined. 01:37:27 -!- Slereah has quit (Ping timeout: 240 seconds). 01:38:49 -!- Slereah has joined. 01:40:23 -!- imode has joined. 01:40:52 -!- Slereah__ has quit (Ping timeout: 260 seconds). 01:46:43 -!- Slereah__ has joined. 01:47:35 -!- Slereah has quit (Ping timeout: 240 seconds). 01:52:58 -!- doesthiswork has joined. 02:35:00 -!- tswett_ has joined. 02:35:13 -!- ais523 has quit (Remote host closed the connection). 02:36:24 -!- ais523 has joined. 02:42:28 -!- Slereah__ has quit (Ping timeout: 260 seconds). 02:50:17 -!- hppavilion[1] has quit (Ping timeout: 260 seconds). 02:54:04 -!- hppavilion[1] has joined. 03:10:07 -!- Slereah has joined. 03:14:52 -!- Slereah__ has joined. 03:16:35 -!- Slereah has quit (Ping timeout: 240 seconds). 03:19:18 -!- Slereah__ has quit (Ping timeout: 255 seconds). 03:25:49 We can invent the computer design that is like half between MIX and MMIX (almost), and, can be call MDIX. 03:26:43 zzo38: But I thought you said that MIX wasn't referring to a number. 03:26:45 `5 w 03:26:49 1/2:smell//Smell is a sense, which is particularly strong in old factory sites. \ the u//The U are a very mad people. \ program//A program is an image created by means of prography. \ warranty//HACKEGO COMES WITHOUT WARRANTY, EXPRESS OR IMPLIED, AND IS UNFIT FOR ANY PURPOSE, INCLUDING THE PURPOSE OF BEING UNFIT FOR ANYTHING. Its warranty has expire 03:26:52 `n 03:26:53 2/2:d. \ roujo//Roujo is a Java heretic leaning on ungrammatical Haskell. His claim to Canadianness is marred by an unholy portal to China. The treaties suffer, so the cocktail will be postponed. He does not understand shell quoting. 03:27:05 shachaf: It is referring to a number, but not a year number. 03:27:33 -!- PattuX has quit (Quit: Connection closed for inactivity). 03:27:37 Why would it refer to a number? 03:28:25 It is an average of the numbers of many other computers of the time (rounded down), apparently. 03:29:07 whoa, so it is. 03:38:06 -!- Slereah has joined. 03:38:55 zzo38: Are you going to ICFP this year? 03:40:57 -!- tswett_ has quit (Ping timeout: 240 seconds). 03:44:40 I do not think so. What day and where is it anyways? 03:44:55 I think it's in England. 03:45:03 Sep 3-9, Oxford 03:50:45 I do not expect to be in England in September 04:19:48 -!- sleffy has quit (Ping timeout: 268 seconds). 04:20:26 I tried loading a MMIX program with mmotype and it says "File was created Thu Jun 16 12:35:08 1881", even though I know that isn't the case. Why it says that? 04:30:39 -!- sleffy has joined. 04:37:04 -!- hppavilion[1] has quit (Ping timeout: 268 seconds). 04:37:46 -!- sleffy has quit (Ping timeout: 276 seconds). 04:54:24 -!- hppavilion[1] has joined. 05:10:01 -!- doesthiswork has quit (Quit: Leaving.). 05:12:40 -!- doesthiswork has joined. 05:26:54 book encoding is a neat hack for really tiny graphs. 05:27:57 just encode the graph as pages of planar graphs and concatenate them together. 05:29:50 -!- ^v has quit (Ping timeout: 258 seconds). 05:38:05 -!- ais523 has quit. 05:51:12 -!- sleffy has joined. 05:57:49 Do you have an example of that? 06:05:35 -!- sleffy has quit (Ping timeout: 240 seconds). 06:06:06 https://en.wikipedia.org/wiki/Book_embedding 06:07:56 OK 06:08:50 OK, that picture explains it 06:21:36 -!- erkin has joined. 06:46:13 -!- sleffy has joined. 07:02:08 -!- FreeFull has quit. 07:04:37 -!- sleffy has quit (Ping timeout: 260 seconds). 07:05:03 -!- sleffy has joined. 07:32:47 -!- doesthiswork has quit (Quit: Leaving.). 07:33:26 -!- sleffy has quit (Ping timeout: 268 seconds). 07:33:52 -!- sleffy has joined. 08:01:11 I have this way to round up to one less than a power of two in MMIX: SRU $0,in,8; ZSNZ $1,$0,255; MOR $0,#FF7F3F1F0F070301,in; OR out,$0,$1 (This assumes the input is a 16-bit number) Is there a better way? 08:01:40 -!- augur has quit (Remote host closed the connection). 08:02:43 Meaning, set all the bits lower than the highest set bit? 08:02:53 Yes 08:02:59 That is the same thing 08:05:28 (For a 8-bit number, the third instruction by itself is sufficient) 08:10:25 -!- sleffy has quit (Ping timeout: 255 seconds). 08:12:29 -!- sleffy has joined. 08:19:05 -!- augur has joined. 08:19:09 Do you like this? 08:20:40 -!- imode has quit (Ping timeout: 246 seconds). 08:20:41 There is also the way to reverse the bits of a 64-bit number in MMIX, which uses MOR twice, with the constant #0102040810204080, but once in the Y position and once in the Z position. 08:21:57 I think the MOR instruction of MMIX really is useful. 08:23:27 -!- augur has quit (Ping timeout: 240 seconds). 08:25:12 Do you like MXOR? 08:26:57 MXOR has less uses that I can find, but it may be good too 08:29:48 -!- AnotherTest has joined. 08:31:33 Obviously the one you mentioned has mor uses. 08:32:18 Yes 08:38:58 [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52527&oldid=52520 * LyricLy * (+89) 08:39:20 -!- augur has joined. 08:40:29 [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52528&oldid=52527 * LyricLy * (+58) /* ly.py */ 08:41:17 -!- augur has quit (Remote host closed the connection). 08:43:54 -!- sleffy has quit (Ping timeout: 240 seconds). 08:47:05 A single MXOR can be used to convert 8 bytes simultaneously from/to Gray code. Unfortunately, that's the most convincing use of MXOR that I have so far, disregarding the fact that in many cases, MXOR and MOR can be used interchangably, because one of the matrices is a permutation matrix. It seems that MXOR should help for some computations in GF(2^8) at least. 08:50:44 I did not think of Gray code, although I did realize the other thing you mention 09:34:43 -!- PattuX has joined. 10:48:29 -!- hppavilion[1] has quit (Quit: HRII'FHALMA MNAHN'K'YARNAK NGAH NILGH'RI'BTHNKNYTH). 11:34:51 -!- boily has joined. 11:38:09 @metar CYUL 11:38:09 CYUL 241000Z 04011G17KT 15SM BKN055 OVC080 17/09 A2986 RMK SC6AC2 SLP114 DENSITY ALT 500FT 11:42:00 -!- augur has joined. 11:46:25 -!- augur has quit (Ping timeout: 248 seconds). 12:10:43 @metar CYUL 12:10:43 CYUL 241100Z 04013KT 15SM OVC055 17/09 A2988 RMK SC8 SLP121 DENSITY ALT 500FT 12:10:59 clouder. 12:29:45 -!- boily has quit (Quit: HARMONIC CHICKEN). 13:31:58 <\oren\> https://twitter.com/Witch_chan2000/status/879189141954625539 13:37:49 -!- imode has joined. 14:00:32 -!- doesthiswork has joined. 14:30:16 -!- `^_^v has joined. 14:34:28 bad wikipedia articles are a gold mine of ideas 14:34:53 A program is how a robot decides when or how to do something. 14:35:13 a Program is a group of related projects managed in a coordinated manner to obtain benefits and control 14:35:40 the source code of a program is the design for the program that it produces 14:35:52 A program was a stack of layers. 14:45:38 -!- GeoDude has changed nick to GeekDude. 14:48:19 -!- tswett has quit (Quit: Leaving). 15:13:12 -!- doesthiswork has quit (Quit: Leaving.). 15:41:50 -!- heroux has quit (Ping timeout: 268 seconds). 15:42:41 -!- augur has joined. 15:43:29 -!- heroux has joined. 15:47:12 -!- augur has quit (Ping timeout: 255 seconds). 15:50:06 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...). 15:53:08 -!- `^_^v has quit (Ping timeout: 258 seconds). 15:54:30 -!- PattuX has quit (Quit: Connection closed for inactivity). 15:57:20 -!- `^_^v has joined. 16:37:27 -!- AnotherTest has quit (Ping timeout: 260 seconds). 16:46:25 -!- viznut_ has changed nick to viznut. 17:01:18 -!- `^_^v has quit (Quit: This computer has gone to sleep). 17:07:41 -!- PattuX has joined. 17:08:48 <\oren\> Lol I have a huge office to myself right now. we got a second office recently to store more programmers in but noone wants to be the first guy on the new office 17:12:33 -!- augur has joined. 17:21:40 -!- LKoen has joined. 17:27:12 -!- FreeFull has joined. 17:44:09 -!- augur has quit (Remote host closed the connection). 17:53:37 -!- __kerbal__ has joined. 18:04:28 -!- `^_^v has joined. 18:05:05 -!- Sprocklem has quit (Ping timeout: 248 seconds). 18:12:15 <* Taneb> hello 18:13:22 -!- AnotherTest has joined. 18:13:53 <__kerbal__> hello 18:17:07 I've just had a few rather fun days in Italy 18:17:55 Haneb 18:19:21 Hichaf 18:19:29 I saw that you saw a cat. 18:19:48 i was all, like, whoa, dude 18:20:00 Yes! 18:20:04 That was in Venice! 18:20:40 I saw a good cat last night but I didn't photograph. 18:26:28 `5 w 18:26:34 1/1:warrigal//Warrigal is #esoteric's resident dingo. It sometimes pretends to be a human. \ yeeeeeeesh//See yeeeeeesh. \ the//the Toe of Harriness's Enclosure \ hacker//Jim Hacker is a former British prime minister. \ companion cube//There's cake inside it. Tear it apart, rip open your companion, and extract the delicious, delicious cake... 18:27:11 `cwlprits companion cube 18:27:18 zgrëp zgrëp 18:27:21 `? cats 18:27:22 Cats are cool, but should be illegal. 18:27:26 `? kitten 18:27:27 kitten? ¯\(°​_o)/¯ 18:30:47 <\oren\> Argh, the coffee machine is very advanced, but you still have to take the milk carafe out of the fridge and put it back each time 18:31:14 I've seen coffee machines that made lattes 18:31:31 <\oren\> Maybe in 2020 we'll finally have an integrated milk chiller 18:34:09 <\oren\> 식료품groceries is good music for blasting in a completely empty empty office 18:34:56 lulz 18:34:58 Good one! 18:45:29 thanks for the weird music \oren\. 18:47:24 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 18:53:11 -!- augur has joined. 18:53:22 -!- sleffy has joined. 18:54:12 -!- augur has quit (Remote host closed the connection). 18:55:21 -!- augur has joined. 19:08:20 `` cd wisdom; for f in ye*sh; do \? $f; done 19:08:24 ​/hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: cd: wisdom: Not a directory \ /hackenv/bin/?: line 5: 19:09:29 -!- ais523 has joined. 19:09:55 `` cd wisdom; for f in ye*sh; do echo -n "$f//"; cat "$f"; done 19:09:56 yeeeeeeeeeesh//See yeeeeeeeeesh. \ yeeeeeeeesh//See yeeeeeeesh. \ yeeeeeeesh//See yeeeeeesh. \ yeeeeeesh//See yeeeeesh. \ yeeeeesh//See yeeeesh. \ yeeeesh//See yeeesh. \ yeeesh//See yeesh. 19:10:06 `? yeesh 19:10:07 yeesh? ¯\(°​_o)/¯ 19:10:31 `dowg yeesh 19:10:37 No output. 19:10:40 how useful 19:10:45 😎 19:10:47 `dowg yeeesh 19:10:54 6202:2015-11-10 le/rn yeeesh/See yeesh. 19:11:12 `dowg yeeeeeeeeeesh 19:11:18 6229:2015-11-19 le/rn yeeeeeeeeeesh/See yeeeeeeeeesh. 19:11:28 one per day? 19:11:30 `dowg yeeeeeeeeesh 19:11:36 10346:2017-03-04 forget yeeeeeeeeesh \ 6228:2015-11-19 le/rn yeeeeeeeeesh/See yeeeeeeeesh. 19:12:09 `? int-e 19:12:10 int-e är inte svensk. Hen kommer att spränga solen. Hen står för sig själv. Hen gillar inte färger, men han gillar dissonans. Er hat ein Hipster-Spiel gekauft. 19:12:28 int-e is into rutabagas? 19:13:05 `` echo wisdom/no*dl 19:13:06 wisdom/nooooodl 19:13:27 -!- augur has quit (Remote host closed the connection). 19:14:31 shachaf: why'd you "`forget" that one but not the others? 19:15:05 So you'll have something to ask. 19:15:39 `dowg yeeeeesh 19:15:45 11080:2017-07-10 revert \ 11079:2017-07-10 forget yeeeeesh \ 6200:2015-11-10 le/rn yeeeeesh/See yeeeesh. 19:15:48 `cd wisdom; echo ye*sh 19:15:49 ​invalid command ( ͡° ͜ʖ ͡°) 19:15:53 `` cd wisdom; echo ye*sh 19:15:54 yeeeeeeeeeesh yeeeeeeeesh yeeeeeeesh yeeeeeesh yeeeeesh yeeeesh yeeesh 19:16:02 `doag bin/cd 19:16:09 7819:2016-05-06 mkx bin/cd//erro "invalid command ( \xcd\xa1\xc2\xb0 \xcd\x9c\xca\x96 \xcd\xa1\xc2\xb0)" \ 7818:2016-05-06 mkx bin/cd//erro invalid command ( \xcd\xa1\xc2\xb0 \xcd\x9c\xca\x96 \xcd\xa1\xc2\xb0) \ 7817:2016-05-06 mkx bin/cd//echo stop trying, it doesnt work 19:16:27 `rm bin/cd 19:16:28 No output. 19:16:35 cd oughtn't be a command anyway. 19:16:41 `` rm wisdom/ye*sh 19:16:43 No output. 19:16:45 kkkk 19:16:46 😉 19:16:59 Except I once wrote a cd program that attaches to its parent with ptrace and changes its current directory. 19:17:24 Oh it's part of the moon episode. 19:19:30 -!- ais523 has quit (Remote host closed the connection). 19:20:40 -!- ais523 has joined. 19:21:44 -!- __kerbal__ has quit (Ping timeout: 260 seconds). 19:24:42 -!- ais523 has quit (Remote host closed the connection). 19:25:53 -!- ais523 has joined. 19:26:15 -!- augur has joined. 20:29:46 -!- imode has quit (Ping timeout: 255 seconds). 20:43:37 `5 w 20:43:41 1/3:virgil//Virgil is a prayer at dawn, as well as an ancient Italian poet who led Dante to hell so they can ask the blind transgendered seer Anchises stupid politics questions concerning contemporary noble families. \ dingbat//dingbat is a famous font designer for Microsoft. \ usb3//USB3 hosts are packaged with a full independent implementation of 20:43:43 `n 20:43:44 2/3: the older USB/USB2, going through separate pins in the same socket. It is similar to DVI, except you need a separate passive converter stub to plug VGA monitor to DVI socket, but you don't need one to plug a USB client to an USB3 host. \ ngram model//An ngram model is just a Markov model with a sliding window state. \ associativity//Associativ 20:43:46 `n 20:43:47 3/3:ity means that h(th) = (ht)h, if you're flexible about it. 20:44:48 `5 20:44:49 1/2:255) it is from 2002 though, I was younger then \ 763) when everyone else was busy going "ewwww, comic sans!" I was reading the text and learned everything \ 525) Mayor says we need to make aluminum items Taneb, PH says you need to make lava items. \ 609) the parser would be even simpler if I 20:44:50 `n 20:44:51 2/2: didn't try to do type inference in it \ 127) Sgeo: hahaah, and i love when they announced it i dare u to press alt f4 and your house ( acts 16:31 your bible) 20:45:16 Taneb: Don't you mean aluminium? 20:45:42 shachaf, Ideally, yes 21:00:38 this fosforic spelling dispute is sodum 21:02:00 apparently the element named for copernicus is copernicium 21:02:53 Are you sure that's not just a variant of copper? 21:03:45 [wiki] [[User:Scoppini]] https://esolangs.org/w/index.php?diff=52529&oldid=44156 * Scoppini * (+14) 21:04:04 as surely as 1 and 1 make 2 21:04:34 you gotta tell me if you're a copernicus 21:04:50 [wiki] [[Language list]] https://esolangs.org/w/index.php?diff=52530&oldid=52448 * Scoppini * (+14) /* S */ 21:05:19 [wiki] [[Language list]] https://esolangs.org/w/index.php?diff=52531&oldid=52530 * Scoppini * (+0) /* S */ 21:10:53 there's also pernicium, named for being pernicious 21:12:59 -!- imode has joined. 21:13:46 Please see http://feelingmyage.co.uk/wp-content/uploads/2011/09/periodictable.gif 21:14:11 what the hell. can any of you see me? 21:14:30 or am I just typing to a dead terminal. 21:15:23 Or is it both? 21:15:32 You feel like you are being watched. 21:15:43 oh wow, okay. so this network doesn't block IRC, but it locks web browsing behind guest access. 21:15:55 time to tunnel. 21:16:36 I think there are easier ways to check whether you're connected to IRC, for example /msg imode test 21:16:59 shachaf: yeah, I figured. but I was so dumbstruck that I didn't think of it. :P 21:26:13 <\oren\> So I guess the main reason I even need to come to work is so I can move a jumper and push a red button now and then 21:27:32 <\oren\> er, wait not jumper. breaker? 21:27:58 <\oren\> the thingy that resets after a power problem 21:29:36 breaker. 21:29:42 \oren\: isn't "breaker" the name of your current build system hth 21:29:48 <\oren\> no 21:30:13 <\oren\> the component I'm working on now uses boost jam 21:32:21 <\oren\> anyway, luckily, it seems I het the right red button 21:52:06 -!- augur has quit (Remote host closed the connection). 21:58:06 -!- augur has joined. 22:12:26 I commonly use "PING ME" to test if IRC connection is working (the server will respond PONG if it is OK) 22:12:53 most clients do that automatically every now and then 22:13:44 \oren\: "circuit breaker" is the normal phrase in British English 22:14:05 referring to a fuse-like component that works electromechanically rather than via physically catching fire, and thus is resettable rather than needing to be replaced 22:18:10 -!- imode has quit (Ping timeout: 240 seconds). 22:37:27 -!- AnotherTest has quit (Ping timeout: 240 seconds). 22:37:31 My own client automatically responds to the server's pings (unless you turn off that function), but does not emit its own automatically 22:38:36 -!- hppavilion[1] has joined. 22:45:43 -!- boily has joined. 22:45:46 @metar CYUL 22:45:46 CYUL 242138Z 08011G16KT 5SM -RA BR FEW009 SCT014 OVC025 16/14 A2995 RMK SF1SC2SC5 SLP143 DENSITY ALT 200FT 22:50:32 -!- `^_^v has quit (Quit: This computer has gone to sleep). 23:14:18 -!- tswett has joined. 23:18:37 I'm pondering what I might use as a "home theory" for math. 23:19:21 A lot of mathematicians seem to "live in" ZFC. They consider the axioms of ZFC to be true statements, and they don't worry too much about their theorems not generalizing outside of ZFC. 23:20:47 I'd call myself a bit more of a skeptic. 23:21:32 I'll admit the axioms of extensionality, specification, pairing, union, replacement, and infinity. 23:21:40 Power sets seem suspect. 23:21:49 And the axiom of choice? Hahaha. 23:25:02 I want my home theory to be something I can actually think of a model of. 23:25:25 Do they really? 23:25:46 https://arxiv.org/pdf/1212.6543.pdf suggests otherwise. 23:26:15 It suggests that power sets *don't* seem suspect? 23:27:38 "Perhaps you will wake up tomorrow, check your email, and find an announcement that ZFC is inconsistent. Apparently, someone has taken the ZFC axioms, performed a long string of logical deductions, and arrived at a contradiction. The work has been checked and re-checked. There is no longer any doubt." 23:27:43 "How would you react? In particular, how would you feel about the implications for your own work? All your theorems would still be true under ZFC, but so too would their negations. Would you conclude that your life’s work had been destroyed?" 23:29:38 I don't normally work in ZFC, but if I did, I'd try to identify which axiom was incorrect and see what could be proved without it 23:29:54 the axiom of choice is a big suspect in that respect 23:30:18 But in ZFC is inconsistent, ZF is inconsistent, too. 23:30:27 although, I thought the axiom of choice had been proven to be independent of ZF? if so, that implies that ZFC is consistent by definition 23:30:39 (if ZF is inconsistent, nothing is independent of it) 23:30:40 Oh, so ZF is consistent now? :) 23:30:42 I guess the proof could be wrong 23:31:34 You can have the same collapse in the meta theory 23:31:45 then ZF could be proved both consistent and inconsistent 23:31:59 I like that 23:32:07 OTOH it'd leave me sceptical of the proof that ZFC were inconsistent 23:32:20 on the basis that there's no reason to conclude that that proof were "about" ZFC 23:32:22 british spellings are so odd sometimes 23:32:43 US spells "sceptical" with a k, right? 23:32:51 that looks bizarre to me 23:32:53 yes, sceptikal 23:33:05 "Sceptical" is still pronounced like "skeptical", right? 23:33:20 yes, the start is like "sceptre" 23:33:36 (which is also spelled differently in US English, but it's the end of the word that's spelled differently, not the start) 23:33:38 Wait, how do you pronounce "sceptre"? 23:33:56 skep - ter 23:33:59 septer 23:34:10 although come to think of it I probably pronounce it incorrectly 23:34:18 I always thought it was "septer", and https://encrypted.google.com/search?q=define:sceptre agrees. 23:34:24 it'd make sence if the c were silent 23:34:41 my written vocabulary is rather larger than my spoken vocabulary 23:34:47 because most of my social interaction is online nowadays 23:34:56 I learned a lot of my English from reading. 23:35:04 But since then I've spoken a fair amount. 23:35:14 So lemme figure out the... uh... what do you call a property of a category that asserts that it contains objects of a particular type? 23:35:15 I still have a noticeable non-native accent, though. 23:35:25 "has"? 23:35:31 "has products" 23:35:32 Sure, a "has-property". 23:35:41 "gains products until end of turn" 23:35:47 "type" here is informal-English, rather than the technical programming meaning? 23:35:49 Lemme figure out the has-properties I'm willing to admit. 23:35:54 ais523: yeah. 23:36:03 So cartesian closedness is a has-property. 23:36:10 A category is cartesian closed if it has exponentials. 23:36:19 "your categories have flying. your opponents' categories lose flying and cannot gain flying." 23:36:28 tswett: we call those commutativity properties 23:36:39 I'll take finite limits and coproducts (for $200, Alex). 23:36:46 i.e. a property that a category obeys a certain commutative diagram 23:37:00 some of them have distinguished objects or morphisms that are necessary to make the diagrams work 23:37:16 Or a certain family of commutative diagrams? 23:37:28 Are commutative diagrams different from equations? 23:37:28 ais523: that sounds like it means there are commutativity properties that aren't "has-properties". 23:37:45 Well, a commutative diagram is essentially a finite collection of equations, right? 23:37:50 Unless it's an infinite diagram, of course. 23:37:50 shachaf: normally they're like equations but with naturality requirements 23:38:06 Commutative diagrams have naturality requirements? 23:38:09 I could explain this better if I understood it myself 23:38:11 which I don't really 23:39:40 I'll also take nLab's "parametrized natural numbers objects". 23:43:00 i,i skeptic tank 23:45:17 shachaf: seems there /isn't/ a naturality requirement; I just looked it up 23:45:27 so right, just equations 23:45:33 I can, in fact, think of a model of this "theory"... I think... 23:45:40 The objects are all primitive recursive subsets of N. 23:45:48 And the morphisms are all primitive recursive functions. 23:45:57 -!- hppavilion[0] has joined. 23:46:20 Where I guess a "primitive recursive subset" would have to be defined as a set whose membership function is a primitive recursive function. 23:47:36 -!- hppavilion[1] has quit (Ping timeout: 260 seconds). 23:48:40 Except I don't know if that actually works... 23:49:51 That category "obviously" has products, coproducts, and a PNNO. So the only question is whether or not it has pullbacks. 23:50:21 Yeah, it totally has pullbacks.