delta-fmap-mu-to-tail : {l : Level} {A : Set l} (n m : Nat) ->
    (d : Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)) ->
  delta-fmap tailDelta (delta-fmap delta-mu d)
  ≡
  (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d)))
delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl
delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl
delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin
  delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds))
  ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩
  delta (mono dxx)
    (delta-fmap delta-mu
     (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
  ∎
delta-fmap-mu-to-tail (S n) (S m) (delta (delta (delta x (delta xx d))
                                                (delta (delta dx (delta dxx dd)) ds)) dds) = begin
  delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
    (delta-fmap tailDelta (delta-fmap delta-mu dds))
  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de)
           (delta-fmap-mu-to-tail n (S m) dds) ⟩
  delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
    (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds)))
  ∎



delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
              ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
delta-association-law {n =   O} (mono d)                          = refl
delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
  ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
  delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
  ≡⟨ cong (\de -> delta x de)
           (delta-association-law (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
  delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
  ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩
  delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
  ∎