Torus/*: update comments and naming

theories/Spaces/Torus/Torus.v

@@ -1,8 +1,7 @@
 Require Import Basics.
 Require Import Cubical.
 
-(* In this file we define the Torus as a HIT generated by two loops and
-   a square between them. *)
+(** In this file we define the Torus as a HIT generated by two loops and a square between them. *)
 
 Notation hr := (sq_refl_h _).
 Notation vr := (sq_refl_v _).
@@ -16,13 +15,13 @@ Module Export Torus.
   Axiom loop_b : tbase = tbase.
   Axiom surf : PathSquare loop_a loop_a loop_b loop_b.
 
-  (* We define the induction principle for Torus *)
+  (** We define the induction principle for Torus *)
   Definition Torus_ind (P : Torus -> Type) (pb : P tbase)
     (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
     (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x
   := (match x with tbase => fun _ _ _ => pb end) pla plb ps.
 
-  (* We declare propsitional computational rules for loop_a and loop_b *)
+  (** We declare propositional computational rules for loop_a and loop_b *)
   Axiom Torus_ind_beta_loop_a : forall (P : Torus -> Type) (pb : P tbase)
     (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
     (ps : DPathSquare P surf pla pla plb plb), DPathSquare P hr
@@ -33,9 +32,7 @@ Module Export Torus.
     (ps : DPathSquare P surf pla pla plb plb), DPathSquare P hr
       (dp_apD (Torus_ind P pb pla plb ps) (loop_b)) plb 1%dpath 1%dpath.
 
-  (* We write out the computation rule for surf even though we will not
-     use it. Instead we currently have an unfinished recursion computation
-     principle, but we don't currently know how to derive it from this *)
+  (** We write out the computation rule for surf even though we will not use it. Instead we currently have an unfinished recursion computation principle, but we don't currently know how to derive it from this *)
   Axiom Torus_ind_beta_surf : forall (P : Torus -> Type) (pb : P tbase)
     (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
     (ps : DPathSquare P surf pla pla plb plb),
@@ -45,12 +42,12 @@ Module Export Torus.
 
 End Torus.
 
-(* We can now define Torus recursion as a sepcial case of Torus induction *)
+(** We can now define Torus recursion as a special case of Torus induction *)
 Definition Torus_rec (P : Type) (pb : P) (pla plb : pb = pb)
   (ps : PathSquare pla pla plb plb) : Torus -> P
   := Torus_ind _ pb (dp_const pla) (dp_const plb) (ds_const ps).
 
-(* We can derive the recursion computation rules for Torus_rec *)
+(** We can derive the recursion computation rules for Torus_rec *)
 Lemma Torus_rec_beta_loop_a (P : Type) (pb : P) (pla plb : pb = pb)
   (ps : PathSquare pla pla plb plb)
   : PathSquare (ap (Torus_rec P pb pla plb ps) loop_a) pla 1 1.
@@ -69,9 +66,7 @@ Proof.
   apply moveR_equiv_V, dp_apD_const.
 Defined.
 
-(* We ought to be able to prove this from Torus_ind_beta_surf
-   but it is currently too difficult. Therefore we will leave it
-   as admitted where it will simply look like an axiom. *)
+(** We ought to be able to prove this from Torus_ind_beta_surf but it is currently too difficult. Therefore we will leave it as admitted where it will simply look like an axiom. *)
 Definition Torus_rec_beta_surf (P : Type) (pb : P) (pla plb : pb = pb)
   (ps : PathSquare pla pla plb plb)
   :  PathCube (sq_ap (Torus_rec P pb pla plb ps) surf) ps

theories/Spaces/Torus/TorusEquivCircles.v

@@ -2,9 +2,9 @@ Require Import Basics Types.
 Require Import Cubical.
 Require Import Spaces.Circle Spaces.Torus.Torus.
 
-(* In this file we prove that the Torus is equivalent to the product of two circles. *)
+(** In this file we prove that the torus is equivalent to the product of two circles. *)
 
-(* Here is a cube filler for help with circle recursion into the torus *)
+(** Here is a cube filler for help with circle recursion into the torus *)
 Definition c2t_square_and_cube
   : {s : PathSquare loop_a loop_a
       (ap (Circle_rec _ tbase loop_b) loop)
@@ -16,7 +16,7 @@ Proof.
   apply cu_fill_left.
 Defined.
 
-(* We define the map from the Torus to the Circles *)
+(** We define the map from the Torus to the Circles *)
 Definition t2c : Torus -> Circle * Circle.
 Proof.
   snrapply Torus_rec.
@@ -26,7 +26,8 @@ Proof.
   + exact (sq_prod (hr, vr)). (* The square is the obvious product of squares *)
 Defined.
 
-(* We now define the curried function from the circles to the torus *)
+(** We now define the curried function from the circles to the torus. *)
+(** TODO: It's easy to remove [Funext] from this definition by using [intro] and [revert] appropriately, but then the cube algebra in the proof of [c2t'_beta] would need to be updated. See https://github.com/HoTT/Coq-HoTT/pull/1824. *)
 Definition c2t' `{Funext} : Circle -> Circle -> Torus.
 Proof.
   snrapply Circle_rec.
@@ -40,13 +41,13 @@ Proof.
       apply (pr1 c2t_square_and_cube). (* We apply the cap we found above *)
 Defined.
 
-(* Here is the uncurried version *)
+(** Here is the uncurried version *)
 Definition c2t `{Funext} : Circle * Circle -> Torus.
 Proof.
   apply uncurry, c2t'.
 Defined.
 
-(* Computation rules for c2t' as a cube filler *)
+(** Computation rules for c2t' as a cube filler *)
 Definition c2t'_beta `{Funext} :
   {bl1 : PathSquare (ap (fun y => c2t' base y) loop) loop_b 1 1 &
   {bl2 : PathSquare (ap (fun x => c2t' x base) loop) loop_a 1 1 &
@@ -78,7 +79,7 @@ Defined.
 Local Open Scope path_scope.
 Local Open Scope cube_scope.
 
-(* We now prove that t2c is a section of c2t *)
+(** We now prove that t2c is a section of c2t *)
 Definition t2c2t `{Funext} : c2t o t2c == idmap.
 Proof.
   (* We start with Torus induction *)
@@ -138,7 +139,7 @@ Proof.
   by destruct p, q.
 Defined.
 
-(* We now prove t2c is a retraction of c2t *)
+(** We now prove t2c is a retraction of c2t *)
 Definition c2t2c `{Funext} : t2c o c2t == idmap.
 Proof.
   nrapply prod_ind.

theories/Spaces/Torus/TorusHomotopy.v

@@ -16,14 +16,14 @@ Local Open Scope pointed_scope.
 
 (** The torus is 1-truncated *)
 
-Global Instance is1type_Torus `{Univalence} : IsTrunc 1 Torus.
+Global Instance is1type_torus `{Univalence} : IsTrunc 1 Torus.
 Proof.
   refine (istrunc_equiv_istrunc _ equiv_torus_prod_Circle^-1).
 Qed.
 
 (** The torus is 0-connected *)
 
-Global Instance isconnected_Torus `{Univalence} : IsConnected 0 Torus.
+Global Instance isconnected_torus `{Univalence} : IsConnected 0 Torus.
 Proof.
   srapply (isconnected_equiv' _ _ equiv_torus_prod_Circle^-1).
   srapply (isconnected_equiv' _ _ (equiv_sigma_prod0 _ _)).
@@ -33,15 +33,17 @@ Qed.
 Local Notation T := ([Torus, _]).
 Local Notation S1 := ([Circle, _]).
 
+(** A pointed version of the equivalence from TorusEquivCircles.v. *)
+(** TODO: If [Funext] is removed from there, remove it from here as well. *)
 Lemma pequiv_torus_prod_circles `{Funext} : T  <~>* S1 * S1.
 Proof.
   srapply Build_pEquiv'.
   1: apply equiv_torus_prod_Circle.
   reflexivity.
 Defined.
 
-(** Fundamental group of Torus *)
-Theorem Pi1Torus `{Univalence}
+(** Fundamental group of torus *)
+Theorem pi1_torus `{Univalence}
   : GroupIsomorphism (Pi 1 T) (grp_prod abgroup_Z abgroup_Z).
 Proof.
   etransitivity.
@@ -52,10 +54,10 @@ Proof.
   1,2: apply pi1_circle.
 Defined.
 
-(** Loop space of Torus *)
+(** Loop space of torus *)
 Theorem loops_torus `{Univalence} : loops T <~>* Int * Int.
 Proof.
   (* Since [T] is 1-truncated, [loops T] is 0-truncated, and is therefore equivalent to its 0-truncation. *)
   refine (_ o*E pequiv_ptr (n:=0)).
-  nrapply Pi1Torus.
+  nrapply pi1_torus.
 Defined.