delta-left-unity-law  : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
                                             (delta-mu  ∙ (delta-fmap delta-eta)) d ≡ id d
delta-left-unity-law (mono x)    = refl
delta-left-unity-law {n = (S n)} (delta x d) = begin
  (delta-mu ∙ delta-fmap delta-eta) (delta x d)            ≡⟨ refl ⟩
  delta-mu ( delta-fmap delta-eta (delta x d))             ≡⟨ refl ⟩
  delta-mu (delta (delta-eta x) (delta-fmap delta-eta d))  ≡⟨ refl ⟩
  delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
  ≡⟨ refl ⟩
  delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
  ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-covariant tailDelta delta-eta d)) ⟩
  delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d))  ≡⟨ refl ⟩
  delta x (delta-mu (delta-fmap (delta-eta {n = n}) d))  ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
  delta x d ≡⟨ refl ⟩
  id (delta x d)  ∎