proposition: Lemma ϕ₁_is_comp (x : C) (f : x ⇒ a) : ϕ₁ i f = f □ (ϕ₁ i (id _ )).
proof: Proof. set (q:=pr1 (pr1 (pr1 (pr1 (pr2 i))))). specialize (q _ _ f (id _ ) f). set (q':=pr1 q ); clearbody q'. assert (H: T f (id a) f). { set (H:= pr1 (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