Nik05 Nik05 --- Day changed Fri Jan 12 2018 pgiarrusso: just found out stdlib already has my definitions in Relation.Unary 12/01 09:49 Pred is my S except that you can can give another set level, why would you want this? 12/01 09:50 I've been searching for this Autoquote library mentioned in "Engineering Proof by Reflection in Agda" but I can't find it 12/01 10:14 how do i make sure something isnt normalised? 12/01 11:58 Nik05 : What do you mean? 12/01 12:30 http://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html#keybindings 12/01 12:33 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 Nik05 : Cntr-u : Check the emacs keybindings. 12/01 13:13 oh its that easy thank you apostolis 12/01 13:21 sorry tottally missed that 12/01 13:23 apostolis but still it doesnt behave as i would like. A \x B is printed as \Sigma A (const B) 12/01 13:26 also with C-u 12/01 13:27 Nik05: 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 pragma 12/01 13:45 Nik05 Nik05: since you asked about the extra level in Relation.Unary’s Pred: 12/01 13:48 that‘s needed for predicates on A that don’t fit in A’s level 12/01 13:48 I defined A \x B = \Sigma A (const B) 12/01 13:49 uh, strange 12/01 13:49 on 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 oh oke 12/01 13:51 Nik05: wait, which keybinding are you prepending C-u to? 12/01 13:52 Nik05 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 else 12/01 13:54 (and it normalizes even more) 12/01 13:55 C-u C-C C-, i was using 12/01 14:00 is there a difference between \all and \lambda? 12/01 14:13 was using them as synonyms... 12/01 14:13 Nik05 that keybinding looks right, confusing 12/01 14:24 Nik05: forall and \lambda are different, yes 12/01 14:24 the type of \lambda x: T. t is \forall x: T. U (where U is t’s type) 12/01 14:25 Nik05: ^^ 12/01 14:25 let me unmagic that :P 12/01 14:27 thank you pgiarrusso 12/01 14:36 hi, I'm currently visiting an algebra lecture, and I'm trying to see how a few of the group theory proofs look in Agda 12/01 19:57 how would you model the concept of a subgroup in Agda? 12/01 19:57 My idea was G is a subgroup of H, iff G and H are both groups and there is an injective function from G to H 12/01 19:58 but I'm not sure if this would be a correct definition 12/01 20:00 or probably rather an injective group-homomorphism from G to H 12/01 20:01 I 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 types 12/01 20:05 m0rphism: you might want to use a characteristic predicate on G’s domain 12/01 20:33 Using 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 now 12/01 20:34 (Also, subobject are more complex, and doing CT in Agda or Coq is pretty hard even for experts) 12/01 20:35 So characteristic predicates are the standard encoding 12/01 20:35 morphism: ^^ 12/01 20:35 * m0rphism : ^^ 12/01 20:36 Conveniently, Nik05 asked tons of questions on Pred in Relation.Unary just now 12/01 20:36 m0rphism: correction on CT: subobjects would indeed translate to injective *homomorphisms*, so CT validates your guess 12/01 20:38 pgiarrusso: Nice, thanks for the info! 12/01 20:40 so if I understand you correctly, then both injective homomorphisms and and characteristic predicates should work 12/01 20:42 (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-nat 12/01 20:44