Definition T_func {a b c : C} (f : a ⇒ b) (g : b ⇒ c) : a ⇒ c := pr1 (pr1 (T_contr a b c f g)).
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.