Lemma ϕo_ϕ₁_ϕ₂ (f : a ⇒ a) : ϕ∙ i f = (ϕ₂ i (id _ ) □ f) □ ϕ₁ i (id _). Proof. set (q:=pr2 (pr1 (pr2 (pr1 (pr2 i))))); simpl in q; clearbody q. specialize (q _ f (id _ ) f). set (q':=pr1 q). clearbody q'. simpl in q'. clear q. match goal with | [_ : ?a → _ |- _ ] => assert a end. { apply comp_compose2. apply (@id_right C'). } specialize (q' X). clear X. set (q:= comp_compose2' q'). clearbody q; clear q'. simpl in *. change (ϕ∙ i f) with (ϕ∙ (pr1 i) f). rewrite <- q. clear q. rewrite ϕ₂_is_comp. 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.