proposition: Lemma T_I_l (a b : C) (f : a ⇒ b) : f ∘ (I_func b) = f.
proof: Proof. assert (H : T f (I_func b) f). { apply (pr1 (pr2 (pr1 (pr2 C)))). apply I_func_I. } assert (H' : T f (I_func b) (T_func f (I_func b))). { apply T_func_T. } set (H2 := pr1 (pr2 (pr2 (pr2 C)))). apply (H2 _ _ _ _ _ _ _ H' H). Defined.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets