HoTT · jdchristensen · Sep 26, 2024 · Sep 26, 2024
diff --git a/.dir-locals.el b/.dir-locals.el
@@ -0,0 +1 @@
+((nil . ((mode . visual-line))))
diff --git a/STYLE.md b/STYLE.md
@@ -1025,9 +1025,9 @@ window that is narrower than the width to which you filled it.  If
 editing in Emacs, turn off `auto-fill-mode` and turn on
 `visual-line-mode`; then you'll be able to read comment paragraphs
 without scrolling horizontally, no matter how narrow your window is.
-Some files contain `(* -*- mode: coq; mode: visual-line -*- *)` at the
-top, which does this automatically; feel free to add it to files that
-are missing it.
+The repository contains a file .dir-locals.el in the top-level directory
+which turns on `visual-line-mode` when emacs visits any file in the
+repository.
 
 Unfortunately, when viewing source code on Github, these long comment
 lines are not wrapped, making them hard to read.  If you use the

diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (* Typeclass instances to allow rewriting in categories. Examples are given later in the file. *)
 
 (* Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database. It must be imported before Basics.Overture. *)

diff --git a/theories/Algebra/Aut.v b/theories/Algebra/Aut.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.

diff --git a/theories/Algebra/ooAction.v b/theories/Algebra/ooAction.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.
 Require Import Algebra.ooGroup.
 

diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.

diff --git a/theories/Basics/Contractible.v b/theories/Basics/Contractible.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Contractibility *)
 
 Require Import Overture PathGroupoids.

diff --git a/theories/Basics/Decidable.v b/theories/Basics/Decidable.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import
   Basics.Overture
   Basics.PathGroupoids

diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Equivalences *)
 
 Require Import

diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Basic definitions of homotopy type theory *)
 
 (** This file defines some of the most basic types and type formers, such as sums, products, Sigma types and path types.  It defines the action of functions on paths [ap], transport, equivalences, and function extensionality.  It also defines truncatedness, and a number of other fundamental definitions used throughout the library. *)

diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * The groupid structure of paths *)
 
 Require Import Basics.Overture Basics.Tactics.

diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * Truncatedness *)
 
 Require Import

diff --git a/theories/Colimits/MappingCylinder.v b/theories/Colimits/MappingCylinder.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Mapping Cylinders *)
 
 Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare.

diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.
 Require Export Colimits.Coeq.

diff --git a/theories/Constant.v b/theories/Constant.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions Factorization.
 Require Import Truncations.Core Modalities.Modality.

diff --git a/theories/Equiv/BiInv.v b/theories/Equiv/BiInv.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope path_scope.

diff --git a/theories/Equiv/PathSplit.v b/theories/Equiv/PathSplit.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

diff --git a/theories/Equiv/Relational.v b/theories/Equiv/Relational.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

diff --git a/theories/EquivGroupoids.v b/theories/EquivGroupoids.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (** * The pregroupoid structure of [Equiv] *)
 
 Require Import Basics.Overture Basics.Equivalences Types.Equiv.

diff --git a/theories/Extensions.v b/theories/Extensions.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Extensions and extendible maps *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Factorization.v b/theories/Factorization.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Factorizations and factorization systems. *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/HFiber.v b/theories/HFiber.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types Diagrams.CommutativeSquares HSet.
 
 Local Open Scope equiv_scope.

diff --git a/theories/HIT/Flattening.v b/theories/HIT/Flattening.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The flattening lemma. *)
 
 Require Import HoTT.Basics.

diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Spaces.Int Spaces.Circle.
 Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.

diff --git a/theories/HIT/Interval.v b/theories/HIT/Interval.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import Basics.Overture Basics.PathGroupoids.

diff --git a/theories/HIT/SetCone.v b/theories/HIT/SetCone.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics Types.Unit.
 Require Import Colimits.Pushout.
 Require Import Truncations.Core.

diff --git a/theories/HIT/V.v b/theories/HIT/V.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * The cumulative hierarchy [V]. *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/HIT/quotient.v b/theories/HIT/quotient.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HSet TruncType.
 Require Import Truncations.Core.

diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics Types.
 Require Import SuccessorStructure.
 Require Import WildCat.

diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import Cubical.

diff --git a/theories/Idempotents.v b/theories/Idempotents.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Constant.
 Require Import Truncations.Core Modalities.Modality.

diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber PathAny Cubical.PathSquare.
 Require Import Diagrams.CommutativeSquares.

diff --git a/theories/Metatheory/Core.v b/theories/Metatheory/Core.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 Require Import HoTT.Basics HoTT.Types.
 
 (** * Metatheory *)

diff --git a/theories/Metatheory/FunextVarieties.v b/theories/Metatheory/FunextVarieties.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Varieties of function extensionality *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Metatheory/ImpredicativeTruncation.v b/theories/Metatheory/ImpredicativeTruncation.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Impredicative truncations. *)
 
 Require Import HoTT.Basics.

diff --git a/theories/Metatheory/IntervalImpliesFunext.v b/theories/Metatheory/IntervalImpliesFunext.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about the homotopical interval. *)
 
 Require Import HoTT.Basics.

diff --git a/theories/Metatheory/Nat.v b/theories/Metatheory/Nat.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Defining the natural numbers from univalence and propresizing. *)
 Require Import Basics.
 Require Import Types.

diff --git a/theories/Metatheory/TruncImpliesFunext.v b/theories/Metatheory/TruncImpliesFunext.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Theorems about trunctions *)
 
 Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool.

diff --git a/theories/Metatheory/UnivalenceVarieties.v b/theories/Metatheory/UnivalenceVarieties.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Varieties of univalence *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Misc.v b/theories/Misc.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** * Miscellaneous material *)
 
 (** If you have a lemma or group of lemmas that you can’t find a better home for, put them here.  However, big “Miscellaneous” files are sub-optimal to work with, so some caveats:

diff --git a/theories/Modalities/Accessible.v b/theories/Modalities/Accessible.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Accessible subuniverses and modalities *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Modalities/Closed.v b/theories/Modalities/Closed.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible Nullification Lex Topological.

diff --git a/theories/Modalities/CoreflectiveSubuniverse.v b/theories/Modalities/CoreflectiveSubuniverse.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modalities.Modality Modalities.Open.
 

diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Extensions Limits.Pullback.
 Require Import Modality Accessible Modalities.Localization.

diff --git a/theories/Modalities/Fracture.v b/theories/Modalities/Fracture.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions Limits.Pullback.
 Require Import Modality Lex Open Closed Nullification.

diff --git a/theories/Modalities/Identity.v b/theories/Modalities/Identity.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality Accessible.
 

diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Limits.Pullback Factorization Truncations.Core.
 Require Import Modality Accessible Modalities.Localization Descent Separated.

diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Localization *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Modalities/Meet.v b/theories/Modalities/Meet.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback.
 Require Import Descent Lex Separated.

diff --git a/theories/Modalities/Modality.v b/theories/Modalities/Modality.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HFiber Extensions Factorization Limits.Pullback.
 Require Export ReflectiveSubuniverse. (* [Export] because many of the lemmas and facts about reflective subuniverses are equally important for modalities. *)

diff --git a/theories/Modalities/Notnot.v b/theories/Modalities/Notnot.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Modality.
 

diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 (** * Nullification *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Modalities/Open.v b/theories/Modalities/Open.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible Nullification Lex.

diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback.
 Require Import PathAny.

diff --git a/theories/Modalities/Separated.v b/theories/Modalities/Separated.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath.
 Require Import HFiber Extensions Factorization Limits.Pullback.
 Require Import Modality Accessible Descent.

diff --git a/theories/Modalities/Topological.v b/theories/Modalities/Topological.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions HoTT.Truncations.
 Require Import Accessible Lex Nullification.

diff --git a/theories/NullHomotopy.v b/theories/NullHomotopy.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import Types.Sigma.
 Local Open Scope path_scope.

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import PathAny.
 Require Import WildCat.

diff --git a/theories/Spaces/BAut/Bool.v b/theories/Spaces/BAut/Bool.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Constant.
 Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness.

diff --git a/theories/Spaces/BAut/Bool/IncoherentIdempotent.v b/theories/Spaces/BAut/Bool/IncoherentIdempotent.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Equiv.BiInv Idempotents.
 Require Import Universes.BAut Spaces.BAut.Bool.

diff --git a/theories/Spaces/BAut/Cantor.v b/theories/Spaces/BAut/Cantor.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import Idempotents.
 Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.

diff --git a/theories/Spaces/Cantor.v b/theories/Spaces/Cantor.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 
 Local Open Scope nat_scope.

diff --git a/theories/Spaces/Card.v b/theories/Spaces/Card.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 (** Representation of cardinals, see Chapter 10 of the HoTT book. *)
 Require Import HoTT.Universes.TruncType.
 Require Import HoTT.Classes.interfaces.abstract_algebra.

diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
 Require Import HSet.

diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.

diff --git a/theories/Spaces/Finite/Finite.v b/theories/Spaces/Finite/Finite.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.
 Require Import Types.
 Require Import HSet.

diff --git a/theories/Spaces/Finite/Tactics.v b/theories/Spaces/Finite/Tactics.v
@@ -1,4 +1,3 @@
-
 Require Import HoTT.Basics Fin.
 
 (** ** Tactics *)

diff --git a/theories/Spaces/No/Addition.v b/theories/Spaces/No/Addition.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.
 

diff --git a/theories/Spaces/No/Core.v b/theories/Spaces/No/Core.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
 Require Import TruncType HSet.
 Require Import HoTT.Truncations.Core.

diff --git a/theories/Spaces/No/Negation.v b/theories/Spaces/No/Negation.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics.
 Require Import HoTT.Spaces.No.Core.
 

diff --git a/theories/Spaces/Spheres.v b/theories/Spaces/Spheres.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics Types.
 Require Import WildCat.Equiv.
 Require Import NullHomotopy.

diff --git a/theories/Spaces/TwoSphere.v b/theories/Spaces/TwoSphere.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
 
 Local Open Scope path_scope.

diff --git a/theories/Spectra/Spectrum.v b/theories/Spectra/Spectrum.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*- *)
-
 (** * Spectra *)
 
 Require Import HoTT.Basics HoTT.Types.

diff --git a/theories/Tactics.v b/theories/Tactics.v
@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Contractible Basics.Equivalences.
 Require Import Types.Prod Types.Forall.
 Require Export Tactics.BinderApply.
Original file line number	Diff line number	Diff line change
		@@ -1,4 +1,3 @@

		Require Import HoTT.Basics Fin.

		( Tactics *)
Expand Down