Lemma catiso_is_globally_prop' (x : C) : ∏ d1 d2 : D x, x ,, d1 = x ,, d2. Proof. intros d1 d2. set (g := isinclweq _ _ _ (pr2 (invweq W)) x). set (h := g ((x ,, d1) ,, idpath _) ((x ,, d2) ,, idpath _)). exact (base_paths _ _ (pr1 h)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.