/home/laney/.irssi/irclogs/Freenode/#agda.log-20170325

--- Day changed Fri Mar 24 2017
akr[m]glguy: I know, I was just thinking that this bight be more elegant with the use of sized types :)24/03 07:22
akr[m]I mean, I could just use ℕ as the size I think24/03 07:25
arjen-jonathanHi all24/03 13:00
arjen-jonathanI broke agda again24/03 13:01
arjen-jonathan:(24/03 13:01
arjen-jonathanAlso, the gmain link in the title is dead24/03 13:02
Saizanarjen-jonathan: i.e. you proved false?24/03 13:06
arjen-jonathanNo, it's not *that* broken24/03 13:08
arjen-jonathanTypechecker loops24/03 13:08
arjen-jonathanIt seems24/03 13:08
arjen-jonathanYou're working on parametricity?24/03 13:11
Saizanyep24/03 13:14
arjen-jonathanThat's awesome. How's it going?24/03 13:16
Saizanso far it can be used for some irrelevance properties, but general "free theorems" are a bit limited by how we cannot have parametricity proofs about parametricity proofs24/03 13:19
Saizanit's been challenging to find the right denotational model24/03 13:19
Saizanand we might have to modify it again24/03 13:20
arjen-jonathanAre you publishing on this topic?24/03 13:24
Saizanwe have a draft, pm me an address and I can mail it to you24/03 13:25
dolioakr[m]: I think I'm wrong, and Saizan is right. Nat is isomorphic to coNat in the classical set model. But that isomorphism can't be continuous with respect to the 'computability topology.'24/03 14:35
akr[m]I'm not sure what that means; to me it seems that the classical isomorphism is not a computable function24/03 14:37
dolioYes, that's what it means.24/03 14:37
dolioThere are some fixed points where least coinciding with greatest will provably not work.24/03 14:39
dolioLike, fixed point of identity.24/03 14:39
dolioLeast is empty set, greatest is singleton set.24/03 14:39
akr[m]I'm not sure what's our function space when talking about fixed points here24/03 14:41
dolioSomething like covariant functors.24/03 14:44
dolioAt least for sets.24/03 14:45
Saizanyeah, it feels weird, but in the end it's just that they are both countable sets24/03 14:51
dolioWell, I wasn't exactly sure that it wouldn't end up bigger than that.24/03 15:05
dolioBecause I think there could be some sets in the classical set model that aren't countable.24/03 15:05
dolioThe question is whether you could somehow use those to construct 'longer' stepping sequences or something.24/03 15:06
dolioAnd not just produce them, but produce enough that there are uncountably many things in the final coalgebra.24/03 15:07
Saizanis there an easy way to characterize which functors have isomorphic initial/final (co)algebras?24/03 15:40
Saizanmaybe all finitary-branching functors have isomorphic initial/final (co)algebras if those are both infinite24/03 15:40
Saizanbecause it only takes induction over omega to build both24/03 15:40
dolioHow branching is id?24/03 15:41
Saizanthe initial algebra of id is not infinite :)24/03 15:42
dolioOh, if infinite.24/03 15:42
dolioI don't think that works.24/03 15:44
dolioLike, finite bit sequences is not going to be isomorphic to potentially infinite bit sequences, classically.24/03 15:44
dolioThere are too many of the latter, right?24/03 15:44
dolioUncountably many infinite ones.24/03 15:45
Saizanuh, right24/03 15:46
Saizanok, now i'm also more surprised by conat being countable24/03 15:48
dolioWell, the difference there is that the uncountable bit sequences all have the same length.24/03 15:48
dolioBut they have different content.24/03 15:48
dolioBut (co)naturals have no content other than length.24/03 15:49
Saizanmakes sense, everything that makes that set big is actually collapsed into the "infinity" element in (co)naturals24/03 15:51
dolioRight. The uncountably many things get quotiented down to a single thing. :)24/03 15:51
dolioAlthough I don't have a good explanation for why you can't have different infinite lengths of things.24/03 15:52
dolioOther than that bisimulation is defined in terms of the naturals.24/03 15:53
dolioInstead of some more general thing.24/03 15:53
dolioLike how mathematicians move from natural-indexed sequences to filters for some things in topology, because the former is limiting.24/03 15:54
dolioOr how 'directed sets' are more general than omega chains.24/03 15:55
Saizanmy rough understanding is that it depends on the functor, but a lot of them commute with limits over the naturals, so longer chains would still reach the same fixed point24/03 15:58
dolioAh.24/03 15:58
akr[m]Given a list of values, I want to construct the type of these values24/03 16:37
akr[m]is there something better I can do than dependent products?24/03 16:37
akr[m](avoiding metaprogramming)24/03 16:37
akr[m]maybe avoiding lists altogether, hmm24/03 16:39
akr[m]my situation is like this: http://lpaste.net/35389524/03 16:44
akr[m]Atomic is something which is defined by the type of states it can be in24/03 16:44
akr[m]Struct is determined by the Atomics it is made up of24/03 16:44
akr[m]and I'd like to have something like Signature, which is the type of atomics some given struct is made of24/03 16:45
mietekSaizan: what’s the status of Agda/cubical? https://github.com/agda/agda/issues/170324/03 22:30

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!