Definition ϕ₂ {a b : C} (f : folds_iso_data a b) {z : C} : (a ⇒ z) ≃ (b ⇒ z) := pr2 (pr1 f) z.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.Folds.folds_precat. Require Import UniMath.Folds.from_precats_to_folds_and_back.