proposition: Lemma ϕ₂_is_comp (z : C) (g : a ⇒ z) : ϕ₂ i g = ϕ₂ i (id _ ) □ g.
proof: 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.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.Folds.folds_precat UniMath.Folds.from_precats_to_folds_and_back