Library UniMath.MoreFoundations.Univalence
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.PartA.
Funextsec and toforallpaths are mutually inverses
Lemma funextsec_toforallpaths {T : UU} {P : T -> UU} {f g : ∏ t : T, P t} :
∏ (h : f = g), funextsec _ _ _ (toforallpaths _ _ _ h) = h.
Show proof.
Lemma toforallpaths_funextsec {T : UU} {P : T -> UU} {f g : ∏ t : T, P t} :
∏ (h : ∏ t : T, f t = g t), toforallpaths _ _ _ (funextsec _ _ _ h) = h.
Show proof.
Definition toforallpaths_funextsec_comp {T : UU} {P : T -> UU} (f g : ∏ t, P t) :
toforallpaths P f g ∘ funextsec P f g = idfun _.
Show proof.
Lemma maponpaths_funextsec {T : UU} {P : T -> UU}
(f g : ∏ t, P t) (t : T) (p : f ~ g) :
maponpaths (λ h, h t) (funextsec _ f g p) = p t.
Show proof.
Definition weqonsec {X Y} (P:X->Type) (Q:Y->Type)
(f:X ≃ Y) (g:∏ x, weq (P x) (Q (f x))) :
(∏ x:X, P x) ≃ (∏ y:Y, Q y).
Show proof.
Definition weq_transportf {X} (P:X->Type) {x y:X} (p:x = y) : (P x) ≃ (P y).
Show proof.
Definition weq_transportf_comp {X} (P:X->Type) {x y:X} (p:x = y) (f:∏ x, P x) :
weq_transportf P p (f x) = f y.
Show proof.
Definition weqonpaths2 {X Y} (w:X ≃ Y) {x x':X} {y y':Y} :
w x = y -> w x' = y' -> (x = x') ≃ (y = y').
Show proof.
Definition eqweqmap_ap {T} (P:T->Type) {t t':T} (e:t = t') (f:∏ t:T, P t) :
eqweqmap (maponpaths P e) (f t) = f t'. Show proof.
Definition eqweqmap_ap' {T} (P:T->Type) {t t':T} (e:t = t') (f:∏ t:T, P t) :
invmap (eqweqmap (maponpaths P e)) (f t') = f t. Show proof.
∏ (h : f = g), funextsec _ _ _ (toforallpaths _ _ _ h) = h.
Show proof.
Lemma toforallpaths_funextsec {T : UU} {P : T -> UU} {f g : ∏ t : T, P t} :
∏ (h : ∏ t : T, f t = g t), toforallpaths _ _ _ (funextsec _ _ _ h) = h.
Show proof.
Definition toforallpaths_funextsec_comp {T : UU} {P : T -> UU} (f g : ∏ t, P t) :
toforallpaths P f g ∘ funextsec P f g = idfun _.
Show proof.
Lemma maponpaths_funextsec {T : UU} {P : T -> UU}
(f g : ∏ t, P t) (t : T) (p : f ~ g) :
maponpaths (λ h, h t) (funextsec _ f g p) = p t.
Show proof.
intermediate_path (toforallpaths _ _ _ (funextsec _ f g p) t).
- generalize (funextsec _ f g p); intros q.
induction q.
reflexivity.
- apply (eqtohomot (eqtohomot (toforallpaths_funextsec_comp f g) p) t).
- generalize (funextsec _ f g p); intros q.
induction q.
reflexivity.
- apply (eqtohomot (eqtohomot (toforallpaths_funextsec_comp f g) p) t).
Definition weqonsec {X Y} (P:X->Type) (Q:Y->Type)
(f:X ≃ Y) (g:∏ x, weq (P x) (Q (f x))) :
(∏ x:X, P x) ≃ (∏ y:Y, Q y).
Show proof.
Definition weq_transportf {X} (P:X->Type) {x y:X} (p:x = y) : (P x) ≃ (P y).
Show proof.
Definition weq_transportf_comp {X} (P:X->Type) {x y:X} (p:x = y) (f:∏ x, P x) :
weq_transportf P p (f x) = f y.
Show proof.
intros. induction p. reflexivity.
Definition weqonpaths2 {X Y} (w:X ≃ Y) {x x':X} {y y':Y} :
w x = y -> w x' = y' -> (x = x') ≃ (y = y').
Show proof.
Definition eqweqmap_ap {T} (P:T->Type) {t t':T} (e:t = t') (f:∏ t:T, P t) :
eqweqmap (maponpaths P e) (f t) = f t'. Show proof.
intros. induction e. reflexivity.
Definition eqweqmap_ap' {T} (P:T->Type) {t t':T} (e:t = t') (f:∏ t:T, P t) :
invmap (eqweqmap (maponpaths P e)) (f t') = f t. Show proof.
intros. induction e. reflexivity.
weak equivalences
Definition pr1_eqweqmap { X Y } ( e: X = Y ) : cast e = pr1 (eqweqmap e).
Show proof.
intros. induction e. reflexivity.
Definition path_to_fun {X Y} : X=Y -> X->Y.
Show proof.
Definition pr1_eqweqmap2 { X Y } ( e: X = Y ) :
pr1 (eqweqmap e) = transportf (λ T:Type, T) e.
Show proof.
intros. induction e. reflexivity.
Definition weqpath_transport {X Y} (w : X ≃ Y) :
transportf (idfun UU) (weqtopaths w) = pr1 w.
Show proof.
Definition weqpath_cast {X Y} (w : X ≃ Y) : cast (weqtopaths w) = w.
Show proof.
Definition switch_weq {X Y} (f:X ≃ Y) {x y} : y = f x -> invweq f y = x.
Show proof.
Definition switch_weq' {X Y} (f:X ≃ Y) {x y} : invweq f y = x -> y = f x.
Show proof.
Local Open Scope transport.
Definition weq_over_sections {S T} (w:S ≃ T)
{s0:S} {t0:T} (k:w s0 = t0)
{P:T->Type}
(p0:P t0) (pw0:P(w s0)) (l:k#pw0 = p0)
(H:(∏ t, P t) -> UU)
(J:(∏ s, P(w s)) -> UU)
(g:∏ f:(∏ t, P t), weq (H f) (J (maponsec1 P w f))) :
weq (hfiber (λ fh:total2 H, pr1 fh t0) p0 )
(hfiber (λ fh:total2 J, pr1 fh s0) pw0).
Show proof.
intros. simple refine (weqbandf _ _ _ _).
{ simple refine (weqbandf _ _ _ _).
{ exact (weqonsecbase P w). }
{ unfold weqonsecbase; simpl. exact g. } }
{ intros [f h]. simpl. unfold maponsec1; simpl.
induction k, l; simpl. unfold transportf; simpl.
apply idweq. }
{ simple refine (weqbandf _ _ _ _).
{ exact (weqonsecbase P w). }
{ unfold weqonsecbase; simpl. exact g. } }
{ intros [f h]. simpl. unfold maponsec1; simpl.
induction k, l; simpl. unfold transportf; simpl.
apply idweq. }
Definition maponpaths_app_homot
{X Y₁ Y₂ : UU}
{f g : Y₁ → X → Y₂}
(p : ∏ (z : Y₁ × X), f (pr1 z) (pr2 z) = g (pr1 z) (pr2 z))
(x : X)
(y : Y₁)
: maponpaths (λ f, f x) (app_homot p y)
=
p (y ,, x).
Show proof.
Definition path_path_fun
{X Y : UU}
{f g : X → Y}
{e₁ e₂ : f = g}
(h : ∏ (x : X), eqtohomot e₁ x = eqtohomot e₂ x)
: e₁ = e₂.
Show proof.
refine (!(@funextsec_toforallpaths X (λ _, Y) f g e₁) @ _).
refine (_ @ @funextsec_toforallpaths X (λ _, Y) f g e₂).
apply maponpaths.
use funextsec.
intro x.
apply h.
refine (_ @ @funextsec_toforallpaths X (λ _, Y) f g e₂).
apply maponpaths.
use funextsec.
intro x.
apply h.