--- Day changed Sat Jan 13 2018
tomjackDoes "characteristic predicate" mean A -> Set?13/01 03:11
tomjackIt 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
tomjackI guess we will just let the setoid relation on Σ A P be trivial on P13/01 04:09
pgiarrussom0rphism: 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
pgiarrussom0rphism: still, it is a good idea to have13/01 09:10
pgiarrussotomjack: m0rphism  the type of characteristic predicates on A is indeed A -> Set, because propositions are types and have type Set in Agda13/01 09:11
pgiarrussotomjack: on the rest, it seems you’re trying to verify that characteristic predicates do induce subobjects, but you don’t say so13/01 09:22
pgiarrussoI never claimed the two definitions are equivalent and they aren’t13/01 09:22
pgiarrussosubobjects are more general13/01 09:22
pgiarrussoNevertheless, what you got is a form of proof irrelevance13/01 09:22
pgiarrussoAnd at least a category theorist might believe the definition of subobjects is sufficient reason to impose this requirement even when just considering characteristic predicates13/01 09:23
pgiarrussoOne might instead wait till this proof irrelevance is needed before imposing it13/01 09:24
pgiarrussotomjack: 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 idea13/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
mietekeffectfully ^^13/01 11:54
m0rphismpgiarrusso: 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
m0rphismI 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
mietekI 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.313/01 12:13
pgiarrussom0rphism: yes, setoids are one standard replacement type theory offers for quotients, since they're hard to define13/01 12:15
trikl[m]I might have better luck by contacting the author13/01 12:15
m0rphismI'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
mietekm0rphism: sort of? http://agda.readthedocs.io/en/v2.5.3/language/instance-arguments.html13/01 12:54
mietekthe proof search method changed, so some old code may not work13/01 12:54
mietekbut they can still be used to implement typeclasses13/01 12:54
m0rphismmietek: I see, thanks!13/01 12:57
pgiarrussom0rphism: IIRC the main change from the paper is that now instance search only considers `instance` definitions13/01 12:59
pgiarrussoanother big change is that instance search only starts for a target type that has been completely inferred, instead of having metavariables still to fill in13/01 13:00
pgiarrussoso you don’t have anything like functional dependencies13/01 13:01
mietekah.13/01 13:01
mietekI think that broke Conor’s gadget13/01 13:01
m0rphismpgiarrusso: thanks, I'll try to keep those differences in mind while reading the paper.13/01 13:02
Nik05is it possible to case split a variable in a let binding?13/01 14:43
Nik05i tried let A = ... in (\B -> {!!}) A13/01 14:51
Nik05but this fails to resolve constraints13/01 14:51
Nik05or how would you rewrite at a random position?13/01 15:23
Nik05how would you structure proofs with equality in agda?13/01 15:47
Nik05oh just with case of13/01 16:26
Nik05still the question about rewriting, how can you do that?13/01 18:22
comietekNik05: you can declare global rewrite rules using the REWRITE pragma13/01 22:44
comietekor, use `subst`13/01 22:44
Nik05`Hi mietek, thank you13/01 22:47

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