proposition: Theorem Equiv_rect (X Y : Struc) (P : X ≅ Y -> UU) : (∏ e : X = Y, P (Struc_univalence _ _ e)) -> ∏ f, P f.
proof: Proof. intros ih f. set (p := ih (invmap (Struc_univalence _ _) f)). set (h := homotweqinvweq (Struc_univalence _ _) f). exact (transportf P h p). Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AlternativeProofs