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