Definition pr1_eqweqmap2 { X Y } ( e: X = Y ) : pr1 (eqweqmap e) = transportf (λ T:Type, T) e. Proof. intros. induction e. reflexivity. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.