proposition: Theorem twooutof3b {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isf : isweq f) (isgf : isweq (g ∘ f)) : isweq g.
proof: Proof. intros. set (wf := make_weq f isf). set (wgf := make_weq (g ∘ f) isgf). set (invf := invmap wf). set (invgf := invmap wgf). set (invg := f ∘ invgf). assert (eginvg : ∏ z : Z, g (invg z) = z). { intro. unfold invg. apply (homotweqinvweq wgf z). } assert (einvgg : ∏ y : Y, invg (g y) = y). { intro. unfold invg. assert (isinvf: isweq invf). { apply isweqinvmap. } assert (isinvgf: isweq invgf). { apply isweqinvmap. } assert (int1 : g y = (g ∘ f) (invf y)). apply (maponpaths g (! homotweqinvweq wf y)). assert (int2 : (g ∘ f) (invgf (g y)) = (g ∘ f) (invf y)). { assert (int3: (g ∘ f) (invgf (g y)) = g y). { apply (homotweqinvweq wgf). } induction int1. apply int3. } assert (int4: (invgf (g y)) = (invf y)). { apply (invmaponpathsweq wgf). apply int2. } assert (int5: (invf (f (invgf (g y)))) = (invgf (g y))). { apply (homotinvweqweq wf). } assert (int6: (invf (f (invgf (g (y))))) = (invf y)). { induction int4. apply int5. } apply (invmaponpathsweq (make_weq invf isinvf)). simpl. apply int6. } apply (isweq_iso g invg einvgg eginvg). Defined.
imports: UniMath.Foundations.Preamble