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.

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.