Theorem isweqmaponsec1 {X Y : UU} (P : Y -> UU) (f : X ≃ Y) : isweq (maponsec1 P f). Proof. intros. set (map := maponsec1 P f). set (invf := invmap f). set (e1 := homotweqinvweq f). set (e2 := homotinvweqweq f). set (im1 := λ (sx : ∏ x, P (f x)) y, sx (invf y)). set (im2 := λ (sy': ∏ y : Y, P (f (invf y))) y, transportf _ (homotweqinvweq f y) (sy' y)). set (invmapp := λ (sx : ∏ x, P (f x)), im2 (im1 sx)). assert (efg0 : ∏ (sx : (∏ x, P (f x))) x, (map (invmapp sx)) x = sx x). { intro. intro. unfold map. unfold invmapp. unfold im1. unfold im2. unfold maponsec1. simpl. fold invf. set (ee := e2 x). fold invf in ee. set (e3x := λ x0 : X, invmaponpathsweq f (invf (f x0)) x0 (homotweqinvweq f (f x0))). set (e3 := e3x x). assert (e4 : homotweqinvweq f (f x) = maponpaths f e3) by apply (pathsinv0 (pathsweq4 f (invf (f x)) x _)). assert (e5 : transportf P (homotweqinvweq f (f x)) (sx (invf (f x))) = transportf P (maponpaths f e3) (sx (invf (f x)))) by apply (maponpaths (λ e40, (transportf P e40 (sx (invf (f x))))) e4). assert (e6 : transportf P (maponpaths f e3) (sx (invf (f x))) = transportf (λ x, P (f x)) e3 (sx (invf (f x)))) by apply (pathsinv0 (functtransportf f P e3 (sx (invf (f x))))). set (ff := λ x, invf (f x)). assert (e7 : transportf (λ x, P (f x)) e3 (sx (invf (f x))) = sx x) by apply (maponsec1l2 (λ x, P (f x)) ff e3x sx x). apply (pathscomp0 (pathscomp0 e5 e6) e7). } assert (efg : ∏ sx : (∏ x, P (f x)), map (invmapp sx) = sx) by (intro; apply (funextsec _ _ _ (efg0 sx))). assert (egf0 : ∏ sy : (∏ y : Y, P y), ∏ y : Y, (invmapp (map sy)) y = sy y). { intros. unfold invmapp. unfold map. unfold im1. unfold im2. unfold maponsec1. set (ff := λ y : Y, f (invf y)). fold invf. apply (maponsec1l2 P ff (homotweqinvweq f) sy y). } assert (egf : ∏ sy : (∏ y : Y, P y), invmapp (map sy) = sy) by (intro; apply (funextsec _ _ _ (egf0 sy))). apply (isweq_iso map invmapp egf efg). Defined.