Library UniMath.MoreFoundations.MoreEquivalences

Equivalences

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.MoreFoundations.Equivalences.

Definition weq_to_InverseEquivalence X Y : X ≃ Y -> Equivalence Y X.
  intros [f r].
  unfold isweq in r.
  set (g := λ y , hfiberpr1 f y (pr1 (r y))).
  set (p := λ y , pr2 (pr1 (r y))).
  simpl in p.
  set (L := λ x , pr2 (r (f x)) (make_hfiber f x (idpath (f x)))).
  set (q := λ x , maponpaths pr1 (L x)).
  set (q' := λ x , !q x).
  refine (makeEquivalence Y X g f q' p _).
  intro y.
  admit.
Abort.

Definition Equivalence_to_invweq X Y : Equivalence X Y -> Y ≃ X.
Show proof.

  intros [f [g [p [q h]]]]. exists g. unfold isweq. intro x.
  exists (f x,,q x). intros [y []]. apply (two_arg_paths_f (!p y)).
  admit.
Abort.

Definition weq_pathscomp0r {X} x {y z:X} (p:y = z) : (x = y ) ≃ (x = z ).
Proof.
  intros. exact (make_weq _ (isweqpathscomp0r _ p)).

Definition iscontrretract_compute {X Y} (p:X ->Y) (s:Y ->X)
(eps:∏ y : Y , p (s y) = y) (is:iscontr X) :
iscontrpr1 (iscontrretract p s eps is) = p (iscontrpr1 is).
Show proof.

intros. unfold iscontrretract. destruct is as [ctr uni].
simpl. reflexivity.

Definition iscontrweqb_compute {X Y} (w:X ≃ Y) (is:iscontr Y) :
iscontrpr1 (iscontrweqb w is) = invmap w (iscontrpr1 is).
Show proof.

intros. unfold iscontrweqb. rewrite iscontrretract_compute.
reflexivity.

Definition compute_iscontrweqb_weqfibtototal_1 {T} {P Q:T ->Type}
           (f:∏ t , (P t ) ≃ (Q t ))
           (is:iscontr (total2 Q)) :
  pr1 (iscontrpr1 (iscontrweqb (weqfibtototal P Q f) is)) = pr1 (iscontrpr1 is).
Show proof.

intros. destruct is as [ctr uni]. reflexivity.

Definition compute_pr1_invmap_weqfibtototal {T} {P Q:T ->Type}
           (f:∏ t , (P t ) ≃ (Q t ))
           (w:total2 Q) :
  pr1 (invmap (weqfibtototal P Q f) w) = pr1 w.
Show proof.

intros. reflexivity.

Definition compute_pr2_invmap_weqfibtototal {T} {P Q:T ->Type}
           (f:∏ t , (P t ) ≃ (Q t ))
           (w:total2 Q) :
  pr2 (invmap (weqfibtototal P Q f) w) = invmap (f (pr1 w)) (pr2 w).
Show proof.

intros. reflexivity.

Definition compute_iscontrweqb_weqfibtototal_3 {T} {P Q:T ->Type}
           (f:∏ t , (P t ) ≃ (Q t ))
           (is:iscontr (total2 Q)) :
  maponpaths pr1 (iscontrweqb_compute (weqfibtototal P Q f) is)
  =
  compute_iscontrweqb_weqfibtototal_1 f is.
Show proof.

intros. destruct is as [ctr uni]. reflexivity.

Definition iscontrcoconustot_comp {X} {x:X} :
iscontrpr1 (iscontrcoconustot X x) = x ,,idpath x.
Show proof.

reflexivity.

Definition funfibtototal {X} (P Q:X ->Type) (f:∏ x:X , P x -> Q x) :
total2 P -> total2 Q.
Show proof.

intros [x p]. exact (x,,f x p).

Definition weqfibtototal_comp {X} (P Q:X ->Type) (f:∏ x:X , (P x ) ≃ (Q x )) :
invmap (weqfibtototal P Q f) = funfibtototal Q P (λ x , invmap (f x)).
Show proof.

intros. apply funextsec; intros [x q]. reflexivity.

Definition eqweqmapap_inv {T} (P:T ->Type) {t u:T} (e:t = u) (p:P u) :
(eqweqmap (maponpaths P e)) ((eqweqmap (maponpaths P (!e))) p) = p.
Show proof.

intros. destruct e. reflexivity.

Definition eqweqmapap_inv' {T} (P:T ->Type) {t u:T} (e:t = u) (p:P t) :
(eqweqmap (maponpaths P (!e))) ((eqweqmap (maponpaths P e)) p) = p.
Show proof.

intros. destruct e. reflexivity.

Definition weqpr1_irr_sec {X} {P:X ->Type}
(irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x) : weq (total2 P) X.
Show proof.

  intros.
  set (isc := λ x , iscontraprop1 (invproofirrelevance _ (irr x)) (sec x)).
  apply Equivalence_to_weq.
  simple refine (makeEquivalence _ _ _ _ _ _ _).
  { exact pr1. }
  { intro x. exact (x,,sec x). }
  { intro x. reflexivity. }
  { intros [x p]. simpl. apply maponpaths. apply irr. }
  { intros [x p]. simpl. apply pair_path_in2_comp1. }

Definition invweqpr1_irr_sec {X} {P:X ->Type}
(irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x) : X ≃ (total2 P ).
Show proof.

  intros.
  set (isc := λ x , iscontraprop1 (invproofirrelevance _ (irr x)) (sec x)).
  apply Equivalence_to_weq.
  simple refine (makeEquivalence _ _ _ _ _ _ _).
  { intro x. exact (x,,sec x). }
  { exact pr1. }
  { intros [x p]. simpl. apply maponpaths. apply irr. }
  { intro x. reflexivity. }
  { intro x'. simpl. rewrite (irrel_paths (irr _) (irr _ _ _) (idpath (sec x'))).
    reflexivity. }

Definition homotinvweqweq' {X} {P:X ->Type}
(irr:∏ x (p q:P x ), p = q) (s:∏ x , P x) (w:total2 P) :
invmap (weqpr1_irr_sec irr s) (weqpr1_irr_sec irr s w) = w.
Show proof.

revert w; intros [x p]. apply pair_path_in2. apply irr.

Definition homotinvweqweq'_comp {X} {P:X ->Type}
           (irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x)
           (x:X) (p:P x) :
  let f := weqpr1_irr_sec irr sec in
  let w := x ,,p in
  let w' := invweq f x in
  @paths (w' = w)
            (homotinvweqweq' irr sec w)
            (maponpaths _ (irr x (sec x) (pr2 w))).
Show proof.

reflexivity.

Definition homotinvweqweq_comp {X} {P:X ->Type}
           (irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x)
           (x:X) (p:P x) :
  let f := weqpr1_irr_sec irr sec in
  let w := x ,,p in
  let w' := invweq f x in
  @paths (w' = w)
            (homotinvweqweq f w)
            (maponpaths _ (irr x (sec x) (pr2 w))).
Show proof.

  try reflexivity. Abort.

Definition homotinvweqweq_comp_3 {X} {P:X ->Type}
           (irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x)
           (x:X) (p:P x) :
  let f := weqpr1_irr_sec irr sec in
  let g := invweqpr1_irr_sec irr sec in
  let w := x ,,p in
  let w' := g x in
  @paths (w' = w)
            (homotweqinvweq g w)
            (maponpaths _ (irr x (sec x) (pr2 w))).
Proof.
  reflexivity.

Definition loop_correspondence {T X Y}
           (f:T ≃ X) (g:T ->Y)
           {t t':T} {l:t = t'}
           {m:f t = f t'} (mi:maponpaths f l = m)
           {n:g t = g t'} (ni:maponpaths g l = n) :
     maponpaths (funcomp (invmap f) g) m @ maponpaths g (homotinvweqweq f t')
  = maponpaths g (homotinvweqweq f t) @ n.
Show proof.

intros. destruct ni, mi, l. simpl. rewrite pathscomp0rid. reflexivity.

Definition loop_correspondence' {X Y} {P:X ->Type}
           (irr:∏ x (p q:P x ), p = q) (sec:∏ x , P x)
           (g:total2 P ->Y)
           {w w':total2 P} {l:w = w'}
           {m:weqpr1_irr_sec irr sec w = weqpr1_irr_sec irr sec w'} (mi:maponpaths (weqpr1_irr_sec irr sec) l = m)
           {n:g w = g w'} (ni:maponpaths g l = n) :
     maponpaths (funcomp (invmap (weqpr1_irr_sec irr sec)) g) m @ maponpaths g (homotinvweqweq' irr sec w')
  = maponpaths g (homotinvweqweq' irr sec w) @ n.
Show proof.

intros. destruct ni, mi, l. simpl. rewrite pathscomp0rid. reflexivity.