Lemma ϕo_determined : ∏ f, ϕ∙ i f = ϕ∙ i' f. Proof. intro f. do 2 rewrite ϕo_ϕ₁_ϕ₂. rewrite ϕ₂_determined. rewrite H. apply idpath. Qed.
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.