Lemma proofirrelevance {X : UU} (is : isaprop X) : ∏ x1 x2, x1 = x2. Proof. intros X is x1. apply (tfc X (λ x2, x1 = x2) is x1 (idpath x1)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.