Definition try0map1 (T : UU) (t : T) (t1 t2 : T) (e1 : t = t1) (e2 : t = t2) (X : try0 T t t1 t2 e1 e2) : t1 = t2. Proof. intros. induction X. apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.