glguy glguy --- Day changed Fri Jan 27 2017 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 https://glguy.net/mockingbird-html/Dark-forest.html 27/01 05:32 check : ∀ X Y Z → (X ∘ Y) ∙ Z ≡ X ∙ (Y ∙ Z); check = by-cases 27/01 05:32 glguy: I’m boggling at ByCases 27/01 09:11 {AS}, tomjack: ^^ 27/01 09:11 boggling? 27/01 09:12 I am finding it neat 27/01 09:13 It does look neat :) 27/01 09:13 If only we could be sure that Agda’s reflection is actually justified 27/01 09:14 mietek: transaltion validation? ;) 27/01 09:15 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 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 jbracker: SubHom is not a Set 27/01 12:25 so you can't use it as a type 27/01 12:25 SubHom a b f is basically a value Hom C a b -> Exists P ((x y : P) -> x \== y) 27/01 12:28 jbracker: did you mean to define it as a type? 27/01 12:29 {AS}: Yes, I did. I got confused... Not sure how to make it a type though right now... 27/01 13:06 jbracker: I think you want something like (a b : Obj C) -> Set (lsuc \ell) 27/01 13:07 and then the body being 27/01 13:07 SubHom a b = PropSubsetOf (Hom C a b) 27/01 13:07 no? 27/01 13:07 {AS}: But then I am not modelling subsets anymore... 27/01 13:08 jbracker:  huh? 27/01 13:08 because each instance of Subcategory could put whatever it wants into the Set (lsuc l_1) 27/01 13:08 jbracker: SubHom should not be a field 27/01 13:09 it should be a definition 27/01 13:09 or am I confusing something? 27/01 13:09 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 If you replace PropSet in PropSubsetOf with Set then it works 27/01 13:14 but I actually want proof irrelevance so I need PropSet 27/01 13:14 jbracker: why don't you just use Agda's Proof irrelevance? :) 27/01 13:22 In any case 27/01 13:23 you can get a set if you do something like 27/01 13:24 (X : Set \ell) -> proj_1 (SubHom a b f X) 27/01 13:25 sorry 27/01 13:28 just do 27/01 13:28 (X : Hom C a b) -> proj_1 (SubHom a b f X) 27/01 13:28 or something like that 27/01 13:28 {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 jbracker: you can define an irrelevant type as follows 27/01 14:43 https://gist.github.com/ahmadsalim/3f54d833b6e23524acf60163220c818b 27/01 14:45 jbracker: ^ 27/01 14:45 How does that let you prove ((x y : A) -> x = y) ? 27/01 14:47 jbracker: irr x = irr y 27/01 14:47 you get an irrelvant injection 27/01 14:47 oh, you don't sorry 27/01 14:49 {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 so in Agda writing . 27/01 14:50 means that the proof is irrelevant 27/01 14:50 pi1 : {ℓ : Level} {A : Set ℓ} → (x y : Irr A) → x ≡ y ; pi1 x y = refl 27/01 14:50 jbracker: Yeah 27/01 14:51 But me telling agda the proof is irrelevant with dot does not make it irrelevant 27/01 14:51 Like if I have 1 : Nat and 2 : Nat then Irr 1 and Irr 2 does not make 1 = 2 27/01 14:52 jbracker: Yeah, it does not 27/01 14:52 I was wrong about that 27/01 14:52 but you can use Irr A as the irrelevant version of A :) 27/01 14:52 so how does agda decide when It it allowed to prove equality based on a given type and when not? 27/01 14:54 jbracker: what do you mean? 27/01 14:54 It checks the dots :) 27/01 14:55 {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 although it should 27/01 14:59 jbracker: I am not sure what you are showing 27/01 15:00 but by pattern matching on x and y 27/01 15:01 you should be able to prove that theorem 27/01 15:01 https://www.irccloud.com/pastebin/UMOVAgxq/ 27/01 15:02 or well, at least if you don't have --without-K on 27/01 15:02 p refl refl = pi1 (irr refl) (irr refl) ; is still rejected 27/01 15:03 jbracker: ^ 27/01 15:03 see my paste 27/01 15:03 Yes I know that that is possible 27/01 15:03 jbracker: I mean 27/01 15:04 But then I don't see how Irr could ever be useful for anything 27/01 15:04 jbracker: it gives you a version of A which has proof irrelevant members 27/01 15:05 But the members don't get irrelevant magically you just wrap them up in Irr. They are still relevant 27/01 15:06 jbracker: irr x is irrelevant for any x 27/01 15:06 x itself is still relevant yes 27/01 15:06 so irr 1 = irr 2 27/01 15:07 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 jbracker: yeah if you want the result to be irrelevant 27/01 15:16 but notice that will give you a Set which is irrelevant 27/01 15:17 not a Set with irrelevant members 27/01 15:17 I don't think there is currently a nice way to do A -> Prop in Agda 27/01 15:19 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 which would be A -> Prop 27/01 15:19 *auch*such 27/01 15:19 jbracker: a simple solution would be to have 27/01 15:20 X -> Irr Y 27/01 15:20 where Y is the Set you want to be irrelevant 27/01 15:20 but yeah, it's fairly complicated 27/01 15:21 jbracker: Hmm, maybe we should just go to your original solution :) 27/01 15:24 {AS}: Ever since you pointed out that I need the projection it does not seem very appealing anymore. 27/01 15:25 Hi all! Is there any library that provides set data structure and some theorems about it? 27/01 16:41 rribeiro: Hi! what kind of sets? 27/01 16:43 Like red-black trees, etc.? 27/01 16:43 {AS}: yeah... Like AVL, red-black 27/01 16:44 The standard library has AVL trees, but I do not see any theorems that could be used about them 27/01 16:44 by google I found http://www.cse.chalmers.se/~nad/repos/lib/src/Data/AVL.agda 27/01 16:45 I do not unfortunately know any myself other 27/01 16:46 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 I'm asking just to reuse stuff and avoid the need of proving it myself :) 27/01 16:46 rribeiro: Ah :) 27/01 16:47 {AS}: Anyway... thanks! :) 27/01 16:47 np 27/01 16:47 I am currently developing a theory of finite sets myself 27/01 16:47 but it's fairly inefficient 27/01 16:47 If all you care about is proving then there is Data.Subset I think 27/01 16:48 https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Subset.agda 27/01 16:48 My job involves Antimirov partial derivatives 27/01 16:49 I'll need finite sets, but problem here is to deal with union operation 27/01 16:49 I see 27/01 16:49 most specifically its properties. 27/01 16:49 like a \in (A \union B) -> a \in A \uplus a \in B ? 27/01 16:50 Stuff like that 27/01 16:50 monoid properties and so on 27/01 16:50 Ah, sorry, maybe someone else here can help :) 27/01 16:51 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 https://www.irif.fr/~letouzey/types2014/abstract-18.pdf ← is there any full version of this? 27/01 19:52 Hi all! 27/01 19:57 Is there a syntax to write (and fill in a hole) let open import Base.Change.Equivalence in ? 27/01 19:58 let open Foo in ? seems to work, so the idea is not 100% insane 27/01 19:59