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

--- Day changed Thu Mar 23 2017
gallaisakr[m]: this seems like a really hard problem. The two don't have the same cardinal so there is hope but I have no idea how to proceed23/03 01:03
akr[m]gallais: can I talk about their cardinals in Agda somehow? maybe we could have a lemma that two things with different cardinals are not the same23/03 07:29
akr[m]also, are there some non-trivial examples of proofs of two types not being the same? I haven't seen anyone do something like t his before23/03 07:34
akr[m]to be honest, I'm not sure what exactly does ℕ ≡ coℕ actually say23/03 07:35
akr[m]I think it might be easier to prove that they are not isomorphic, but I'm not sure whether or not that's the same as ≡ in Agda23/03 07:36
gallaisVia subst, I think that saying they are equal does give you an iso23/03 07:38
gallaisI guess one way of dealing with this is deriving decidability of equality on coN from the one of N + the iso23/03 07:39
gallaisAnd you can then solve the halting problem (but it'd require a lot of work to formally derive a contradiction from that)23/03 07:39
akr[m]interesting23/03 07:43
akr[m]so has no one formalized that in Agda before?23/03 07:43
akr[m](halting problem etc.)23/03 07:43
gallaisI don't know.23/03 07:48
akr[m]thank you, I have to catch a class now :)23/03 07:51
akr[m]gallais: what about my question about cardinals? has anyone succeeded in formalizing that in Agda?23/03 10:17
akr[m](e.g. having a function which to at least each type in the first universe assigns a  cardinal or something like that)23/03 10:17
akr[m]or in MLTT even; I know that MLTT can express some fairly large cardinals23/03 10:18
akr[m](I guess my last remark is rather pointless; the maximum cardinality of any type that a theory is able to express would have to be the same as the largest cardinal it can express)23/03 10:24
akr[m](though I don't know whether we can get maximum cardinality already in the first universe)23/03 10:24
akr[m]hmm okay it seems that cardinals in constructive mathematics behave somewhat differently than in classical set theory23/03 10:29
akr[m]so I have no idea what I'm talking about :)23/03 10:29
aochagaviaI have a problem with a small proof... Some parts of it are being highlighted in yellow by Emacs and I don't know how to solve it23/03 10:52
aochagaviathe code is on https://gist.github.com/aochagavia/82a731dcecd0e9b9ba11af517ec3a88923/03 10:52
aochagaviaany ideas?23/03 10:52
Saizanaochagavia: try List.Cons instead of Cons23/03 11:06
aochagaviait works!23/03 11:06
aochagavia:D23/03 11:06
aochagaviaso the problem was that Agda was unable to infer a suitable type?23/03 11:07
akr[m]gallais: I'm thinking about what can functions from coℕ to ℕ actually do23/03 12:03
Saizangone but, the problem was that Cons is overloaded (somewhere else) and Agda wasn't able to disambiguate23/03 12:03
akr[m]it seems to me that they have to infect unify infinitely many elements: they map cozero to some natural number, but then they have to send all the other conats to same other number23/03 12:04
akr[m]as they can't recurse23/03 12:04
akr[m]e.g. https://gist.github.com/osense/ec9b4740e025a70c9e87c35be99b592a#file-conat-agda-L6523/03 12:04
Saizanakr[m]: they have to be constant at some point, not necessarily zero though23/03 12:04
akr[m]ok, so they can distinguish finitely many elements, but at some point they have to map everything to the same natural?23/03 12:05
akr[m]how can I use that in the proof of cant-inject23/03 12:06
Saizanmh, tbh, in a classical set model, conat is just 1 + Nat, which is indeed isomorphic to Nat, iiuc23/03 12:09
Saizanso i don't know if you can internally prove they are distinct23/03 12:09
akr[m]but it should at least be true that there is no injection, at the very least?23/03 12:10
akr[m]I mean, provable :)23/03 12:10
akr[m]hmm23/03 12:11
akr[m]I think classically you can send ω to zero and then co0 to 1, co1 to 2 etc.23/03 12:12
gallaisThe problem is that a lot of these results are meta-results. You don't have access to them from inside the theory.23/03 12:15
akr[m]hmm, this was easy:23/03 12:16
akr[m]no-inject-means-not-same : {A B : Set} → ¬ (Σ[ f ∈ (A → B) ] (injective f)) → A ≢ B23/03 12:16
akr[m]no-inject-means-not-same no-inj refl = no-inj ( id , λ x y z → z)23/03 12:16
akr[m]what results do you mean, specifically?23/03 12:17
lpaste_gallais pasted “eqdec_omega” at http://lpaste.net/35385823/03 12:31
akr[m]nice :)23/03 12:34
Saizanis argh disprovable though?23/03 14:11
gallaisI don't think so.23/03 14:18
gallaisIt's more that, combined with the halting problem, the ability to test whether a conat is omega seems scary23/03 14:19
gallaisbut depending on the formulation of the HP that's provable, we may still not be able to extract a proof of false from tis23/03 14:21
gallaisthis*23/03 14:21
dolioYou're going to get into trouble in a set theoretic model by saying that the least fixed point of 1+ is identical to the greatest fixed point.23/03 17:40
dolioAt least, I think you will.23/03 17:41
dolioOr even isomorphic.23/03 17:42
dolioThat sort of thing is the defining characteristic of non-total theories.23/03 17:42
dolio(When it occurs for all fixed points, that is.)23/03 17:43
dolioSo I'm not sure conat will end up as 1 + Nat in a cllasical set model.23/03 17:46
dolioAlso, since conat is the final coalgebra, and nat is the initial algebra, you should be able to use your equivalence between them to write: hylo : (A -> 1 + A) -> (1 + B -> B) -> A -> B23/03 17:51
dolioI don't know if you can prove enough about what it does for it to be a problem.23/03 18:02
dolioIf you can prove that 'hylo f g = g . map (hylo f g) . f' that's probably bad, though.23/03 18:03
dolioBecause then hylo right g x = g (right (hylo right g x))23/03 18:05
mietekFailed to solve the following constraints:23/03 19:36
mietek  Is not empty type of sizes: (.w′ ⊩⋆ _Γ_494 p d γ)23/03 19:36
mietekWhat does that mean?23/03 19:36
mietek"type of sizes"?23/03 19:36
mietekNot using sized types23/03 19:36
akr[m]Hmm, I thought I could use sized types to define a type T which has nullary constructors (say, a b c : T), and then a binary constructor (say, [] : T → ℕ → T) which can only be applied once23/03 21:30
akr[m]so that a and b[0] are valid values, but c[0][1] is not23/03 21:30
akr[m]but it doesn't look like sized types have the concept of "zero"?23/03 21:31
akr[m]dolio: what you're saying is interesting, but I don't know enough to construct a meaningful reply :)23/03 21:34
akr[m]it seems that I've once again managed to open a con of worms that is beyond my understanding with the whole nat - conat thing23/03 21:34
akr[m]can*23/03 21:35
glguyakr[m]: You can do that; you don't need "sized typed".23/03 22:35

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