# Library UniMath.MoreFoundations.PartD

Require Export UniMath.Foundations.All.

Lemma eqweqmap_transportb {T U: Type} (p: T = U) :
(λ u:U, eqweqmap (! p) u) = transportb (λ X:Type, X) p.
Proof.
induction p. reflexivity.
Defined.

Lemma eqweqmap_weqtopaths {T U} (w : TU) : eqweqmap (weqtopaths w) = w.
Proof.
exact (homotweqinvweq (univalence T U) w).
Defined.

Lemma sum_of_fibers {A B:Type} (f: A B) :
( b:B, hfiber f b) A.
Proof.
use make_weq.
- intro bap. exact (pr1 (pr2 bap)).
- intro a. use make_iscontr.
+ use make_hfiber.
× (f a).
use make_hfiber.
{ exact a. }
{ reflexivity. }
× cbn. reflexivity.
+ intro b1a1p1p. induction b1a1p1p as [b1a1p1 p]. induction p.
induction b1a1p1 as [b1 [a1 p1]]. induction p1. reflexivity.
Defined.

Definition display {A: Type} :
( B, B A) (A Type).
Proof.
intro Bf. exact (hfiber (pr2 Bf)).
Defined.

Definition totalfst {A: Type} :
(A Type) ( B, B A).
Proof.
intro P. ( a:A, P a). exact pr1.
Defined.

Lemma totalfst_display {A: Type} (Bf: B, B A) : totalfst (display Bf) = Bf.
Proof.
use total2_paths_f.
- apply weqtopaths. apply sum_of_fibers.
- rewrite transportf_fun.
rewrite <- eqweqmap_transportb.
rewrite eqweqmap_pathsinv0.
rewrite eqweqmap_weqtopaths.
reflexivity.
Defined.

Lemma display_totalfst {A: Type} (P: A Type) : display(totalfst(P)) = P.
Proof.
apply funextsec; intro a.
apply pathsinv0.
apply weqtopaths.
apply ezweqpr1.
Defined.

Lemma display_weq (A:Type) :
( B, B A) (A Type).
Proof.
display.
apply (isweq_iso display totalfst).
- exact totalfst_display.
- exact display_totalfst.
Defined.