address review comments

Signed-off-by: Ali Caglayan <[email protected]>

Author: Alizter

theories/Homotopy/Hopf.v

@@ -23,7 +23,7 @@ Proof.
   srapply Build_pFam.
   - apply (Susp_rec (Y:=Type) X X).
     (** In order to use the flattening lemma for colimits to show that the total space is a join, we need for this equivalence to be a composition with the inverted identity equivalence so that the fiber is definitionally equivalent to the flattening lemma sigma type. This doesn't change anything elsewhere, but saves us having to rewrite an IsEquiv witness. *)
-    exact (fun x => path_universe ((x *.) o equiv_idmap^-1)).
+    exact (fun x => path_universe ((x *.) o equiv_idmap)).
   - simpl. exact pt.
 Defined.
 
@@ -106,14 +106,18 @@ Proof.
   rapply freudenthal_hspace.
 Defined.
 
-(** *** Total space of the Hopf fibration *)
+(** *** Total space of the Hopf construction *)
 
-(** The total space of the Hopf fibration on [Susp X] is the join of [X] with itself. Note that we need both left and right multiplication to be equivalences. This is true when [X] is a 0-connected H-space for example. *)
+(** The total space of the Hopf construction on [Susp X] is the join of [X] with itself. Note that we need both left and right multiplication to be equivalences. This is true when [X] is a 0-connected H-space for example. *)
 (* TODO: Show that this is a pointed equivalence. We cannot yet do this as we cannot compute with the flattening lemma due to the massive size of the proof. *)
 Definition equiv_hopf_total_join `{Univalence} (X : pType)
   `{IsHSpace X} `{forall a, IsEquiv (a *.)} `{forall a, IsEquiv (.* a)}
-  : psigma (hopf_construction X) <~> pjoin X X.
+  : psigma (hopf_construction X) <~>* pjoin X X.
 Proof.
+  symmetry.
+  snrapply Build_pEquiv'.
+  2: shelve.
+  symmetry.
   snrefine (_ oE (pushout_flattening (f:=const_tt X) (g:=const_tt X) _
     (Unit_ind (pointed_type X)) (Unit_ind (pointed_type X)) (fun _ => equiv_idmap)
     (fun x => Build_Equiv _ _ (fun y => sg_op x y) (H1 x)))^-1%equiv).
@@ -124,11 +128,31 @@ Proof.
     snrapply Build_Equiv.
     + exact (.* x).
     + exact _.
-  - rapply equiv_sigma_unit_ind.
-  - rapply equiv_sigma_unit_ind.
-  - simpl.
-    hnf.
-    reflexivity.
-  - intros [x y].
-    reflexivity.
-Defined.
+  - exact (equiv_contr_sigma (Unit_ind (pointed_type X))).
+  - exact (equiv_contr_sigma (Unit_ind (pointed_type X))).
+  - hnf; reflexivity.
+  - hnf; reflexivity.
+  Unshelve.
+  unfold "pt".
+  Opaque pushout_flattening.
+  simpl.
+  Transparent pushout_flattening.
+  unfold pushout_flattening.
+  unfold "pt".
+  rapply (moveR_equiv_V' (equiv_functor_sigma' _ _)). 
+  Opaque Colimit_Pushout_Flattening.PO_flattening.
+  Opaque flattening_coh_2.
+  simpl.
+  unfold functor_sigma.
+  simpl.
+  unfold Colimit.functor_colimit.
+  simpl.
+  unfold Colimit.cocone_postcompose_inv.
+  unfold Cocone.cocone_postcompose.
+  simpl.
+  apply moveR_equiv_M'.
+
+
+    
+Admitted.
+     

theories/Types/Unit.v

@@ -117,15 +117,3 @@ Definition contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A
 
 (** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when [const tt] is used in a context that doesn't have [Universe Minimization ToSet] as this file does. If we ever set that globally, then we could get rid of this and remove some imports of this file. *)
 Definition const_tt (A : Type) := @const A Unit tt.
-
-(** Families over Unit type are equivalent to the type at the base point. *)
-Lemma equiv_sigma_unit_ind (P : Unit -> Type)
-  : sig P <~> P tt.
-Proof.
-  simple refine (equiv_adjointify _ _ _ _).
-  - intros [[] p]; exact p.
-  - intros p; exists tt; exact p.
-  - reflexivity.
-  - intros [[] p].
-    reflexivity.
-Defined.