# /home/laney/.irssi/irclogs/Freenode/#agda.log-20170228

wedify wedify --- Day changed Mon Feb 27 2017 holy moly i thought i was finally ready to published my dependently typed chess expressions library only to just now realize i haven't done anything to enforce the king not being in check when it ends its move 27/02 01:54 that adds a ton more work 27/02 01:54 i like how the holes give a concrete feel to progress. 'ok i have ten problems now' 'now eight' 'now twelve' 27/02 02:34 wedify: you also need to ensure that you can not put the king in check if you move another piece 27/02 08:58 Like if you guard your king with a rook against an attacking piece, then you can not move the rook 27/02 08:58 wedify: do you also support castling and en passant? 27/02 09:00 AC : ∀ {A B : Set} → {P : A → B → Set} → (∀ a → Σ[ b ∈ B ] P a b) → Σ[ f ∈ (A → B) ] (∀ a → P a (f a)) 27/02 09:48 does that seem okay? there also seems to be a dependent version I found here: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.SomeCombinators 27/02 09:48 also, can I postulate the extensional version and derive LEM without too much work? :) 27/02 09:50 that should basically be the Diaconescu's theorem, which seems nontrivial 27/02 09:51 akr: Diaconescu's theorem only works for constructive _set_ theory 27/02 09:54 not constructive type theory 27/02 09:54 oh, so I can't do it in Agda, unless I first formalise constructive set theory or something? 27/02 09:54 akr: Yeah 27/02 09:55 I mean if you could derive LEM it would be unsound 27/02 09:55 hmm, wait, so you're saying I can't even state the extensional choice in Agda? 27/02 09:56 as in, postulate 27/02 09:56 akr: hmm 27/02 09:56 how would you postulate it? 27/02 09:57 I'm not sure :) but we have setoids… 27/02 09:57 http://r6.ca/blog/20050604T143800Z.html 27/02 09:57 akr: I mean you can use the classical existential instead of the constructive one 27/02 09:58 but then you introduce a classical construct already 27/02 09:58 In any case, my point is that if you want lem, just postulate it 27/02 09:58 oh, that reminds me: how do you define classical ∀ and ∃ in Agda? 27/02 09:59 akr: classical is the same as constructive for forall 27/02 09:59 {AS}: I don't want LEM, I'm just playing with these things :) 27/02 09:59 {AS}: oh, so the classical ∃ϕ is ¬∀¬ϕ? 27/02 10:00 akr: yeah 27/02 10:00 I don't see why ∀ is the same between classical and constructive though, where should I look for an explanation? 27/02 10:01 or is it obvious somehow? :) 27/02 10:03 akr: I think it has something to do with elimination forms 27/02 10:04 I am unsure the precise reason 27/02 10:04 I see, so I'd have to look into MLTT 27/02 10:05 one of these days… :) 27/02 10:05 {AS}: thank you, I have to go now 27/02 10:05 OK, bye 27/02 10:05 When checking a dependent type, should I evaluate to NF first? 27/02 12:27 aphorisme: usually WHNF is used 27/02 12:40 {AS}: so I go recursively down the type? Since, when evaluating, I should type check it first, or? 27/02 12:41 aphorisme: you would type check the type before the values yes 27/02 12:41 aphorisme: you might consider https://github.com/sweirich/pi-forall 27/02 12:41 Ah! 27/02 12:42 Nice. 27/02 12:42 Thanks, {AS}. 27/02 12:42 np! :) 27/02 12:42 {AS}: that's a good one. i didn't think of that. i support castling but not en passant. i will though, one step at a time 27/02 20:41 it's neat how programming this forces me to make explicit all sorts of things that i take for granted 27/02 20:42

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