delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
      (f : A -> B) -> (x : A) ->
      (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
delta-eta-is-nt {n = O}   f x = refl
delta-eta-is-nt {n = S n} f x = begin
  (delta-eta ∙ f) x                        ≡⟨ refl ⟩
  delta-eta (f x)                          ≡⟨ refl ⟩
  delta (f x) (delta-eta (f x))
  ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
  delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
  delta-fmap f (delta x (delta-eta x))     ≡⟨ refl ⟩
  delta-fmap f (delta-eta x)               ∎