--- Day changed Sun Jun 25 2017 | ||

mietek | rntz: yes | 25/06 00:20 |
---|---|---|

mietek | rntz: when you declare a field, surround its name with {braces} | 25/06 00:20 |

Taneb | Is there a proper way to gently massage types that I have proven to be equal | 25/06 06:52 |

Taneb | I'm using Reflection.Binary.PropositionalEquality.subst\_2 and it's getting pretty hairy | 25/06 06:52 |

Taneb | ...I think at some point I should have switched to Reflection.Binary.HeterogeneousEquality | 25/06 06:54 |

Taneb | Except I'm doing that bit with a different setoid! Aaargh! | 25/06 06:55 |

Taneb | https://github.com/Taneb/Categories/blob/master/Functor.agda#L12 is the type I'm trying to define a sensible equivalence relation for | 25/06 07:04 |

Taneb | F ≈̂ G = Σ (∀ α → ⟦ α ⟧ᶠ ≡ ⟦ α ⟧ᵍ) (λ p → ∀ {α β} (f : C.Mor α β) → subst₂ D.Mor (p α) (p β) ⟪ f ⟫ᶠ D.≈ ⟪ f ⟫ᵍ) | 25/06 07:05 |

Taneb | where | 25/06 07:05 |

Taneb | open Functor F renaming (⟦_⟧ to ⟦_⟧ᶠ; ⟪_⟫ to ⟪_⟫ᶠ) | 25/06 07:05 |

Taneb | open Functor G renaming (⟦_⟧ to ⟦_⟧ᵍ; ⟪_⟫ to ⟪_⟫ᵍ) | 25/06 07:05 |

Taneb | ^that's what I have so far | 25/06 07:05 |

Taneb | And I can't prove symmetry for it | 25/06 07:06 |

Taneb | Any pointers? | 25/06 07:06 |

Taneb | Hmm, I can't prove Ens is cartesian closed without extensionality I think | 25/06 11:37 |

Taneb | At least not the way I'm going about it | 25/06 11:37 |

akr[m] | How do I assert that a function is terminating? | 25/06 11:43 |

akr[m] | ok it's {-# TERMINATING #-} | 25/06 11:47 |

akr[m] | Does anyone have any idea if this double application of the induction hypothesis can actually not terminate, or if it's just that Agda can't see the termination? https://github.com/osense/linear/blob/master/BCI/Hilbert/Definition.agda#L43 | 25/06 12:19 |

akr[m] | should I try to rewrite it with well-founded induction | 25/06 12:20 |

mietek | akr[m]: deduction theorem for Hilbert system with B, C, I? | 25/06 16:30 |

akr[m] | mietek: yup | 25/06 16:32 |

akr[m] | also without contraction and weaking | 25/06 16:33 |

mietek | I have a feeling we spoke about this some time ago | 25/06 16:33 |

akr[m] | indeed :) | 25/06 16:33 |

mietek | are you sure this can work? | 25/06 16:33 |

akr[m] | work in what sense? I'm pretty sure BCI is a legitimate system | 25/06 16:34 |

mietek | yes; I mean, have you proven the theorem for the system by other means | 25/06 16:34 |

akr[m] | it's a fragment of linear logic | 25/06 16:35 |

akr[m] | I have not :) | 25/06 16:35 |

mietek | one thing I’ve been running into is, the termination checker doesn’t like too much abstraction | 25/06 16:36 |

mietek | for example, if I have | 25/06 16:36 |

mietek | _⊢⋆_ : Cx → Ty⋆ → Set | 25/06 16:37 |

mietek | Δ ⁏ Γ ⊢⋆ Ξ = All (Δ ⁏ Γ ⊢_) Ξ | 25/06 16:37 |

mietek | (a pointwise closure of ⊢ over lists) | 25/06 16:37 |

mietek | defined using a generic All | 25/06 16:37 |

comietek | https://www.irccloud.com/pastebin/WqyybeE7/ | 25/06 16:37 |

mietek | then, in a mutual block, I have to manually unroll a definition that is otherwise fine | 25/06 16:38 |

mietek | for it to pass the termination check | 25/06 16:38 |

mietek | maybe your function composition is a bit much? | 25/06 16:39 |

mietek | I should submit this as a bug, actually | 25/06 16:39 |

akr[m] | so what I'm doing there is that I am applying the induction hypothesis twice over itself | 25/06 16:39 |

akr[m] | I think you normally can't do that in structural induction | 25/06 16:40 |

mietek | I don’t know, but it sounds problematic | 25/06 16:40 |

akr[m] | yes, very problematic | 25/06 16:45 |

akr[m] | hmm, this is weird | 25/06 17:22 |

akr[m] | I'm doing a proof on induction on terms and in one case I can only do it on closed terms | 25/06 17:22 |

akr[m] | does this happen normally? | 25/06 17:22 |

akr[m] | proof of induction* | 25/06 17:22 |

mietek | akr[m]: show your work | 25/06 17:34 |

akr[m] | hmm | 25/06 17:38 |

akr[m] | it's a mess atm :) | 25/06 17:38 |

mietek | yes. cleaning it up to a self-contained problem case is often like rubber-duck debugging. | 25/06 17:41 |

akr[m] | lol | 25/06 17:49 |

akr[m] | termination checker fails if you write `(π₁ ∘ π₂) x` but is fine with `π₁ (π₂ x)` | 25/06 17:50 |

mietek | that is literally what I mean earlier | 25/06 18:04 |

akr[m] | ah, lol | 25/06 18:11 |

mietek | akr[m]: haha, https://twitter.com/pigworker/status/879049256342040576 | 25/06 20:13 |

akr[m] | lol | 25/06 20:14 |

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