--- Day changed Wed Feb 01 2017
jonsterlingtomjack: ouch!01/02 00:45
mudriSomeone needs to update the topic line here? ;-)01/02 00:51
glguyWhat date would we update it to?01/02 00:53
glguySince the ticket is open would we just put "today"?01/02 00:53
mudriUm... good point.01/02 00:54
subttleHi, the wordsmith in me would like to ask a question. I'm learning Agda by making a bunch of proofs about Regular Expressions. Right now I am working on structural (read: ignoring algebraic properties) equality of RegExps and I have an already completed proof of congruent Kleene-star:01/02 01:45
subttle⋆-cong : Congruent₁ {A = RegExp} _≡r_ _⋆01/02 01:45
subttlewhere _≡r_ is structural equality. This signature is essentially: 01/02 01:45
subttle{i j : RegExp} → i ≡r j → (_≡r_ on _⋆) i j01/02 01:45
subttleMy question is: is there a name for going the other way? i.e.01/02 01:45
subttle{i j : RegExp} → (_≡r_ on _⋆) i j → i ≡r j01/02 01:45
subttleI also finished the code for this and just called it "⋆-uncong" but I would like to know if there is a better term for this. I'm using agda-stdlib 0.13. Thank you for your help.01/02 01:46
mudrisubttle: it looks like some sort of injectivity.01/02 10:36
mudriThink, if f x = f y then x = y, but with a different equivalence relation.01/02 10:38
{AS}Yeah this is exactly injectivity01/02 11:14
{AS}basically you are saying that * preserves equivalences01/02 11:15
gallaismietek: I see you were talking about hsubst as nbe a few weeks ago. Have you seen this? https://github.com/larrytheliquid/sbe01/02 16:10
mietekgallais: yes, I did; thank you. Do you have an opinion?01/02 16:10
mietekThe link in the readme seems wrong... 01/02 16:11
mietekIt should be http://www.larrytheliquid.com/drafts/sbe.pdf01/02 16:11
mietekgallais: I didn’t quite understand what’s novel about it01/02 16:13
mietekgallais: I should read it again, now that I have some more practice01/02 16:13
mietekgallais: if I recall correctly, I didn’t really see how what they’re doing is different from NbE01/02 16:14
gallaisSame here tbh. Nbe for a bidirectional calculus. I'd have hoped to see the diagram on the 2nd page as an Agda theorem but AFAICT sbe is *defined* as the composition01/02 16:17
mietek"More generally, an important difference between normalization and hereditary substitution is that the former preserves the type (A) and context (Γ ) of its input, while the latter only preserves its type (the context changes to ∆)." 01/02 16:19
mietekDoes it really change?01/02 16:19
mietekNot in my hsubst it doesn’t01/02 16:19
mietekgallais: the way I understood Sam Lindley when he said hsubst is really NbE (or, everything is really NbE) was, if you start with NbE with an explicit model, and continue inlining enough things, you should eventually arrive at hsubst01/02 16:22
mietekI haven’t done that, though01/02 16:22
mietekI’m not sure how you would get spines this way01/02 16:22
larrytheliquidin agda 2.4 i could disable agda-input (backslash translating to unicode) with (toggle-input-method). does anyone know how to disable it in using the agda 2.5?01/02 18:52
glguylarrytheliquid: C-\   and  M-x toggle-input-method <enter> both work for me with spacemac + agda 2.5.201/02 19:21
larrytheliquidweird, doesnt work for me on emacs 24.5 for mac01/02 19:25
larrytheliquidbut i did find the solution, (quail-deactivate) and (quail-activate) do the trick01/02 19:25
glguyIf it matters, I'm using emacs 25.1.101/02 19:26
larrytheliquidyeah not sure about emacs versions mattering either01/02 19:27
larrytheliquidthx for trying it out though01/02 19:27
mieteklarrytheliquid: oh hi :)01/02 19:29
larrytheliquidmietek: hiya01/02 19:30
mieteklarrytheliquid: your SbE work came up today. I’d love to ask you a couple questions about it. Since it’s not really Agda-specific, would you like to join ##dependent?01/02 19:31
larrytheliquidsure01/02 19:31

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