Lemma T_I_l (a b : C) (f : a ⇒ b) : f ∘ (I_func b) = f. 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.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.