proposition: Lemma T_contr : ∏ (a b c : C) (f : a ⇒ b) (g : b ⇒ c), iscontr (∑ h, T f g h).
proof: 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.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets