Lemma I_unique : ∏ (a : C) (i i' : a ⇒ a), I i → I i' → i = i'. 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.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.