Definition left_unit_as_nat_z_iso: nat_z_iso lunit_left_gen (functor_identity [C, D]). Proof. use make_nat_z_iso. + use make_nat_trans. * intro F. apply λ_functors. * apply is_nat_trans_l_functors. + intro F. cbn. use nat_trafo_z_iso_if_pointwise_z_iso. intro c. use tpair. * exact (identity (pr1 F c)). * abstract ( apply Isos.is_inverse_in_precat_identity ). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.