Lemma T_contr : ∏ (a b c : C) (f : a ⇒ b) (g : b ⇒ c), iscontr (∑ h, T f g h). Proof. intros a b c f g. set (H' := make_hProp (iscontr (∑ h : a ⇒ c, T f g h)) (isapropiscontr _ )). apply (pr1 (pr2 (pr2 C)) a b c f g H'). simpl; intro t; exists t. intro t'. apply subtypePath. - intro; apply pr2. - destruct t as [t tp]; destruct t' as [t' tp']; simpl in *. apply (pr1 (pr2 (pr2 (pr2 C))) _ _ _ f g ); assumption. Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.