proposition: Theorem isdecinclhomot {X Y : UU} (f g : X -> Y) (h : ∏ x : X, paths (f x) (g x)) (is : isdecincl f) : isdecincl g.
proof: Proof. intros. intro y. apply (isdecpropweqf (weqhfibershomot f g h y) (is y)). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom