--- Day changed Fri Jan 27 2017 | ||

glguy | I was playing with Agda to check my solutions to To Mock a Mockingbird. I wanted to generate a set of birds to show that there existed some birds that satisfied one property but not another. To do that I had to show that my composition operation matched my application one, which was a boring elaboration of cases (like 20 cases each with just refl). I made a macro for automating that. I thought someone might find it neat: | 27/01 05:32 |
---|---|---|

glguy | https://glguy.net/mockingbird-html/Dark-forest.html | 27/01 05:32 |

glguy | check : ∀ X Y Z → (X ∘ Y) ∙ Z ≡ X ∙ (Y ∙ Z); check = by-cases | 27/01 05:32 |

mietek | glguy: I’m boggling at ByCases | 27/01 09:11 |

mietek | {AS}, tomjack: ^^ | 27/01 09:11 |

tomjack | boggling? | 27/01 09:12 |

mietek | I am finding it neat | 27/01 09:13 |

{AS} | It does look neat :) | 27/01 09:13 |

mietek | If only we could be sure that Agda’s reflection is actually justified | 27/01 09:14 |

{AS} | mietek: transaltion validation? ;) | 27/01 09:15 |

jbracker | Can somebody tell me why http://pastebin.com/4Yz1Ntzu produces the given error and how I can fix it? I get that "SubHom a b f" has type "Set (lsuc l_1)" but why does agda insist it need be of type "Set l_1"? | 27/01 11:44 |

jbracker | I have tried to give the definition of Subcategory the type "Set (lsuc (lsuc (l_0 u l_1)))" but that does not change anything | 27/01 11:47 |

{AS} | jbracker: SubHom is not a Set | 27/01 12:25 |

{AS} | so you can't use it as a type | 27/01 12:25 |

{AS} | SubHom a b f is basically a value Hom C a b -> Exists P ((x y : P) -> x \== y) | 27/01 12:28 |

{AS} | jbracker: did you mean to define it as a type? | 27/01 12:29 |

jbracker | {AS}: Yes, I did. I got confused... Not sure how to make it a type though right now... | 27/01 13:06 |

{AS} | jbracker: I think you want something like (a b : Obj C) -> Set (lsuc \ell) | 27/01 13:07 |

{AS} | and then the body being | 27/01 13:07 |

{AS} | SubHom a b = PropSubsetOf (Hom C a b) | 27/01 13:07 |

{AS} | no? | 27/01 13:07 |

jbracker | {AS}: But then I am not modelling subsets anymore... | 27/01 13:08 |

{AS} | jbracker: huh? | 27/01 13:08 |

jbracker | because each instance of Subcategory could put whatever it wants into the Set (lsuc l_1) | 27/01 13:08 |

{AS} | jbracker: SubHom should not be a field | 27/01 13:09 |

{AS} | it should be a definition | 27/01 13:09 |

{AS} | or am I confusing something? | 27/01 13:09 |

jbracker | I think you are. SubHom needs to be a field because it defines the subset of Homomorphism to use for the subcategory and that depends on the subcategory you are looking at. I am not even convinced that you are right with SubHom a b f not being a type, because: SubHom a b f = {-some-} ProbSet = \exists (P : Set) -> ((x y : P) -> x = y). So SubHom a b f is a type. The whole thing works if you replace PropSet with Set everywhere... | 27/01 13:13 |

jbracker | If you replace PropSet in PropSubsetOf with Set then it works | 27/01 13:14 |

jbracker | but I actually want proof irrelevance so I need PropSet | 27/01 13:14 |

{AS} | jbracker: why don't you just use Agda's Proof irrelevance? :) | 27/01 13:22 |

{AS} | In any case | 27/01 13:23 |

{AS} | you can get a set if you do something like | 27/01 13:24 |

{AS} | (X : Set \ell) -> proj_1 (SubHom a b f X) | 27/01 13:25 |

{AS} | sorry | 27/01 13:28 |

{AS} | just do | 27/01 13:28 |

{AS} | (X : Hom C a b) -> proj_1 (SubHom a b f X) | 27/01 13:28 |

{AS} | or something like that | 27/01 13:28 |

jbracker | {AS}: I see. So agda problem is coming from the second part of the dependent tuple. What do you mean with Agdas proof irrelevance? I thought Prop was removed from agda and all of the proof-irrelevance functions I have seen so far a specific to certain types | 27/01 14:41 |

{AS} | jbracker: you can define an irrelevant type as follows | 27/01 14:43 |

{AS} | https://gist.github.com/ahmadsalim/3f54d833b6e23524acf60163220c818b | 27/01 14:45 |

{AS} | jbracker: ^ | 27/01 14:45 |

jbracker | How does that let you prove ((x y : A) -> x = y) ? | 27/01 14:47 |

{AS} | jbracker: irr x = irr y | 27/01 14:47 |

{AS} | you get an irrelvant injection | 27/01 14:47 |

{AS} | oh, you don't sorry | 27/01 14:49 |

jbracker | {AS}: Thats crazy, how the hell does that work? How can you get proof-irrelevance by just wrapping things up in Irr? | 27/01 14:50 |

{AS} | so in Agda writing . | 27/01 14:50 |

{AS} | means that the proof is irrelevant | 27/01 14:50 |

jbracker | pi1 : {ℓ : Level} {A : Set ℓ} → (x y : Irr A) → x ≡ y ; pi1 x y = refl | 27/01 14:50 |

{AS} | jbracker: Yeah | 27/01 14:51 |

jbracker | But me telling agda the proof is irrelevant with dot does not make it irrelevant | 27/01 14:51 |

jbracker | Like if I have 1 : Nat and 2 : Nat then Irr 1 and Irr 2 does not make 1 = 2 | 27/01 14:52 |

{AS} | jbracker: Yeah, it does not | 27/01 14:52 |

{AS} | I was wrong about that | 27/01 14:52 |

{AS} | but you can use Irr A as the irrelevant version of A :) | 27/01 14:52 |

jbracker | so how does agda decide when It it allowed to prove equality based on a given type and when not? | 27/01 14:54 |

{AS} | jbracker: what do you mean? | 27/01 14:54 |

{AS} | It checks the dots :) | 27/01 14:55 |

jbracker | {AS}: I don't get it. And experiementing with it seems to render this utterly useless. For example: p : ∀ {ℓ} {A B : Set ℓ} (x y : A ≡ B) → x ≡ y ; p x y = pi1 (irr x) (irr y) ; does not work | 27/01 14:59 |

jbracker | although it should | 27/01 14:59 |

{AS} | jbracker: I am not sure what you are showing | 27/01 15:00 |

{AS} | but by pattern matching on x and y | 27/01 15:01 |

{AS} | you should be able to prove that theorem | 27/01 15:01 |

{AS} | https://www.irccloud.com/pastebin/UMOVAgxq/ | 27/01 15:02 |

{AS} | or well, at least if you don't have --without-K on | 27/01 15:02 |

jbracker | p refl refl = pi1 (irr refl) (irr refl) ; is still rejected | 27/01 15:03 |

{AS} | jbracker: ^ | 27/01 15:03 |

{AS} | see my paste | 27/01 15:03 |

jbracker | Yes I know that that is possible | 27/01 15:03 |

{AS} | jbracker: I mean | 27/01 15:04 |

jbracker | But then I don't see how Irr could ever be useful for anything | 27/01 15:04 |

{AS} | jbracker: it gives you a version of A which has proof irrelevant members | 27/01 15:05 |

jbracker | But the members don't get irrelevant magically you just wrap them up in Irr. They are still relevant | 27/01 15:06 |

{AS} | jbracker: irr x is irrelevant for any x | 27/01 15:06 |

{AS} | x itself is still relevant yes | 27/01 15:06 |

{AS} | so irr 1 = irr 2 | 27/01 15:07 |

jbracker | So you are saying I should write: SubsetOf X = X -> Irr (Set l) instead of what I have now with PropSet? | 27/01 15:10 |

{AS} | jbracker: yeah if you want the result to be irrelevant | 27/01 15:16 |

{AS} | but notice that will give you a Set which is irrelevant | 27/01 15:17 |

{AS} | not a Set with irrelevant members | 27/01 15:17 |

{AS} | I don't think there is currently a nice way to do A -> Prop in Agda | 27/01 15:19 |

jbracker | SO I want: SubObj : (Obj C) -> Set ... ; auch that I know for all (c : Obj c) -> (q p : SubObj c) -> q ≡ p | 27/01 15:19 |

jbracker | which would be A -> Prop | 27/01 15:19 |

jbracker | *auch*such | 27/01 15:19 |

{AS} | jbracker: a simple solution would be to have | 27/01 15:20 |

{AS} | X -> Irr Y | 27/01 15:20 |

{AS} | where Y is the Set you want to be irrelevant | 27/01 15:20 |

{AS} | but yeah, it's fairly complicated | 27/01 15:21 |

{AS} | jbracker: Hmm, maybe we should just go to your original solution :) | 27/01 15:24 |

jbracker | {AS}: Ever since you pointed out that I need the projection it does not seem very appealing anymore. | 27/01 15:25 |

rribeiro | Hi all! Is there any library that provides set data structure and some theorems about it? | 27/01 16:41 |

{AS} | rribeiro: Hi! what kind of sets? | 27/01 16:43 |

{AS} | Like red-black trees, etc.? | 27/01 16:43 |

rribeiro | {AS}: yeah... Like AVL, red-black | 27/01 16:44 |

rribeiro | The standard library has AVL trees, but I do not see any theorems that could be used about them | 27/01 16:44 |

{AS} | by google I found http://www.cse.chalmers.se/~nad/repos/lib/src/Data/AVL.agda | 27/01 16:45 |

{AS} | I do not unfortunately know any myself other | 27/01 16:46 |

rribeiro | This is almost the implementation in STD library. The point is that there's no lemmas about union and other operations | 27/01 16:46 |

rribeiro | I'm asking just to reuse stuff and avoid the need of proving it myself :) | 27/01 16:46 |

{AS} | rribeiro: Ah :) | 27/01 16:47 |

rribeiro | {AS}: Anyway... thanks! :) | 27/01 16:47 |

{AS} | np | 27/01 16:47 |

{AS} | I am currently developing a theory of finite sets myself | 27/01 16:47 |

{AS} | but it's fairly inefficient | 27/01 16:47 |

{AS} | If all you care about is proving then there is Data.Subset I think | 27/01 16:48 |

{AS} | https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Subset.agda | 27/01 16:48 |

rribeiro | My job involves Antimirov partial derivatives | 27/01 16:49 |

rribeiro | I'll need finite sets, but problem here is to deal with union operation | 27/01 16:49 |

{AS} | I see | 27/01 16:49 |

rribeiro | most specifically its properties. | 27/01 16:49 |

{AS} | like a \in (A \union B) -> a \in A \uplus a \in B ? | 27/01 16:50 |

rribeiro | Stuff like that | 27/01 16:50 |

rribeiro | monoid properties and so on | 27/01 16:50 |

{AS} | Ah, sorry, maybe someone else here can help :) | 27/01 16:51 |

rribeiro | I believe that it is not hard to do, but it is time consuming. My hope is to find some library with these basic results ready for use. | 27/01 16:51 |

schoppenhauer | https://www.irif.fr/~letouzey/types2014/abstract-18.pdf ← is there any full version of this? | 27/01 19:52 |

pgiarrusso | Hi all! | 27/01 19:57 |

pgiarrusso | Is there a syntax to write (and fill in a hole) let open import Base.Change.Equivalence in ? | 27/01 19:58 |

pgiarrusso | `let open Foo in ?` seems to work, so the idea is not 100% insane | 27/01 19:59 |

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