proposition: Lemma I_unique : ∏ (a : C) (i i' : a ⇒ a), I i → I i' → i = i'.
proof: Proof. intros a i i' Hi Hi'. destruct C as [CC [Cid Ccomp]]; simpl in *. assert (H1 : T i i' i). { apply (pr1 (pr2 Cid) _ _ _ _ ). assumption. } assert (H2 : T i i' i'). { apply (pr2 (pr2 Cid) _ _ _ _ ) . assumption. } apply (pr1 (pr2 Ccomp) _ _ _ _ _ _ _ H1 H2). Qed.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets