proposition: Lemma T_func_T {a b c : C} (f : a ⇒ b) (g : b ⇒ c) : T f g (f ∘ g).
proof: Proof. apply (pr2 (pr1 (T_contr a b c f g))). Defined.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets