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