2025/04/10

2025-04-10 00:01:13 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-10 00:01:30 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 00:02:35 +0200tromp(~textual@2001:1c00:3487:1b00:2db1:da99:c28d:36bf) (Quit: My iMac has gone to sleep. ZZZzzz…)
2025-04-10 00:02:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 00:08:05 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) krjst
2025-04-10 00:08:10 +0200tv(~tv@user/tv) (Read error: Connection reset by peer)
2025-04-10 00:14:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 00:15:20 +0200ljdarj1(~Thunderbi@user/ljdarj) ljdarj
2025-04-10 00:16:52 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
2025-04-10 00:18:26 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-04-10 00:18:26 +0200ljdarj1ljdarj
2025-04-10 00:20:20 +0200 <__monty__> Can you elaborate?
2025-04-10 00:21:20 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 00:21:39 +0200__monty__(~toonn@user/toonn) (Quit: leaving)
2025-04-10 00:23:00 +0200chiselfuse(~chiselfus@user/chiselfuse) (Ping timeout: 264 seconds)
2025-04-10 00:23:47 +0200chiselfuse(~chiselfus@user/chiselfuse) chiselfuse
2025-04-10 00:32:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 00:33:09 +0200 <EvanR> supposedly A * B * C * D = A * (B * C) * D = (A * B) * C * C
2025-04-10 00:33:14 +0200 <EvanR> D
2025-04-10 00:33:23 +0200 <EvanR> but not really xD
2025-04-10 00:33:33 +0200 <EvanR> when you get down to brass tacks
2025-04-10 00:33:59 +0200 <EvanR> (or ML)
2025-04-10 00:37:09 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 00:43:40 +0200tv(~tv@user/tv) tv
2025-04-10 00:43:48 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) krjst
2025-04-10 00:47:52 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 00:52:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 246 seconds)
2025-04-10 00:53:31 +0200Sgeo(~Sgeo@user/sgeo) Sgeo
2025-04-10 01:00:16 +0200krjst(~krjst@2604:a880:800:c1::16b:8001) (Quit: bye)
2025-04-10 01:03:40 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:04:10 +0200ystael(~ystael@user/ystael) (Ping timeout: 272 seconds)
2025-04-10 01:06:30 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:07:28 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Client Quit)
2025-04-10 01:08:09 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:08:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 01:09:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 01:11:44 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2025-04-10 01:14:30 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye)
2025-04-10 01:14:59 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 01:19:17 +0200Square(~Square4@user/square) (Ping timeout: 248 seconds)
2025-04-10 01:19:28 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:19:42 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:21:44 +0200polykernel(~polykerne@user/polykernel) (Ping timeout: 252 seconds)
2025-04-10 01:23:46 +0200polykernel(~polykerne@user/polykernel) polykernel
2025-04-10 01:24:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-10 01:25:09 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2025-04-10 01:28:02 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds)
2025-04-10 01:29:29 +0200ljdarj(~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds)
2025-04-10 01:31:04 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:31:53 +0200Square2(~Square@user/square) Square
2025-04-10 01:33:45 +0200sprotte24(~sprotte24@p200300d16f0bc1000c82a6b41033ea55.dip0.t-ipconnect.de) (Quit: Leaving)
2025-04-10 01:35:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:35:49 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 248 seconds)
2025-04-10 01:39:34 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.)
2025-04-10 01:39:58 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 01:48:53 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:51:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 01:56:12 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net) (Ping timeout: 252 seconds)
2025-04-10 01:56:49 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e)
2025-04-10 01:57:02 +0200inca(~inca@pool-96-255-212-224.washdc.fios.verizon.net)
2025-04-10 01:57:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds)
2025-04-10 01:59:05 +0200XZDX(~xzdx@2601:404:ce00:4e51:214:51ff:fe2b:e82e) (Changing host)
2025-04-10 01:59:05 +0200XZDX(~xzdx@user/XZDX) XZDX
2025-04-10 02:03:10 +0200jespada(~jespada@r190-133-30-51.dialup.adsl.anteldata.net.uy) (Ping timeout: 252 seconds)
2025-04-10 02:08:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:11:52 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) (Quit: bye)
2025-04-10 02:12:13 +0200krjst(~krjst@2a0a:4cc0:2000:789a:b827:c6ff:fed6:bb48) krjst
2025-04-10 02:13:05 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)
2025-04-10 02:21:38 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Remote host closed the connection)
2025-04-10 02:22:22 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de)
2025-04-10 02:23:55 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 02:23:56 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:25:18 +0200poscat0x04(~poscat@user/poscat) (Ping timeout: 276 seconds)
2025-04-10 02:26:16 +0200machinedgod(~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 252 seconds)
2025-04-10 02:28:37 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 02:31:02 +0200polyphem(~rod@p4fc2cdf8.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-04-10 02:31:05 +0200 <EvanR> Frege observed, as we did above, that in the study of functions it is sufficient to focus on unary functions (i.e., functions that take exactly one argument).
2025-04-10 02:31:22 +0200 <EvanR> (The procedure of viewing a multiple-arity operation as a sequence of abstractions that yield an equivalent unary operation is called currying the operation.
2025-04-10 02:31:29 +0200 <EvanR> Perhaps it would be more historically accurate to call the operation fregeing, but there are often miscarriages of justice in the appellation of mathematical ideas.)
2025-04-10 02:31:45 +0200 <EvanR> lol
2025-04-10 02:32:29 +0200 <haskellbridge> <Morj> There's a quote you can find that someone who invented the thing is less powerful than the one who named this thing
2025-04-10 02:32:32 +0200 <haskellbridge> <Morj> I call it Morj's law
2025-04-10 02:38:01 +0200poscat(~poscat@user/poscat) poscat
2025-04-10 02:39:25 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 02:39:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:45:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 02:45:35 +0200notdabs(~Owner@2600:1700:69cf:9000:19b2:995a:60d5:3b93) (Quit: Leaving)
2025-04-10 02:53:09 +0200xff0x(~xff0x@2405:6580:b080:900:b50:e5e9:27c3:86) (Ping timeout: 248 seconds)
2025-04-10 02:55:31 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 02:55:49 +0200foul_owl(~kerry@94.156.149.99) (Ping timeout: 248 seconds)
2025-04-10 02:58:09 +0200otto_s(~user@p4ff27c58.dip0.t-ipconnect.de) (Ping timeout: 252 seconds)
2025-04-10 03:00:05 +0200otto_s(~user@p4ff278a2.dip0.t-ipconnect.de)
2025-04-10 03:01:03 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 276 seconds)
2025-04-10 03:03:56 +0200acidjnk_new(~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de)
2025-04-10 03:05:53 +0200acidjnk_new3(~acidjnk@p200300d6e71c4f997cc0cb9b6e0fa5d7.dip0.t-ipconnect.de) (Ping timeout: 248 seconds)
2025-04-10 03:06:42 +0200foul_owl(~kerry@174-21-146-90.tukw.qwest.net) foul_owl
2025-04-10 03:08:43 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 245 seconds)
2025-04-10 03:13:42 +0200j1n37-(~j1n37@user/j1n37) j1n37
2025-04-10 03:13:56 +0200j1n37(~j1n37@user/j1n37) (Ping timeout: 252 seconds)
2025-04-10 03:21:07 +0200tavare(~tavare@150.129.88.189) tavare
2025-04-10 03:21:07 +0200tavare(~tavare@150.129.88.189) (Changing host)
2025-04-10 03:21:07 +0200tavare(~tavare@user/tavare) tavare
2025-04-10 03:25:05 +0200acidjnk_new(~acidjnk@p200300d6e71c4f996d25e8a80f1711a4.dip0.t-ipconnect.de) (Read error: Connection reset by peer)
2025-04-10 03:26:27 +0200foul_owl(~kerry@174-21-146-90.tukw.qwest.net) (Ping timeout: 265 seconds)
2025-04-10 03:27:06 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 03:28:54 +0200ezzieygu1wuf(~Unknown@user/ezzieyguywuf) (Ping timeout: 246 seconds)
2025-04-10 03:30:39 +0200aforemny_(~aforemny@i59F4C56B.versanet.de) (Ping timeout: 244 seconds)
2025-04-10 03:31:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Ping timeout: 264 seconds)
2025-04-10 03:32:00 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 03:32:37 +0200 <EvanR> in the law: if x == y then f x == f y, (congruence), would you say "== preserves function application" or "function application preserves ==" and/or what is the congruence, == or function application
2025-04-10 03:36:18 +0200Square(~Square4@user/square) Square
2025-04-10 03:37:13 +0200weary-traveler(~user@user/user363627) (Quit: Konversation terminated!)
2025-04-10 03:37:29 +0200weary-traveler(~user@user/user363627) user363627
2025-04-10 03:39:08 +0200Square2(~Square@user/square) (Ping timeout: 245 seconds)
2025-04-10 03:40:19 +0200foul_owl(~kerry@94.156.149.91) foul_owl
2025-04-10 03:42:54 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 03:47:39 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 03:50:08 +0200aforemny(~aforemny@i59F4C778.versanet.de) aforemny
2025-04-10 03:50:13 +0200xff0x(~xff0x@fsb6a9491c.tkyc517.ap.nuro.jp)
2025-04-10 03:58:42 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:03:27 +0200 <haskellbridge> <Bowuigi> EvanR in HoTT the unit type is denoted as mathbb{1} and its inhabitant is denoted * (or with a star)
2025-04-10 04:03:43 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 244 seconds)
2025-04-10 04:04:28 +0200 <haskellbridge> <Bowuigi> If you want something convention independent just ask for the limit/adjunction version of those constructs
2025-04-10 04:05:18 +0200tessier(~tessier@ip68-8-117-219.sd.sd.cox.net) (Ping timeout: 272 seconds)
2025-04-10 04:05:30 +0200 <EvanR> yes I saw that in HoTT
2025-04-10 04:06:26 +0200tessier(~tessier@ec2-184-72-149-67.compute-1.amazonaws.com) tessier
2025-04-10 04:06:47 +0200 <haskellbridge> <Bowuigi> Also the product type is only associative up to isomorphism, members of (AxB)xC and members of Ax(BxC) are not equal, just equivalent (except under univalence)
2025-04-10 04:06:55 +0200 <EvanR> 𝟙
2025-04-10 04:08:13 +0200 <haskellbridge> <Bowuigi> Yes, the boolean type is mathbb{2} and in general any type with exactly N elements is denoted mathbb{N}
2025-04-10 04:14:26 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:16:32 +0200slack1256(~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) slack1256
2025-04-10 04:16:48 +0200tavare(~tavare@user/tavare) (Remote host closed the connection)
2025-04-10 04:17:51 +0200 <slack1256> Has anyone used tsvector in persistent ?
2025-04-10 04:17:58 +0200 <slack1256> How do you declare in as a datatype?
2025-04-10 04:18:50 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 04:21:00 +0200ryanbooker(uid4340@id-4340.hampstead.irccloud.com) ryanbooker
2025-04-10 04:24:54 +0200TheCoffeMaker(~TheCoffeM@user/thecoffemaker) (Ping timeout: 276 seconds)
2025-04-10 04:26:49 +0200 <monochrom> EvanR: Interesting, I have always thought of it as == preserves function application, but the other round is just as valid.
2025-04-10 04:26:54 +0200TheCoffeMaker(~TheCoffeM@user/thecoffemaker) TheCoffeMaker
2025-04-10 04:29:48 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:29:57 +0200j1n37(~j1n37@user/j1n37) j1n37
2025-04-10 04:31:13 +0200j1n37-(~j1n37@user/j1n37) (Ping timeout: 265 seconds)
2025-04-10 04:34:06 +0200stef204(~stef204@user/stef204) (Quit: WeeChat 4.2.1)
2025-04-10 04:35:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 272 seconds)
2025-04-10 04:37:02 +0200slack1256(~slack1256@2803:c600:5111:9ab8:7184:9cb0:2874:e233) (Remote host closed the connection)
2025-04-10 04:45:34 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 04:46:14 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca) (Ping timeout: 260 seconds)
2025-04-10 04:47:39 +0200 <EvanR> I got that off stanford.edu on the topic of lambda calculus
2025-04-10 04:48:03 +0200 <EvanR> where it describes eta conversion as "= preserving application and abstraction"
2025-04-10 04:50:29 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 05:01:22 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:06:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds)
2025-04-10 05:17:07 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:18:10 +0200tamer(~tamer@user/tamer) (Read error: Connection reset by peer)
2025-04-10 05:22:24 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 05:32:23 +0200hattckory(~hattckory@bras-base-toroon4524w-grc-30-70-27-118-207.dsl.bell.ca)
2025-04-10 05:32:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:34:23 +0200 <haskellbridge> <Liamzee> curious, have people built a linear lens system for vector yet? IIRC, there was something about that on Bartosz Milewski's site
2025-04-10 05:34:25 +0200 <haskellbridge> <Liamzee> https://bartoszmilewski.com/2024/02/07/linear-lenses-in-haskell/
2025-04-10 05:34:29 +0200tamer(~tamer@5.2.74.82)
2025-04-10 05:37:53 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds)
2025-04-10 05:41:02 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 05:48:38 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 05:50:14 +0200zlqrvx_(~zlqrvx@101.175.150.247)
2025-04-10 05:51:15 +0200zlqrvx(~zlqrvx@101.175.150.247) (Read error: Connection reset by peer)
2025-04-10 05:54:04 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 260 seconds)
2025-04-10 05:57:56 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich
2025-04-10 06:01:16 +0200bitdex_(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 06:01:24 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-04-10 06:04:03 +0200whez(uid470288@id-470288.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2025-04-10 06:04:27 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:09:08 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds)
2025-04-10 06:09:14 +0200peterbecich(~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds)
2025-04-10 06:10:50 +0200 <ski> EvanR : "`f' preserves equality" (i'd say `=', unless you specifically mean decidable equality) (and it's not "function application" but "(function appliation of) `f'"). `(==)' would be the congruence relation (wrt `f') here
2025-04-10 06:12:26 +0200michalz(~michalz@185.246.207.201)
2025-04-10 06:20:15 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn
2025-04-10 06:23:05 +0200bitdex_(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2025-04-10 06:23:28 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) bitdex
2025-04-10 06:25:18 +0200merijn(~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 268 seconds)