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.
Proof.
  intros [f [g [p [q h]]]]. ∃ g. unfold isweq. intro x.
  ∃ (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)).
Defined.

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).
Proof.
  intros. unfold iscontrretract. destruct is as [ctr uni].
  simpl. reflexivity.
Defined.

Definition iscontrweqb_compute {X Y} (w:X ≃ Y) (is:iscontr Y) :
  iscontrpr1 (iscontrweqb w is) = invmap w (iscontrpr1 is).
Proof.
  intros. unfold iscontrweqb. rewrite iscontrretract_compute.
  reflexivity.
Defined.

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).
Proof.
  intros. destruct is as [ctr uni]. reflexivity.
Defined.

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.
Proof.
  intros. reflexivity.
Defined.

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).
Proof.
  intros. reflexivity.
Defined.

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.
Proof.
  intros. destruct is as [ctr uni]. reflexivity.
Defined.

Definition iscontrcoconustot_comp {X} {x:X} :
  iscontrpr1 (iscontrcoconustot X x) = x,,idpath x.
Proof.
  reflexivity.
Defined.

Definition funfibtototal {X} (P Q:X→Type) (f:∏ x:X, P x → Q x) :
  total2 P → total2 Q.
Proof.
  intros [x p]. exact (x,,f x p).
Defined.

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)).
Proof.
  intros. apply funextsec; intros [x q]. reflexivity.
Defined.

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.
Proof.
  intros. destruct e. reflexivity.
Defined.

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.
Proof.
  intros. destruct e. reflexivity.
Defined.

Definition weqpr1_irr_sec {X} {P:X→Type}
           (irr:∏ x (p q:P x), p = q) (sec:∏ x, P x) : weq (total2 P) X.
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. }
Defined.

Definition invweqpr1_irr_sec {X} {P:X→Type}
           (irr:∏ x (p q:P x), p = q) (sec:∏ x, P x) : X ≃ (total2 P).
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. }
Defined.

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.
Proof.
  revert w; intros [x p]. apply pair_path_in2. apply irr.
Defined.

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))).
Proof.
  reflexivity. Defined.

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))).
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.
Defined.

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.
Proof.
  intros. destruct ni, mi, l. simpl. rewrite pathscomp0rid. reflexivity.
Defined.

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.
Proof.
  intros. destruct ni, mi, l. simpl. rewrite pathscomp0rid. reflexivity.
Defined.