proposition: Theorem hsubtype_rect {X:UU} (S T : hsubtype X) (P : S ≡ T -> UU) : (∏ e : S=T, P (hsubtype_univalence S T e)) ≃ ∏ f, P f.
proof: Proof. intros. apply weqinvweq, weqonsecbase. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions