--- Day changed Sun Jun 25 2017
mietekrntz: yes25/06 00:20
mietekrntz: when you declare a field, surround its name with {braces}25/06 00:20
TanebIs there a proper way to gently massage types that I have proven to be equal25/06 06:52
TanebI'm using Reflection.Binary.PropositionalEquality.subst\_2 and it's getting pretty hairy25/06 06:52
Taneb...I think at some point I should have switched to Reflection.Binary.HeterogeneousEquality25/06 06:54
TanebExcept I'm doing that bit with a different setoid! Aaargh!25/06 06:55
Tanebhttps://github.com/Taneb/Categories/blob/master/Functor.agda#L12 is the type I'm trying to define a sensible equivalence relation for25/06 07:04
TanebF ≈̂ G = Σ (∀ α → ⟦ α ⟧ᶠ ≡ ⟦ α ⟧ᵍ) (λ p → ∀ {α β} (f : C.Mor α β) → subst₂ D.Mor (p α) (p β) ⟪ f ⟫ᶠ D.≈ ⟪ f ⟫ᵍ)25/06 07:05
Taneb  where25/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 far25/06 07:05
TanebAnd I can't prove symmetry for it25/06 07:06
TanebAny pointers?25/06 07:06
TanebHmm, I can't prove Ens is cartesian closed without extensionality I think25/06 11:37
TanebAt least not the way I'm going about it25/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#L4325/06 12:19
akr[m]should I try to rewrite it with well-founded induction25/06 12:20
mietekakr[m]: deduction theorem for Hilbert system with B, C, I?25/06 16:30
akr[m]mietek: yup25/06 16:32
akr[m]also without contraction and weaking25/06 16:33
mietekI have a feeling we spoke about this some time ago25/06 16:33
akr[m]indeed :)25/06 16:33
mietekare you sure this can work?25/06 16:33
akr[m]work in what sense? I'm pretty sure BCI is a legitimate system25/06 16:34
mietekyes; I mean, have you proven the theorem for the system by other means25/06 16:34
akr[m]it's a fragment of linear logic25/06 16:35
akr[m]I have not :)25/06 16:35
mietekone thing I’ve been running into is, the termination checker doesn’t like too much abstraction25/06 16:36
mietekfor example, if I have25/06 16:36
mietek  _⊢⋆_ : Cx → Ty⋆ → Set25/06 16:37
mietek  Δ ⁏ Γ ⊢⋆ Ξ = All (Δ ⁏ Γ ⊢_) Ξ25/06 16:37
mietek(a pointwise closure of ⊢ over lists)25/06 16:37
mietekdefined using a generic All25/06 16:37
comietekhttps://www.irccloud.com/pastebin/WqyybeE7/25/06 16:37
mietekthen, in a mutual block, I have to manually unroll a definition that is otherwise fine25/06 16:38
mietekfor it to pass the termination check25/06 16:38
mietekmaybe your function composition is a bit much?25/06 16:39
mietekI should submit this as a bug, actually25/06 16:39
akr[m]so what I'm doing there is that I am applying the induction hypothesis twice over itself25/06 16:39
akr[m]I think you normally can't do that in structural induction25/06 16:40
mietekI don’t know, but it sounds problematic25/06 16:40
akr[m]yes, very problematic25/06 16:45
akr[m]hmm, this is weird25/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 terms25/06 17:22
akr[m]does this happen normally?25/06 17:22
akr[m]proof of induction*25/06 17:22
mietekakr[m]: show your work25/06 17:34
akr[m]hmm25/06 17:38
akr[m]it's a mess atm :)25/06 17:38
mietekyes. cleaning it up to a self-contained problem case is often like rubber-duck debugging.25/06 17:41
akr[m]lol25/06 17:49
akr[m]termination checker fails if you write `(π₁ ∘ π₂) x` but is fine with `π₁ (π₂ x)`25/06 17:50
mietekthat is literally what I mean earlier25/06 18:04
akr[m]ah, lol25/06 18:11
mietekakr[m]: haha, https://twitter.com/pigworker/status/87904925634204057625/06 20:13
akr[m]lol25/06 20:14

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