--- Day changed Thu Mar 23 2017 | ||

gallais | akr[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 proceed | 23/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 same | 23/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 before | 23/03 07:34 |

akr[m] | to be honest, I'm not sure what exactly does ℕ ≡ coℕ actually say | 23/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 Agda | 23/03 07:36 |

gallais | Via subst, I think that saying they are equal does give you an iso | 23/03 07:38 |

gallais | I guess one way of dealing with this is deriving decidability of equality on coN from the one of N + the iso | 23/03 07:39 |

gallais | And 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] | interesting | 23/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 |

gallais | I 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 cardinals | 23/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 theory | 23/03 10:29 |

akr[m] | so I have no idea what I'm talking about :) | 23/03 10:29 |

aochagavia | I 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 it | 23/03 10:52 |

aochagavia | the code is on https://gist.github.com/aochagavia/82a731dcecd0e9b9ba11af517ec3a889 | 23/03 10:52 |

aochagavia | any ideas? | 23/03 10:52 |

Saizan | aochagavia: try List.Cons instead of Cons | 23/03 11:06 |

aochagavia | it works! | 23/03 11:06 |

aochagavia | :D | 23/03 11:06 |

aochagavia | so 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 do | 23/03 12:03 |

Saizan | gone but, the problem was that Cons is overloaded (somewhere else) and Agda wasn't able to disambiguate | 23/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 number | 23/03 12:04 |

akr[m] | as they can't recurse | 23/03 12:04 |

akr[m] | e.g. https://gist.github.com/osense/ec9b4740e025a70c9e87c35be99b592a#file-conat-agda-L65 | 23/03 12:04 |

Saizan | akr[m]: they have to be constant at some point, not necessarily zero though | 23/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-inject | 23/03 12:06 |

Saizan | mh, tbh, in a classical set model, conat is just 1 + Nat, which is indeed isomorphic to Nat, iiuc | 23/03 12:09 |

Saizan | so i don't know if you can internally prove they are distinct | 23/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] | hmm | 23/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 |

gallais | The 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 ≢ B | 23/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/353858 | 23/03 12:31 |

akr[m] | nice :) | 23/03 12:34 |

Saizan | is argh disprovable though? | 23/03 14:11 |

gallais | I don't think so. | 23/03 14:18 |

gallais | It's more that, combined with the halting problem, the ability to test whether a conat is omega seems scary | 23/03 14:19 |

gallais | but depending on the formulation of the HP that's provable, we may still not be able to extract a proof of false from tis | 23/03 14:21 |

gallais | this* | 23/03 14:21 |

dolio | You'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 |

dolio | At least, I think you will. | 23/03 17:41 |

dolio | Or even isomorphic. | 23/03 17:42 |

dolio | That 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 |

dolio | So I'm not sure conat will end up as 1 + Nat in a cllasical set model. | 23/03 17:46 |

dolio | Also, 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 -> B | 23/03 17:51 |

dolio | I don't know if you can prove enough about what it does for it to be a problem. | 23/03 18:02 |

dolio | If you can prove that 'hylo f g = g . map (hylo f g) . f' that's probably bad, though. | 23/03 18:03 |

dolio | Because then hylo right g x = g (right (hylo right g x)) | 23/03 18:05 |

mietek | Failed to solve the following constraints: | 23/03 19:36 |

mietek | Is not empty type of sizes: (.w′ ⊩⋆ _Γ_494 p d γ) | 23/03 19:36 |

mietek | What does that mean? | 23/03 19:36 |

mietek | "type of sizes"? | 23/03 19:36 |

mietek | Not using sized types | 23/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 once | 23/03 21:30 |

akr[m] | so that a and b[0] are valid values, but c[0][1] is not | 23/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 thing | 23/03 21:34 |

akr[m] | can* | 23/03 21:35 |

glguy | akr[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!