Lemma pfq : pr1 (pr1 E') · i_a · e' = h. Proof. pose (pr2 (pr1 E')) as W. simpl in W. rewrite pd_e in W. do 2 rewrite assoc in W. pose (z_iso_inv_to_right _ _ _ _ _ _ W) as V. refine (_ @ V). rewrite ! assoc'. do 2 apply maponpaths. refine (! id_right _ @ _). apply maponpaths, pathsinv0. apply (pr2 (pr2 (pr2 i_x))). Qed.
Require Import UniMath.Foundations.All. 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.Monics. Require Import UniMath.CategoryTheory.Retracts.