Lemma T_assoc (a b c d : C) (f : a ⇒ b) (g : b ⇒ c) (h : c ⇒ d) : f ∘ (g ∘ h) = (f ∘ g) ∘ h. Proof. apply (pr2 (pr2 (pr2 (pr2 C))) a b c d f g h (f ∘ g) (g ∘ h)). - apply T_func_T. - apply T_func_T. - apply T_func_T. - apply T_func_T. Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.