Lemma I_contr : ∏ a : C, iscontr (∑ f : a ⇒ a, I f). 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.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.