proposition: Lemma I_contr : ∏ a : C, iscontr (∑ f : a ⇒ a, I f).
proof: Proof. intro a. set (H := pr1 (pr1 (pr2 C)) a). set (H' := make_hProp (iscontr (∑ f : a ⇒ a, I f)) (isapropiscontr _ )). apply (H H'); simpl. intro t; exists t. intro t'. apply subtypePath. - intro b; apply pr2. - destruct t; destruct t'; apply I_unique; assumption. Defined.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets