Lemma ϕ₂_is_comp (z : C) (g : a ⇒ z) : ϕ₂ i g = ϕ₂ i (id _ ) □ g. Proof. set (q:=pr2 (pr1 (pr1 (pr2 i)))). simpl in q. specialize (q _ _ (id _ ) g g). set (q':=pr1 q ); clearbody q'. assert (H: T (id a) g g). { set (H:= pr2 (pr2 (pr1 (pr2 C)))). apply H. apply I_func_I. } set (q'H:= q' H). clearbody q'H; clear H q' q. apply path_to_ctr. assumption. 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.