--- Day changed Fri Jan 12 2018 | ||

Nik05` | pgiarrusso: just found out stdlib already has my definitions in Relation.Unary | 12/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 it | 12/01 10:14 |

Nik05 | how do i make sure something isnt normalised? | 12/01 11:58 |

apostolis | Nik05 : What do you mean? | 12/01 12:30 |

apostolis | http://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html#keybindings | 12/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 |

apostolis | Nik05` : Cntr-u : Check the emacs keybindings. | 12/01 13:13 |

Nik05 | oh its that easy thank you apostolis | 12/01 13:21 |

Nik05 | sorry tottally missed that | 12/01 13:23 |

Nik05 | apostolis but still it doesnt behave as i would like. A \x B is printed as \Sigma A (const B) | 12/01 13:26 |

Nik05 | also with C-u | 12/01 13:27 |

pgiarrusso | 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 |

pgiarrusso | Nik05` Nik05: since you asked about the extra level in Relation.Unary’s Pred: | 12/01 13:48 |

pgiarrusso | that‘s needed for predicates on A that don’t fit in A’s level | 12/01 13:48 |

Nik05 | I defined A \x B = \Sigma A (const B) | 12/01 13:49 |

pgiarrusso | uh, strange | 12/01 13:49 |

pgiarrusso | 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 |

Nik05 | oh oke | 12/01 13:51 |

pgiarrusso | Nik05: wait, which keybinding are you prepending C-u to? | 12/01 13:52 |

pgiarrusso | 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 |

pgiarrusso | (and it normalizes even more) | 12/01 13:55 |

Nik05 | C-u C-C C-, i was using | 12/01 14:00 |

Nik05 | is there a difference between \all and \lambda? | 12/01 14:13 |

Nik05 | was using them as synonyms... | 12/01 14:13 |

pgiarrusso | Nik05 that keybinding looks right, confusing | 12/01 14:24 |

pgiarrusso | Nik05`: forall and \lambda are different, yes | 12/01 14:24 |

pgiarrusso | the type of \lambda x: T. t is \forall x: T. U (where `U` is `t`’s type) | 12/01 14:25 |

pgiarrusso | Nik05: ^^ | 12/01 14:25 |

Nik05 | let me unmagic that :P | 12/01 14:27 |

Nik05 | thank you pgiarrusso | 12/01 14:36 |

m0rphism | 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 |

m0rphism | how would you model the concept of a subgroup in Agda? | 12/01 19:57 |

m0rphism | 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 |

m0rphism | but I'm not sure if this would be a correct definition | 12/01 20:00 |

m0rphism | or probably rather an injective group-homomorphism from G to H | 12/01 20:01 |

m0rphism | 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 |

pgiarrusso | m0rphism: you might want to use a characteristic predicate on G’s domain | 12/01 20:33 |

pgiarrusso | 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 |

pgiarrusso | (Also, subobject are more complex, and doing CT in Agda or Coq is pretty hard even for experts) | 12/01 20:35 |

pgiarrusso | So characteristic predicates are the standard encoding | 12/01 20:35 |

pgiarrusso | morphism: ^^ | 12/01 20:35 |

pgiarrusso | * m0rphism : ^^ | 12/01 20:36 |

pgiarrusso | Conveniently, Nik05 asked tons of questions on Pred in Relation.Unary just now | 12/01 20:36 |

pgiarrusso | m0rphism: correction on CT: subobjects would indeed translate to injective *homomorphisms*, so CT validates your guess | 12/01 20:38 |

m0rphism | pgiarrusso: Nice, thanks for the info! | 12/01 20:40 |

m0rphism | so if I understand you correctly, then both injective homomorphisms and and characteristic predicates should work | 12/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-nat | 12/01 20:44 |

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