proposition: Theorem weqfromhfiberfromstn { n : nat } { X : UU } ( x : X ) ( is : isisolated X x ) ( f : ⟦n⟧ -> X ) : total2 ( λ x0 : nat, hfiber f x ≃ (⟦x0⟧) ).
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions