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.
Show proof.
Lemma eqweqmap_weqtopaths {T U} (w : T≃U) : eqweqmap (weqtopaths w) = w.
Show proof.
Lemma sum_of_fibers {A B:Type} (f: A -> B) :
(∑ b:B, hfiber f b) ≃ A.
Show proof.
Definition display {A: Type} :
(∑ B, B -> A) -> (A -> Type).
Show proof.
Definition totalfst {A: Type} :
(A -> Type) -> (∑ B, B -> A).
Show proof.
Lemma totalfst_display {A: Type} (Bf: ∑ B, B -> A) : totalfst (display Bf) = Bf.
Show proof.
Lemma display_totalfst {A: Type} (P: A -> Type) : display(totalfst(P)) = P.
Show proof.
Lemma display_weq (A:Type) :
(∑ B, B -> A) ≃ (A -> Type).
Show proof.
Lemma eqweqmap_transportb {T U: Type} (p: T = U) :
(λ u:U, eqweqmap (! p) u) = transportb (λ X:Type, X) p.
Show proof.
induction p. reflexivity.
Lemma eqweqmap_weqtopaths {T U} (w : T≃U) : eqweqmap (weqtopaths w) = w.
Show proof.
Lemma sum_of_fibers {A B:Type} (f: A -> B) :
(∑ b:B, hfiber f b) ≃ A.
Show proof.
use make_weq.
- intro bap. exact (pr1 (pr2 bap)).
- intro a. use make_iscontr.
+ use make_hfiber.
* exists (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.
- intro bap. exact (pr1 (pr2 bap)).
- intro a. use make_iscontr.
+ use make_hfiber.
* exists (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.
Definition display {A: Type} :
(∑ B, B -> A) -> (A -> Type).
Show proof.
Definition totalfst {A: Type} :
(A -> Type) -> (∑ B, B -> A).
Show proof.
Lemma totalfst_display {A: Type} (Bf: ∑ B, B -> A) : totalfst (display Bf) = Bf.
Show proof.
use total2_paths_f.
- apply weqtopaths. apply sum_of_fibers.
- rewrite transportf_fun.
rewrite <- eqweqmap_transportb.
rewrite eqweqmap_pathsinv0.
rewrite eqweqmap_weqtopaths.
reflexivity.
- apply weqtopaths. apply sum_of_fibers.
- rewrite transportf_fun.
rewrite <- eqweqmap_transportb.
rewrite eqweqmap_pathsinv0.
rewrite eqweqmap_weqtopaths.
reflexivity.
Lemma display_totalfst {A: Type} (P: A -> Type) : display(totalfst(P)) = P.
Show proof.
Lemma display_weq (A:Type) :
(∑ B, B -> A) ≃ (A -> Type).
Show proof.
exists display.
apply (isweq_iso display totalfst).
- exact totalfst_display.
- exact display_totalfst.
apply (isweq_iso display totalfst).
- exact totalfst_display.
- exact display_totalfst.