--- Day changed Fri Jan 12 2018
Nik05`pgiarrusso: just found out stdlib already has my definitions in Relation.Unary12/01 09:49
Nik05`Pred is my S except that you can can give another set level, why would you want this?12/01 09:50
trikl[m]I've been searching for this Autoquote library mentioned in "Engineering Proof by Reflection in Agda" but I can't find it12/01 10:14
Nik05how do i make sure something isnt normalised?12/01 11:58
apostolisNik05 : What do you mean?12/01 12:30
apostolishttp://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html#keybindings12/01 12:33
Nik05`apostolis: hi I got a definition of Set almost equal to that of Pred in Relation.Unary when in agda mode set gets normalised to A -> Set _ but I would like to keep my set definition there. In coq you can fold or not use unfold. But how would you do that in agfa?12/01 12:34
apostolisNik05` : Cntr-u : Check the emacs keybindings.12/01 13:13
Nik05oh its that easy thank you apostolis 12/01 13:21
Nik05sorry tottally missed that12/01 13:23
Nik05apostolis but still it doesnt behave as i would like. A \x B is printed as \Sigma A (const B) 12/01 13:26
Nik05also with C-u12/01 13:27
pgiarrussoNik05: any chance you have a non-standard \x that’s just a syntax abbreviation (which would be silly, but...)? Because that’s inlined on parsing. In that case you might need a DISPLAY pragma12/01 13:45
pgiarrussoNik05` Nik05: since you asked about the extra level in Relation.Unary’s Pred:12/01 13:48
pgiarrussothat‘s needed for predicates on A that don’t fit in A’s level12/01 13:48
Nik05I defined A \x B = \Sigma A (const B) 12/01 13:49
pgiarrussouh, strange12/01 13:49
pgiarrussoon levels: for instance, if A: Set a, forall (B: Set a). ... A ... B fits in Set (suc a), not in Set a (because Agda’s predicative)12/01 13:50
Nik05oh oke12/01 13:51
pgiarrussoNik05: wait, which keybinding are you prepending C-u to?12/01 13:52
pgiarrussoNik05 because showing a goal with `C-u C-c C-,` skips normalization (ditto with `C-u C-c C-.`), and that’s missing from those docs; while `C-u C-c C-n` does something else12/01 13:54
pgiarrusso(and it normalizes even more)12/01 13:55
Nik05C-u C-C C-, i was using12/01 14:00
Nik05is there a difference between \all and \lambda?12/01 14:13
Nik05was using them as synonyms...12/01 14:13
pgiarrussoNik05 that keybinding looks right, confusing12/01 14:24
pgiarrussoNik05`: forall and \lambda are different, yes12/01 14:24
pgiarrussothe type of \lambda x: T. t is \forall x: T. U (where `U` is `t`’s type)12/01 14:25
pgiarrussoNik05: ^^12/01 14:25
Nik05let me unmagic that :P12/01 14:27
Nik05thank you pgiarrusso 12/01 14:36
m0rphismhi, I'm currently visiting an algebra lecture, and I'm trying to see how a few of the group theory proofs look in Agda12/01 19:57
m0rphismhow would you model the concept of a subgroup in Agda?12/01 19:57
m0rphismMy idea was G is a subgroup of H, iff G and H are both groups and there is an injective function from G to H12/01 19:58
m0rphismbut I'm not sure if this would be a correct definition12/01 20:00
m0rphismor probably rather an injective group-homomorphism from G to H12/01 20:01
m0rphismI guess the problem is, that I don't know how to translate the `G \subset H` restriction to Agda, now that the sets G and H have become types12/01 20:05
pgiarrussom0rphism: you might want to use a characteristic predicate on G’s domain12/01 20:33
pgiarrussoUsing injective function can also work but it gives a *different* definition; that way lies the concept of subobject in category theory, but that would be a distraction for now12/01 20:34
pgiarrusso(Also, subobject are more complex, and doing CT in Agda or Coq is pretty hard even for experts)12/01 20:35
pgiarrussoSo characteristic predicates are the standard encoding12/01 20:35
pgiarrussomorphism: ^^12/01 20:35
pgiarrusso* m0rphism : ^^12/01 20:36
pgiarrussoConveniently, Nik05 asked tons of questions on Pred in Relation.Unary just now12/01 20:36
pgiarrussom0rphism: correction on CT: subobjects would indeed translate to injective *homomorphisms*, so CT validates your guess12/01 20:38
m0rphismpgiarrusso: Nice, thanks for the info!12/01 20:40
m0rphismso if I understand you correctly, then both injective homomorphisms and and characteristic predicates should work12/01 20:42
srpx(cross-posting from #Idris) Hello! Would love some input on this quetion: https://stackoverflow.com/questions/48233736/is-it-possible-to-derive-induction-for-the-church-encoded-nat12/01 20:44

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