Require Import HoTT.Basics HoTT.Types.
Require Import HFiber.
Require Import Truncations.
Require Import Universes.BAut.

Local Open Scope trunc_scope.
Local Open Scope path_scope.

Class IsRigid (A : Type) :=
  path_aut_rigid : ∀ f g : A <~> A, f == g.

Global Instance contr_aut_rigid `{Funext} (A : Type) `{IsRigid A}
  : Contr (A <~> A).
Proof.
  apply (Build_Contr _ equiv_idmap).
  intros f; apply path_equiv, path_arrow, path_aut_rigid.
Defined.

Global Instance contr_baut_rigid `{Univalence} {A : Type} `{IsRigid A}
  : Contr (BAut A).
Proof.
  refine (contr_change_center (point (BAut A))).
  refine (contr_trunc_conn (Tr 0)).
  apply istrunc_S.
  intros Z W; baut_reduce.
  refine (istrunc_equiv_istrunc (n := -1) (A <~> A)
                      (path_baut (point (BAut A)) (point (BAut A)))).
Defined.

Definition rigid_contr_Baut `{Univalence} {A : Type} `{Contr (BAut A)}
  : IsRigid A.
Proof.
  unfold IsRigid.
  equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) f.
  equiv_intro ((path_baut (point (BAut A)) (point (BAut A)))^-1) g.
  apply ap10, ap, ap, path_contr.
Defined.

Global Instance rigid_ishprop
       (A : Type) `{IsHProp A} : IsRigid A.
Proof.
  intros f g x; apply path_ishprop.
Defined.

Definition aut_homomorphism_end `{Funext} {X Y : Type}
           (M : (X → X) → (Y → Y))
           (Mid : M idmap == idmap)
           (MC : ∀ f g, M (g o f) == M g o M f)
  : (X <~> X) → (Y <~> Y).
Proof.
  assert (MS : ∀ f g, g o f == idmap → (M g) o (M f) == idmap).
  { intros g f s x.
    transitivity (M (f o g) x).
    + symmetry. refine (MC g f x).
    + transitivity (M idmap x).
      × apply ap10, ap, path_arrow.
        intros y; apply s.
      × apply Mid. }
  assert (ME : (∀ f, IsEquiv f → IsEquiv (M f))).
  { intros f ?.
    refine (isequiv_adjointify (M f) (M f^-1) _ _);
      apply MS; [ apply eisretr | apply eissect ]. }
  exact (fun f ⇒ (Build_Equiv _ _ (M f) (ME f _))).
Defined.

Definition baut_prod_rigid_equiv `{Univalence}
           (X A : Type) (n : trunc_index)
           `{IsTrunc n.+1 X} `{IsRigid A} `{IsConnected n.+1 A}
  : BAut X <~> BAut (X × A).
Proof.
  refine (Build_Equiv _ _ (baut_prod_r X A) _).
  apply isequiv_surj_emb.
  { apply BuildIsSurjection; intros Z.
    baut_reduce.
    refine (tr (point _ ; _)).
    apply path_sigma_hprop; reflexivity. }
  { apply isembedding_isequiv_ap.
    intros Z W.
    pose (L := fun e : Z <~> W ⇒ equiv_functor_prod_r (B := A) e).
    refine (isequiv_commsq
             L (ap (baut_prod_r X A))
             (path_baut Z W)
             (path_baut (baut_prod_r X A Z) (baut_prod_r X A W))
             (fun e ⇒ (ap_baut_prod_r X A e)^)).
    refine ((isconnected_elim (Tr (-1)) (A := A) _ _).1).
    { apply contr_inhabited_hprop;
        [ exact _ | refine (merely_isconnected n A) ]. }
    intros a0.
    baut_reduce.
    pose (M := fun f:X×A → X×A ⇒ fun x ⇒ fst (f (x,a0))).
    assert (MH : ∀ (a:A) (f:X×A → X×A) (x:X),
               fst (f (x,a)) = fst (f (x,a0))).
    { refine (conn_map_elim (Tr n) (unit_name a0) _ _).
      intros; reflexivity. }
    assert (MC : ∀ (f g :X×A → X×A), M (g o f) == M g o M f).
    { intros f g x; unfold M.
      transitivity (fst (g (fst (f (x,a0)), snd (f (x,a0))))).
      - reflexivity.
      - apply MH. }
    pose (M' := aut_homomorphism_end M (fun x ⇒ 1) MC).
    assert (Mker : ∀ f, M' f == 1%equiv → f == 1%equiv).
    { unfold M', M; cbn. intros f p.
      pose (fh := fun x a ⇒ (MH a f x) @ p x).
      pose (g := fun x a ⇒ snd (f (x,a))).
      assert (ge : ∀ x, IsEquiv (g x)).
      { apply isequiv_from_functor_sigma.
        refine (isequiv_commsq' _ f
                  (equiv_sigma_prod0 X A) (equiv_sigma_prod0 X A) _).
        intros [x a]; cbn.
        apply path_prod; [ apply fh | reflexivity ]. }
      intros [x a].
      pose (gisid := path_aut_rigid (Build_Equiv _ _ (g x) (ge x)) 1).
      apply path_prod.
      - apply fh.
      - apply gisid. }
    assert (Minj : ∀ f g, M' f == M' g → f == g).
    { intros f g p z.
      apply moveL_equiv_M.
      revert z.
      refine (Mker (g^-1 oE f) _).
      intros x.
      refine (MC f g^-1 x @ _).
      change ((M' g)^-1 (M f x) = x).
      apply moveR_equiv_V, p. }
    refine (isequiv_adjointify L M' _ _);
      intros e;
      apply path_equiv, path_arrow;
      try apply Minj;
      intros x; reflexivity. }
Defined.