Closed pufferffish closed 10 months ago
Copy and pasted from discord for more context:
Basically like FreeCMon
and FreeMon
are very complicated because you need like a bunch of lemmas like these to convert lookup
to sharp
:
♯-asscor :
∀ a b cs z ->
lookup (a L.∷ 𝔜 .algebra (M.⊕ , lookup (b L.∷ cs L.∷ L.[])) L.∷ L.[]) z
≡
sharp M.MonSig 𝔜 (lookup (a L.∷ b L.∷ cs L.∷ L.[])) (lookup (leaf fzero L.∷ node (M.⊕ , lookup (leaf fone L.∷ leaf ftwo L.∷ L.[])) L.∷ L.[]) z)
A lot of work is spent converting lookup
to sharp
, then apply structure equalities like 𝔜-cmon M.assocr (lookup (_♯ m ∷ _♯ n ∷ _♯ o ∷ []))
in the SList
example:
♯-α a b cs =
_ ≡⟨ cong (λ z -> 𝔜 .algebra (M.⊕ , z)) (funExt (♯-asscor (f a) (f b) (cs ♯))) ⟩
_ ≡⟨ sym (𝔜-cmon M.assocr (lookup (f a L.∷ f b L.∷ (cs ♯) L.∷ L.[]))) ⟩ -- sym assocr, a + (b + c) = (a + b) + c
_ ≡⟨ cong (λ z -> 𝔜 .algebra (M.⊕ , z)) (sym (funExt (♯-comm (f a) (f b) (cs ♯)))) ⟩
_ ≡⟨ cong (λ z -> 𝔜 .algebra (M.⊕ , lookup (z L.∷ (cs ♯) L.∷ L.[]) )) lemma-comm ⟩ -- comm (a + b) + c = (b + a) + c
_ ≡⟨ cong (λ z -> 𝔜 .algebra (M.⊕ , z)) (funExt (♯-comm (f b) (f a) (cs ♯))) ⟩
_ ≡⟨ 𝔜-cmon M.assocr (lookup (f b L.∷ f a L.∷ (cs ♯) L.∷ L.[])) ⟩ -- assocr, (b + a) + c = b + (a + c)
_ ≡⟨ cong (λ z -> 𝔜 .algebra (M.⊕ , z)) (sym (funExt (♯-asscor (f b) (f a) (cs ♯)))) ⟩
_ ∎
I was basically spamming these lemmas, converting lookup to sharp, apply equality, convert back to lookup, and repeat
If we can somehow automatically generate these lemmas it would look a lot better but I can't think of anything beside writing tactics:
lemma : (z : Arity 2) ->
lookup (𝔜 .algebra (M.e , lookup []) ∷ _♯ m ∷ []) z
≡
sharp M.MonSig 𝔜 (λ _ → _♯ m) (lookup (node (M.e , lookup []) ∷ leaf fzero ∷ []) z)
lemma : (z : Arity 2) ->
lookup (_♯ m ∷ 𝔜 .algebra (M.e , lookup []) ∷ []) z
≡
sharp M.MonSig 𝔜 (λ _ → _♯ m) (lookup (leaf fzero ∷ node (M.e , lookup []) ∷ []) z)
These are just the lemmas saying how to interpret the symbols as functions, equations as 1-paths, and so should be moved to the Desc file, and reused from there. For groupoids, similarly, interpret coherences as 2-paths.
It might be possible to write a generic lemma about arities by induction on the arity argument, but we just need these for 0, 1, 2, and we discussed a few ways of writing them.
Mostly done except #52
The lemmas about sharp in free monoid can probably be factored out
Note: It might be a fact about FinTree and some form of sharp-eta there are a couple of sharp M.MonSig 𝔜 (λ → ♯ m), so sharp of a constant function should be a constant function