Theorem weqfromhfiberfromstn { n : nat } { X : UU } ( x : X ) ( is : isisolated X x ) ( f : ⟦n⟧ -> X ) : total2 ( λ x0 : nat, hfiber f x ≃ (⟦x0⟧) ). Proof. intros. set ( t := weqfromdecsubsetofstn ( λ i : _, eqbx X x is ( f i ) ) ). split with ( pr1 t ). apply ( weqcomp ( weqhfibertobhfiber f x is ) ( pr2 t ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.