--- Day changed Sat Jan 13 2018 | ||

tomjack | Does "characteristic predicate" mean A -> Set? | 13/01 03:11 |
---|---|---|

tomjack | It is strange... Under the relationship (isomorphism up to isomorphism) between families of sets and sets with maps, the injectivity of a map corresponds to (x : A) (u v : P x) -> u = v for a family. Will we see this requirement in a vanilla Agda definition of subgroups using families? | 13/01 03:17 |

tomjack | I guess we will just let the setoid relation on Σ A P be trivial on P | 13/01 04:09 |

pgiarrusso | m0rphism: injective homomorphisms aren’t the whole story. Category theorists quotient isomorphic subobjects together, and quotients are hard to express in type theory (though you can use setoids), so I guess I don’t recommend this road for this goal. | 13/01 09:09 |

pgiarrusso | m0rphism: still, it is a good idea to have | 13/01 09:10 |

pgiarrusso | tomjack: m0rphism the type of characteristic predicates on A is indeed A -> Set, because propositions are types and have type Set in Agda | 13/01 09:11 |

pgiarrusso | tomjack: on the rest, it seems you’re trying to verify that characteristic predicates do induce subobjects, but you don’t say so | 13/01 09:22 |

pgiarrusso | I never claimed the two definitions are equivalent and they aren’t | 13/01 09:22 |

pgiarrusso | subobjects are more general | 13/01 09:22 |

pgiarrusso | Nevertheless, what you got is a form of proof irrelevance | 13/01 09:22 |

pgiarrusso | And at least a category theorist might believe the definition of subobjects is sufficient reason to impose this requirement even when just considering characteristic predicates | 13/01 09:23 |

pgiarrusso | One might instead wait till this proof irrelevance is needed before imposing it | 13/01 09:24 |

pgiarrusso | tomjack: you might need this proof irrelevance when you try to prove equalities on Σ A P, but I’m not sure if and where it’s needed; OTOH, in classical math you do have proof irrelevance, so it’s probably a good idea | 13/01 09:26 |

trikl[m] | Agda 2.4.2 had a function `type : Name -> Type` that given a quoted term in context produced the type of it. As far as I'm aware this has been replaced by `getType : Name -> TC Type` in 2.5.3. If I understood correctly, `unquote` can be used to make the typechecker execute a `TC` computation, but I haven't discovered how to put these two things together. Can anyone clarify? | 13/01 10:01 |

mietek | effectfully ^^ | 13/01 11:54 |

m0rphism | pgiarrusso: Thanks again for the pointers; they are very much appreciated! I'm not yet at the point where I understand everything in detail, but most concepts still ring a bell, so it's good to have those associations. I will definetly have a look at sub-objects and setoids, when I find time. | 13/01 12:09 |

trikl[m] | mietek: So the docs say that `unquote m` has type `A` where `m : Term -> TC T` | 13/01 12:11 |

trikl[m] | From that I understand there's a way of getting out of the `TC` monad? | 13/01 12:11 |

m0rphism | I guess studying setoids should also help to get a better grasp of the Agda "stdlib" where I remember having seen this concept before. | 13/01 12:11 |

mietek | I haven’t used `TC` | 13/01 12:12 |

trikl[m] | I'm trying to make the little autoquote library in https://github.com/toothbrush/reflection-proofs work with Agda 2.5.3 | 13/01 12:13 |

pgiarrusso | m0rphism: yes, setoids are one standard replacement type theory offers for quotients, since they're hard to define | 13/01 12:15 |

trikl[m] | I might have better luck by contacting the author | 13/01 12:15 |

m0rphism | I'm currently looking into type classes in Agda beyond the basics mentioned on readthedocs.io. Does the paper "On the Bright Side of Type Classes: Instance Arguments in Agda" by Devriese & Piessens (ICFP 2011) still represent the current state in Agda? Apparently the concepts of the paper have been envisioned for Agda 2.2.12. | 13/01 12:50 |

mietek | m0rphism: sort of? http://agda.readthedocs.io/en/v2.5.3/language/instance-arguments.html | 13/01 12:54 |

mietek | the proof search method changed, so some old code may not work | 13/01 12:54 |

mietek | but they can still be used to implement typeclasses | 13/01 12:54 |

m0rphism | mietek: I see, thanks! | 13/01 12:57 |

pgiarrusso | m0rphism: IIRC the main change from the paper is that now instance search only considers `instance` definitions | 13/01 12:59 |

pgiarrusso | another big change is that instance search only starts for a target type that has been completely inferred, instead of having metavariables still to fill in | 13/01 13:00 |

pgiarrusso | so you don’t have anything like functional dependencies | 13/01 13:01 |

mietek | ah. | 13/01 13:01 |

mietek | I think that broke Conor’s gadget | 13/01 13:01 |

m0rphism | pgiarrusso: thanks, I'll try to keep those differences in mind while reading the paper. | 13/01 13:02 |

Nik05 | is it possible to case split a variable in a let binding? | 13/01 14:43 |

Nik05 | i tried let A = ... in (\B -> {!!}) A | 13/01 14:51 |

Nik05 | but this fails to resolve constraints | 13/01 14:51 |

Nik05 | or how would you rewrite at a random position? | 13/01 15:23 |

Nik05 | how would you structure proofs with equality in agda? | 13/01 15:47 |

Nik05 | oh just with case of | 13/01 16:26 |

Nik05 | still the question about rewriting, how can you do that? | 13/01 18:22 |

comietek | Nik05: you can declare global rewrite rules using the REWRITE pragma | 13/01 22:44 |

comietek | or, use `subst` | 13/01 22:44 |

Nik05` | Hi mietek, thank you | 13/01 22:47 |

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