Lemma ϕ₁_is_comp (x : C) (f : x ⇒ a) : ϕ₁ i f = f □ (ϕ₁ i (id _ )). 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.
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.