Library UniMath.MoreFoundations.AlternativeProofs
An alternative proof of total2_paths_equiv
Theorem total2_paths_equiv' {A : UU} (B : A -> UU) (x y : ∑ x, B x) :
x = y ≃ x ╝ y.
Show proof.
simple refine (weqtotaltofib _ _ _ _ _).
- intros z p. exists (maponpaths pr1 p). induction p. reflexivity.
- apply isweqcontrcontr.
+ apply iscontrcoconusfromt.
+ exists (x ,, idpath _ ,, idpath _).
intro w. induction w as [w p], w as [a b], p as [p q], x as [a' b'], (p:a' = a), (q:b' = b).
reflexivity.
- intros z p. exists (maponpaths pr1 p). induction p. reflexivity.
- apply isweqcontrcontr.
+ apply iscontrcoconusfromt.
+ exists (x ,, idpath _ ,, idpath _).
intro w. induction w as [w p], w as [a b], p as [p q], x as [a' b'], (p:a' = a), (q:b' = b).
reflexivity.
Lemma total2_paths_equiv'_compute {A : UU} (B : A -> UU) (x y : ∑ x, B x) :
pr1weq (total2_paths_equiv' B x y) = (λ (r : x = y), base_paths _ _ r ,, fiber_paths r).
Show proof.
reflexivity.