Lemma reflects_isos_cat_of_elems_forgetful : reflects_isos cat_of_elems_forgetful. Proof. intros [c x] [d y] f Hf. apply is_iso_from_is_z_iso. assert (H := is_z_iso_from_is_iso _ Hf); clear Hf. destruct f as [f i]; destruct H as [f' j]. assert (i' : #X f' y = x). { intermediate_path (#X f' (#X f x)). - exact (maponpaths (#X f') (!i)). - intermediate_path (#X (f' ∘ f) x). + exact (eqtohomot (!functor_comp X f f') x). + intermediate_path (#X (identity c) x). * exact (eqtohomot (maponpaths #X (pr1 j)) x). * exact (eqtohomot (functor_id X c) x). } exists (f' ,, i'). split; apply cat_of_elems_mor_eq; [ exact (pr1 j) | exact (pr2 j) ]. 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.