Lemma T_I_r (a b : C) (f : a ⇒ b) : (I_func a) ∘ f = f. Proof. assert (H : T (I_func a) f f). { apply (pr2 (pr2 (pr1 (pr2 C)))). apply I_func_I. } assert (H' : T (I_func a) f (T_func (I_func a) f)). { 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.