proposition: Proposition indexed_cat_lunitor_alt {x y : C} (f : x --> y) (xx : Φ x) : # (Φ $ f) (indexed_cat_id Φ x xx) · indexed_cat_comp Φ (identity x) f xx = idtoiso (maponpaths (λ g, (Φ $ g) xx) (!(id_left f))).
proof: Proof. refine (_ @ id_left _). cbn. rewrite (indexed_cat_lunitor f xx). refine (!(id_right _) @ _). rewrite !assoc'. do 2 apply maponpaths. refine (_ @ pr1_idtoiso_concat _ _). change (identity ((Φ $ identity x · f) xx)) with (pr1 (idtoiso (idpath ((Φ $ identity x · f) xx)))). do 2 apply maponpaths. refine (_ @ maponpathscomp0 (λ g, (Φ $ g) xx) _ _). rewrite pathsinv0r. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations