--- Day changed Fri Jan 27 2017
glguyI 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
glguyhttps://glguy.net/mockingbird-html/Dark-forest.html27/01 05:32
glguycheck : ∀ X Y Z → (X ∘ Y) ∙ Z ≡ X ∙ (Y ∙ Z); check = by-cases27/01 05:32
mietekglguy: I’m boggling at ByCases27/01 09:11
mietek{AS}, tomjack: ^^27/01 09:11
tomjackboggling?27/01 09:12
mietekI am finding it neat27/01 09:13
{AS}It does look neat :)27/01 09:13
mietekIf only we could be sure that Agda’s reflection is actually justified27/01 09:14
{AS}mietek: transaltion validation? ;)27/01 09:15
jbrackerCan 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
jbrackerI have tried to give the definition of Subcategory the type "Set (lsuc (lsuc (l_0 u l_1)))" but that does not change anything27/01 11:47
{AS}jbracker: SubHom is not a Set27/01 12:25
{AS}so you can't use it as a type27/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 being27/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
jbrackerbecause 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 field27/01 13:09
{AS}it should be a definition27/01 13:09
{AS}or am I confusing something?27/01 13:09
jbrackerI 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
jbrackerIf you replace PropSet in PropSubsetOf with Set then it works27/01 13:14
jbrackerbut I actually want proof irrelevance so I need PropSet27/01 13:14
{AS}jbracker: why don't you just use Agda's Proof irrelevance? :)27/01 13:22
{AS}In any case27/01 13:23
{AS}you can get a set if you do something like27/01 13:24
{AS}(X : Set \ell) -> proj_1 (SubHom a b f X)27/01 13:25
{AS}sorry27/01 13:28
{AS}just do27/01 13:28
{AS}(X : Hom C a b) -> proj_1 (SubHom a b f X)27/01 13:28
{AS}or something like that27/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 types27/01 14:41
{AS}jbracker: you can define an irrelevant type as follows27/01 14:43
{AS}https://gist.github.com/ahmadsalim/3f54d833b6e23524acf60163220c818b27/01 14:45
{AS}jbracker: ^27/01 14:45
jbrackerHow does that let you prove ((x y : A) -> x = y) ?27/01 14:47
{AS}jbracker: irr x = irr y27/01 14:47
{AS}you get an irrelvant injection27/01 14:47
{AS}oh, you don't sorry27/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 irrelevant27/01 14:50
jbrackerpi1 : {ℓ : Level} {A : Set ℓ} → (x y : Irr A) → x ≡ y ; pi1 x y = refl27/01 14:50
{AS}jbracker: Yeah27/01 14:51
jbrackerBut me telling agda the proof is irrelevant with dot does not make it irrelevant27/01 14:51
jbrackerLike if I have 1 : Nat and 2 : Nat then Irr 1 and Irr 2 does not make 1 = 227/01 14:52
{AS}jbracker: Yeah, it does not27/01 14:52
{AS}I was wrong about that27/01 14:52
{AS}but you can use Irr A as the irrelevant version of A :)27/01 14:52
jbrackerso 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 work27/01 14:59
jbrackeralthough it should27/01 14:59
{AS}jbracker: I am not sure what you are showing27/01 15:00
{AS}but by pattern matching on x and y27/01 15:01
{AS}you should be able to prove that theorem27/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 on27/01 15:02
jbrackerp refl refl = pi1 (irr refl) (irr refl) ; is still rejected27/01 15:03
{AS}jbracker: ^27/01 15:03
{AS}see my paste27/01 15:03
jbrackerYes I know that that is possible27/01 15:03
{AS}jbracker: I mean27/01 15:04
jbrackerBut then I don't see how Irr could ever be useful for anything27/01 15:04
{AS}jbracker: it gives you a version of A which has proof irrelevant members27/01 15:05
jbrackerBut the members don't get irrelevant magically you just wrap them up in Irr. They are still relevant27/01 15:06
{AS}jbracker: irr x is irrelevant for any x27/01 15:06
{AS}x itself is still relevant yes27/01 15:06
{AS}so irr 1 = irr 227/01 15:07
jbrackerSo 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 irrelevant27/01 15:16
{AS}but notice that will give you a Set which is irrelevant27/01 15:17
{AS}not a Set with irrelevant members27/01 15:17
{AS}I don't think there is currently a nice way to do A -> Prop in Agda27/01 15:19
jbrackerSO I want: SubObj : (Obj C) -> Set ... ; auch that I know for all (c : Obj c) -> (q p : SubObj c) -> q ≡ p27/01 15:19
jbrackerwhich would be A -> Prop27/01 15:19
jbracker*auch*such27/01 15:19
{AS}jbracker: a simple solution would be to have27/01 15:20
{AS}X -> Irr Y27/01 15:20
{AS}where Y is the Set you want to be irrelevant27/01 15:20
{AS}but yeah, it's fairly complicated27/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
rribeiroHi 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-black27/01 16:44
rribeiroThe standard library has AVL trees, but I do not see any theorems that could be used about them27/01 16:44
{AS}by google I found http://www.cse.chalmers.se/~nad/repos/lib/src/Data/AVL.agda27/01 16:45
{AS}I do not unfortunately know any myself other27/01 16:46
rribeiroThis is almost the implementation in STD library. The point is that there's no lemmas about union and other operations27/01 16:46
rribeiroI'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}np27/01 16:47
{AS}I am currently developing a theory of finite sets myself27/01 16:47
{AS}but it's fairly inefficient27/01 16:47
{AS}If all you care about is proving then there is Data.Subset I think27/01 16:48
{AS}https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Subset.agda27/01 16:48
rribeiroMy job involves Antimirov partial derivatives27/01 16:49
rribeiroI'll need finite sets, but problem here is to deal with union operation27/01 16:49
{AS}I see27/01 16:49
rribeiromost 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
rribeiroStuff like that27/01 16:50
rribeiromonoid properties and so on27/01 16:50
{AS}Ah, sorry, maybe someone else here can help :)27/01 16:51
rribeiroI 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
schoppenhauerhttps://www.irif.fr/~letouzey/types2014/abstract-18.pdf ← is there any full version of this?27/01 19:52
pgiarrussoHi all!27/01 19:57
pgiarrussoIs 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% insane27/01 19:59

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