README.md

@@ -99,4 +99,4 @@ More information can be found in the [Wiki][22].
 [20]: https://code.visualstudio.com/
 [21]: https://github.com/coq-community/vscoq
 
-[22]: https://github.com/HoTT/HoTT/wiki
+[22]: https://github.com/HoTT/HoTT/wiki

STYLE.md

@@ -3,7 +3,7 @@
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 <!-- *generated with [DocToc](https://github.com/thlorenz/doctoc)* -->
 <!-- Ali: VSCode is able to do the TOC using the "Markdown All in One" extension. Section numbering too! -->
-## Table of Contents 
+## Table of Contents
 
 - [1. Conventions And Style Guide](#1-conventions-and-style-guide)
   - [1.1. Organization](#11-organization)
@@ -676,7 +676,7 @@ in `bar` appropriately.
 
 (It is possible to explicitly declare and name universes globally with
 the `Universe` command, but we are not using that in the HoTT
-library.  Universes declared with `Universe` will be discharged on each 
+library.  Universes declared with `Universe` will be discharged on each
 section definition independently.)
 
 Unfortunately it is not currently possible to declare the universe
@@ -1124,7 +1124,7 @@ where they are defined.
   The unification algorithm used by `apply` is different and often
   less powerful than the one used by `refine`, though it is
   occasionally better at pattern matching.
- 
+
   Here are some tips:
   - If `apply` fails with a unification error you think it shouldn't
     have, try `rapply`.
@@ -1135,7 +1135,7 @@ where they are defined.
   - If you don't want Coq to create evars for certain subgoals,
     add an `s` to the tactic name to make it use `simple refine`.
 
-  
+
 ## 1.12. Contributing to the library ##
 
 ### 1.12.1. Fork & Pull ###

contrib/SetoidRewrite.v

@@ -99,7 +99,7 @@ Proof.
   intros f1 f2.
   apply (is0functor_postcomp a b c g ).
 Defined.
-                  
+
 #[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
   {a b c : A}
   : CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
@@ -111,7 +111,7 @@ Proof.
   exact eq_g.
 Defined.
 
-#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A} 
+#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A}
   {R : Relation B} (F : A -> B)
   `{CMorphisms.Proper _ (GpdHom ==> R) F}
   : CMorphisms.Proper (Hom ==> R) F.
@@ -194,7 +194,7 @@ Defined.
 
 Proposition nat_equiv_faithful {A B : Type}
   {F G : A -> B} `{Is1Functor _ _ F}
-  `{!Is0Functor G, !Is1Functor G} 
+  `{!Is0Functor G, !Is1Functor G}
   `{!HasEquivs B} (tau : NatEquiv F G)
   : Faithful F -> Faithful G.
 Proof.

etc/Book.py

@@ -190,7 +190,7 @@ def die(msg):
         content = content[content.index('\n')+1:]
         # Update Book_X_Y_Z
         book = "_".join(map(str,entry['number']))
-        # content = re.sub('Book_[0-9_]*[0-9]', 'Book_{0}'.format(book), content) 
+        # content = re.sub('Book_[0-9_]*[0-9]', 'Book_{0}'.format(book), content)
         # content = re.sub('Definition Book_[0-9_]*[0-9]', 'Definition Book_{0}'.format(book), content)
         # previous two removed since they break Exercise 2.2 and 2.3
         # It is a common error to write things like Lemma_X_Y_Z instead of Book_X_Y_Z,

etc/coqcreplace.py

@@ -169,7 +169,7 @@ def replace(vfile):
             if not match:
                 break
             lines[i] = replace_match(match, coqc_replace, lines[i])
-            
+
             attempts += 1
             with open(vfile, 'w', encoding="utf-8") as f:
                 f.write(''.join(lines))

etc/fix_trailing_whitespace.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+
+# This command removes trailing whitespace from all files in the repository.
+
+git grep -l -z -E '\s+$' | xargs -0 sed -i 's/\s\+$//'

etc/generate_coqproject.sh

@@ -10,7 +10,7 @@ else
 fi
 
 ## List untracked .v files
-#UNTRACKED_V_FILES=$(git ls-files --others --exclude-standard "*.v") 
+#UNTRACKED_V_FILES=$(git ls-files --others --exclude-standard "*.v")
 
 ## Combine untracked and tracked .v files
 printf -v UNSORTED_V_FILES '%s\n%s' "$TRACKED_V_FILES" "$UNTRACKED_V_FILES"

etc/homotopy.css

@@ -2,7 +2,7 @@
    text in crazy fonts and colors. */
 
 body { padding: 0px 0px;
-       margin: 0px 0px; 
+       margin: 0px 0px;
        background-color: white }
 
 #page { display: block;
@@ -18,7 +18,7 @@ body { padding: 0px 0px;
           border-bottom-style: solid;
           border-width: thin }
 
-#header h1 { padding: 0; 
+#header h1 { padding: 0;
              margin: 0;}
 
 
@@ -45,28 +45,28 @@ body { padding: 0px 0px;
 #main .keyword { color : #cf1d1d }
 #main { color: black }
 
-.section {padding-top: 13px; 
-           padding-bottom: 13px; 
-           padding-left: 3px; 
+.section {padding-top: 13px;
+           padding-bottom: 13px;
+           padding-left: 3px;
            margin-top: 5px;
            margin-bottom: 5px;
            font-size : 175% }
 
-h2.section {padding-left: 3px; 
-             padding-top: 12px; 
-             padding-bottom: 10px; 
+h2.section {padding-left: 3px;
+             padding-top: 12px;
+             padding-bottom: 10px;
              font-size : 130% }
 
-h3.section {padding-left: 3px; 
-             padding-top: 7px; 
-             padding-bottom: 7px; 
+h3.section {padding-left: 3px;
+             padding-top: 7px;
+             padding-bottom: 7px;
              font-size : 115% }
 
-h4.section { 
+h4.section {
                    background-color: white;
-                   padding-left: 0px; 
-                   padding-top: 0px; 
-                   padding-bottom: 0px; 
+                   padding-left: 0px;
+                   padding-top: 0px;
+                   padding-bottom: 0px;
                    font-size : 100%;
                    font-style : bold;
                    text-decoration : underline;
@@ -81,45 +81,45 @@ h4.section {
 	     padding-bottom: 10px;
              border-style: plain}
 
-.inlinecode { 
+.inlinecode {
     display: inline;
 /*    font-size: 125%; */
     color: #666666;
-    font-family: monospace } 
+    font-family: monospace }
 
-.doc .inlinecode { 
+.doc .inlinecode {
     display: inline;
-    font-size: 120%; 
+    font-size: 120%;
     color: rgb(30%,30%,70%);
-    font-family: monospace } 
+    font-family: monospace }
 
-.doc .inlinecode .id { 
-    color: rgb(30%,30%,70%); 
-} 
+.doc .inlinecode .id {
+    color: rgb(30%,30%,70%);
+}
 
-.inlinecodenm { 
+.inlinecodenm {
     display: inline;
     color: #444444;
 }
 
-.doc .code { 
+.doc .code {
     display: inline;
-    font-size: 120%; 
-    color: rgb(30%,30%,70%); 
-    font-family: monospace } 
+    font-size: 120%;
+    color: rgb(30%,30%,70%);
+    font-family: monospace }
 
-.comment { 
+.comment {
     display: inline;
     font-family: monospace;
-    color: rgb(50%,50%,80%); 
-} 
+    color: rgb(50%,50%,80%);
+}
 
-.code { 
+.code {
     display: block;
 /*  padding-left: 15px; */
-    font-size: 110%; 
+    font-size: 110%;
     font-family: monospace;
- } 
+ }
 
 table.infrule {
   border: 0px;
@@ -141,7 +141,7 @@ tr.infrulemiddle hr {
 }
 
 .infrulenamecol {
-    color: rgb(60%,60%,60%); 
+    color: rgb(60%,60%,60%);
     font-size: 80%;
     padding-left: 1em;
     padding-bottom: 0.1em
@@ -154,55 +154,55 @@ tr.infrulemiddle hr {
 
 .id { display: inline; }
 
-.id[type="constructor"] { 
+.id[type="constructor"] {
     color: rgb(60%,0%,0%);
 }
 
-.id[type="var"] { 
+.id[type="var"] {
     color: rgb(40%,0%,40%);
 }
 
-.id[type="variable"] { 
+.id[type="variable"] {
     color: rgb(40%,0%,40%);
 }
 
-.id[type="definition"] { 
+.id[type="definition"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="abbreviation"] { 
+.id[type="abbreviation"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="lemma"] { 
+.id[type="lemma"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="instance"] { 
+.id[type="instance"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="projection"] { 
+.id[type="projection"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="method"] { 
+.id[type="method"] {
     color: rgb(0%,40%,0%);
 }
 
-.id[type="inductive"] { 
+.id[type="inductive"] {
     color: rgb(0%,0%,80%);
 }
 
-.id[type="record"] { 
+.id[type="record"] {
     color: rgb(0%,0%,80%);
 }
 
-.id[type="class"] { 
+.id[type="class"] {
     color: rgb(0%,0%,80%);
 }
 
-.id[type="keyword"] { 
+.id[type="keyword"] {
  color : #cf1d1d;
 /*     color: black; */
 }

test/Algebra/Groups/Presentation.v

@@ -6,4 +6,4 @@ Local Open Scope mc_mult_scope.
 Check ⟨ x | x * x * x , -x ⟩.
 Check ⟨ x , y | x * y ,  x * y * x , x * (-y) * x * x * x⟩.
 Check ⟨ x , y , z | x * y * z , x * -z , x * y⟩.
- 
+

test/Metatheory/FunextVarieties.v

@@ -1,4 +1,4 @@
-From HoTT.Metatheory Require Import FunextVarieties. 
+From HoTT.Metatheory Require Import FunextVarieties.
 
 (** Checking the universes of FunextVarieties.v *)
 

theories/Algebra/AbGroups/Abelianization.v

@@ -30,7 +30,7 @@ From this we can show that Abel G is an abelian group.
 
 In fact this models the following HIT:
 
-HIT Abel (G : Group) := 
+HIT Abel (G : Group) :=
  | ab : G -> Abel G
  | ab_comm : forall x y z, ab (x * (y * z)) = ab (x * (z * y)).
 
@@ -77,7 +77,7 @@ Section Abel.
   Global Instance istrunc_abel : IsHSet Abel := _.
 
   (** We can derive the induction principle from the ones for truncation and the coequalizer. *)
-  Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)} 
+  Definition Abel_ind (P : Abel -> Type) `{forall x, IsHSet (P x)}
     (a : forall x, P (ab x)) (c : forall x y z, DPath P (ab_comm x y z)
       (a (x * (y * z))) (a (x * (z * y))))
     : forall (x : Abel), P x.
@@ -111,7 +111,7 @@ Section Abel.
   Defined.
 
   (** Here is a simpler version of Abel_ind when our target is an HProp. This lets us discard all the higher paths. *)
-  Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)} 
+  Definition Abel_ind_hprop (P : Abel -> Type) `{forall x, IsHProp (P x)}
     (a : forall x, P (ab x)) : forall (x : Abel), P x.
   Proof.
     srapply (Abel_ind _ a).

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -2,7 +2,7 @@ Require Import Basics Types HSet HFiber Limits.Pullback.
 Require Import WildCat Pointed.Core Homotopy.ExactSequence.
 Require Import Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.AbPullback AbGroups.Biproduct.
-Require Import AbSES.Core AbSES.Pullback. 
+Require Import AbSES.Core AbSES.Pullback.
 Require Import Modalities.Identity Modalities.Modality Truncations.Core.
 
 Local Open Scope pointed_scope.

theories/Algebra/AbSES/Pushout.v

@@ -195,7 +195,7 @@ Proof.
     + exact (ap (fun x => _ + g1.1 x) (grp_unit_l _)^).
 Defined.
 
-Definition abses_pushout_path_data_1 `{Univalence} {A A' B : AbGroup} (f : A $-> A') {E : AbSES B A} 
+Definition abses_pushout_path_data_1 `{Univalence} {A A' B : AbGroup} (f : A $-> A') {E : AbSES B A}
   : fmap (abses_pushout f) (Id E) = Id (abses_pushout f E).
 Proof.
   srapply path_sigma_hprop.
@@ -243,7 +243,7 @@ Proof.
   - snrefine (ab_pushout_rec ab_biprod_inl _ _).
     + exact (functor_ab_biprod f grp_homo_id).
     + reflexivity.
-  - intro a'. 
+  - intro a'.
     apply path_prod.
     + simpl.
       exact (ap _ (grp_homo_unit f) @ right_identity _).

theories/Algebra/Groups/FreeGroup.v

@@ -52,7 +52,7 @@ Section Reduction.
 
   Local Notation "[ x ]" := (word_sing x).
 
-  (** Now we wish to define the free group on A as the following HIT: 
+  (** Now we wish to define the free group on A as the following HIT:
 
     HIT N(A) : hSet
      | eta : Words -> N(A)