proposition: Lemma α_functors_pointwise_is_z_iso (hsF: has_homsets F)(X : functor C D)(Y : functor D E)(Z : functor E F) : is_z_isomorphism(C:= functor_precategory C F hsF) (α_functors X Y Z).
proof: Proof. exists (α_functors_inv X Y Z). split; apply nat_trans_eq; try assumption; intro c; apply id_left. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory