proposition: Theorem twooutof3c {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isf : isweq f) (isg : isweq g) : isweq (g ∘ f).
proof: Proof. intros. set (wf := make_weq f isf). set (wg := make_weq g isg). set (invf := invmap wf). set (invg := invmap wg). set (gf := g ∘ f). set (invgf := invf ∘ invg). assert (egfinvgf : ∏ x : X, invgf (gf x) = x). { intros x. assert (int1 : invf (invg (g (f x))) = invf (f x)). { apply (maponpaths invf (homotinvweqweq wg (f x))). } assert (int2 : invf (f x) = x). { apply (homotinvweqweq wf x). } induction int1. apply int2. } assert (einvgfgf : ∏ z : Z, gf (invgf z) = z). { intros z. assert (int1 : g (f (invgf z)) = g (invg z)). { unfold invgf. apply (maponpaths g (homotweqinvweq wf (invg z))). } assert (int2 : g (invg z) = z). { apply (homotweqinvweq wg z). } induction int1. apply int2. } apply (isweq_iso gf invgf egfinvgf einvgfgf). Defined.
imports: UniMath.Foundations.Preamble