Lemma uf_eq {c1 c2 : C} (f : C⟦c1,c2⟧) : ∏ (d1 : D c1) (d2 : D c2), (d1 -->[f] d2) ≃ (pr1 (uo c1) -->[f] pr1 (uo c2)). Proof. intros d1 d2. assert (p1 : d1 = pr1 (uo c1)). { apply uo. } assert (p2 : d2 = pr1 (uo c2)). { apply uo. } induction p1. induction p2. apply idweq. 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.