HoTT : Construct a fiber bundle (fiber space = Bool, base space = S1), and prove the total space is homotopy equivalent to S1 itself.

S1B.v

Require Import Overture PathGroupoids Equivalences Trunc HProp HSet.
Require Import types.Unit types.Paths types.Sigma types.Forall types.Arrow.
Require Import types.Bool types.Universe Misc.
Require Import hit.Circle.
Local Open Scope path_scope.
Local Open Scope equiv_scope.

Instance isequiv_negb' : @IsEquiv@{Type Type} Bool Bool negb.
Proof.
    refine (@BuildIsEquiv
              _ _
              negb negb
              (fun b => if b as b return negb (negb b) = b then idpath else idpath)
              (fun b => if b as b return negb (negb b) = b then idpath else idpath)
              _).
    intros []; simpl; exact idpath.
Defined.

Section AssumeUnivalence.
Context `{Univalence}.
Context `{Funext}.

Definition Twisted_Bool : S1 -> Type :=
  S1_rectnd Type Bool (path_universe negb).

Definition S1B : Type := sig Twisted_Bool.

Lemma S1B_loop_transport_negb b : transport Twisted_Bool loop b = negb b.
Proof.
  refine (transport_idmap_ap _ _ _ _ _ _ @ _).
  refine (ap (fun x => transport idmap x b) (S1_rectnd_beta_loop _ _ _) @ _).
  apply transport_path_universe.
Qed.

Lemma S1B_loopV_transport_negb b : transport Twisted_Bool loop ^ b = negb b.
Proof.
  apply moveR_transport_V.
  rewrite S1B_loop_transport_negb.
  destruct b; reflexivity.
Qed.

Definition S1B_loop b : (base; b) = (base; negb b) :> S1B.
Proof.
  (* refine (path_sigma _ (base; b) (base; negb b) loop _). *)
  refine (path_sigma' _ loop _).
  apply S1B_loop_transport_negb.
Defined.

Definition S1_to_S1B : S1 -> S1B.
Proof.
  refine (S1_rectnd S1B (base; false) _).
  refine (@concat _ _ (base; true) _ _ _).
  - apply S1B_loop.
  - apply S1B_loop.
Defined.

Definition S1B_to_S1_curried : forall (x:S1), Twisted_Bool x -> S1.
Proof.
  refine (S1_rect (fun x => Twisted_Bool x -> S1) (fun _ => base) _).
  apply path_forall.
  intros b.
  refine (transport_arrow _ _ _ @ _).
  refine (transport_const _ _ @ _).
  destruct b.
  - refine loop.
  - refine 1.
Defined.

Definition S1B_to_S1 : S1B -> S1.
Proof.
  apply sig_rect, S1B_to_S1_curried.
Defined.

Lemma ap_S1B_to_S1_S1B_loop b :
  ap S1B_to_S1 (S1B_loop b) = if b then 1 else loop.
Proof.
  unfold S1B_loop.
  unfold S1B_to_S1.
  rewrite (ap_sigT_rectnd_path_sigma Twisted_Bool _ _ loop).
  simpl.
  hott_simpl.
  unfold compose; rewrite ap_const; hott_simpl.
  unfold S1B_to_S1_curried.
  rewrite S1_rect_beta_loop.
  simpl; hott_simpl.
  rewrite ap10_path_forall.
  hott_simpl.
  rewrite S1B_loop_transport_negb.
  destruct b; reflexivity.
Qed.

Lemma S1B_loop_another b :
  path_sigma' Twisted_Bool loop 1 =
    S1B_loop b @ ap (exist _ base) (S1B_loop_transport_negb b)^.
Proof.
  unfold S1B_loop.
  destruct (S1B_loop_transport_negb b).
  hott_simpl.
Qed.

Definition pull_halfloop : forall b : Bool, (base; false) = (base; b) :> S1B.
Proof.
  intros [|].
  - apply inverse, S1B_loop.
  - apply 1.
Defined.

Definition S1B_to_S1_isequiv : IsEquiv S1B_to_S1.
Proof.
  refine (isequiv_adjointify S1B_to_S1 S1_to_S1B _ _).
  - hnf.
    refine (S1_rect _ 1 _).
    refine (transport_paths_FFlr _ _ @ _).
    rewrite concat_p1.
    cut (ap S1B_to_S1 (ap S1_to_S1B loop) = loop);
      [intros Hl; rewrite Hl; apply concat_Vp |].
    unfold S1_to_S1B.
    rewrite S1_rectnd_beta_loop.
    rewrite (ap_pp _ _).
    rewrite ap_S1B_to_S1_S1B_loop.
    change (ap S1B_to_S1 (S1B_loop false) @ 1 = loop).
    rewrite ap_S1B_to_S1_S1B_loop.
    apply concat_p1.
  - hnf.
    intros [].
    refine (S1_rect
              (fun x => forall b, S1_to_S1B (S1B_to_S1 (x; b)) = (x; b))
              pull_halfloop _).
    apply path_forall.
    intros b.
    rewrite transport_forall.
    rewrite (transportD_is_transport Twisted_Bool
              (fun y => S1_to_S1B (S1B_to_S1 y) = y)).
    rewrite S1B_loop_another.
    rewrite transport_pp.
    rewrite (transport_compose (fun y => S1_to_S1B (S1B_to_S1 y) = y)).
    rewrite <-transport_pp.
    rewrite <-ap_pp.
    generalize (transport_pV Twisted_Bool loop b).
    rewrite S1B_loopV_transport_negb.
    intros p.
    simpl; hott_simpl.
    destruct b.
    + simpl; hott_simpl.
      rewrite (set_path2 _ (idpath true)), ap_1, transport_1.
      rewrite transport_paths_FFlr.
      hott_simpl.
      rewrite ap_V, ap_V, ap_S1B_to_S1_S1B_loop.
      unfold S1_to_S1B.
      rewrite S1_rectnd_beta_loop.
      rewrite inv_pp.
      hott_simpl.
    + simpl; hott_simpl.
      rewrite (set_path2 _ (idpath false)), ap_1, transport_1.
      rewrite transport_paths_FFlr.
      hott_simpl.
      rewrite ap_V, ap_V, ap_S1B_to_S1_S1B_loop.
      hott_simpl.
Qed.