Several issues with 2.5.1.1

[JacquesCarette]

In particular Categories.NaturalIsomorphisms does not build (the very last line of my-iso is no longer well-formed).

There seems to be issues with Categories.Morphisms.Iso as well, but I believe I've dealt with those (in my fork).

More specifically, I am currently getting
/Users/carette/Agda/categories/Categories/NaturalIsomorphism.agda:213,3-18
Functor.F₀ F₁ x != w of type D.Obj
when checking that the type
(F₁ : Functor C D) (x₁ : C.Obj) (w : D.Obj) (G₁ : Functor C D)
(F≡G₁
: {A B : C.Obj} (f : A C.⇒ B) → Functor.F₁ F₁ f ∼ Functor.F₁ G₁ f)
(G≡F₁
: {A B : C.Obj} (f : A C.⇒ B) →
Functor.F₁ G₁ f ∼ Functor.F₁ F₁ f) →
(.Categories.NaturalIsomorphism...my-η {.o} {.ℓ} {.e} {.o′} {.ℓ′}
{.e′} {C} {D} F G F≡G F₁ G₁ F≡G₁ x₁
| w | Functor.F₀ G₁ x₁ | oneway-helper (F≡G₁ C.id))
D.∘
(.Categories.NaturalIsomorphism...my-η {.o} {.ℓ} {.e} {.o′} {.ℓ′}
{.e′} {C} {D} F G F≡G G₁ F₁ G≡F₁ x₁
| Functor.F₀ G₁ x₁ | w | oneway-helper (G≡F₁ C.id))
D.≡ D.id
of the generated with function is well-formed

where 'oneway-helper' is my short name for the "helper" function buried under oneway (just to make debugging easier). I am quite willing to help, I am just rather stuck at the moment.

[JacquesCarette]

Pull request #15 has fixed all of this.