chore: Fix markdown list formatting (#1047)

Removes double line breaks in lists as it makes them display with too much spacing. The following is for testing purposes: Co-authored-by: VojtechStep <vojtechstepancik@outlook.com>
UniMath · Mar 1, 2024 · bbab819 · bbab819
1 parent 106965f
commit bbab819
Show file tree

Hide file tree

Showing 19 changed files with 0 additions and 22 deletions.
diff --git a/FILE-CONVENTIONS.md b/FILE-CONVENTIONS.md
@@ -173,7 +173,6 @@ contents of the file.
 ## See also
 
 - For a template file see [`TEMPLATE.lagda.md`](TEMPLATE.lagda.md).
-
 - An instructive example of a file with the expected structure is
   [`order-theory.galois-connections`](https://raw.githubusercontent.com/UniMath/agda-unimath/master/src/order-theory/galois-connections.lagda.md).
 

diff --git a/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md b/src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md
@@ -266,7 +266,6 @@ module _
 
 - [Set-magmoids](category-theory.set-magmoids.md) capture the structure of
   composition operations on binary families of sets.
-
 - [Precategories](category-theory.precategories.md) are associative and unital
   composition operations on binary families of sets.
 - [Nonunital precategories](category-theory.nonunital-precategories.md) are

diff --git a/src/category-theory/conservative-functors-precategories.lagda.md b/src/category-theory/conservative-functors-precategories.lagda.md
@@ -102,7 +102,6 @@ module _
 ## See also
 
 - [Essentially injective functors](category-theory.essentially-injective-functors-precategories.md)
-
 - [Pseudomonic functors](category-theory.pseudomonic-functors-precategories.md)
   are conservative.
 - [Fully faithful functors](category-theory.fully-faithful-functors-precategories.md)

diff --git a/src/category-theory/replete-subprecategories.lagda.md b/src/category-theory/replete-subprecategories.lagda.md
@@ -315,7 +315,6 @@ This remains to be formalized.
 ## See also
 
 - Every [subcategory](category-theory.subcategories.md) is replete.
-
 - Because of universe polymorphism,
   [large subcategories](category-theory.large-subcategories.md) are not large
   replete by construction, although they are levelwise replete.

diff --git a/src/foundation-core/functoriality-dependent-function-types.lagda.md b/src/foundation-core/functoriality-dependent-function-types.lagda.md
@@ -133,7 +133,6 @@ module _
   [`foundation.type-arithmetic-dependent-function-types`](foundation.type-arithmetic-dependent-function-types.md).
 - Equality proofs in dependent function types are characterized in
   [`foundation.equality-dependent-function-types`](foundation.equality-dependent-function-types.md).
-
 - Functorial properties of function types are recorded in
   [`foundation.functoriality-function-types`](foundation.functoriality-function-types.md).
 - Functorial properties of dependent pair types are recorded in

diff --git a/src/foundation-core/functoriality-dependent-pair-types.lagda.md b/src/foundation-core/functoriality-dependent-pair-types.lagda.md
@@ -445,7 +445,6 @@ module _
   [`foundation.equality-dependent-pair-types`](foundation.equality-dependent-pair-types.md).
 - The universal property of dependent pair types is treated in
   [`foundation.universal-property-dependent-pair-types`](foundation.universal-property-dependent-pair-types.md).
-
 - Functorial properties of cartesian product types are recorded in
   [`foundation.functoriality-cartesian-product-types`](foundation.functoriality-cartesian-product-types.md).
 - Functorial properties of dependent product types are recorded in

diff --git a/src/foundation/equality-dependent-function-types.lagda.md b/src/foundation/equality-dependent-function-types.lagda.md
@@ -96,6 +96,5 @@ module _
   [`foundation.equality-cartesian-product-types`](foundation.equality-cartesian-product-types.md).
 - Equality proofs in dependent pair types are characterized in
   [`foundation.equality-dependent-pair-types`](foundation.equality-dependent-pair-types.md).
-
 - Function extensionality is postulated in
   [`foundation.function-extensionality`](foundation.function-extensionality.md).
diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md
@@ -261,7 +261,6 @@ module _
   [`foundation.equality-cartesian-product-types`](foundation.equality-cartesian-product-types.md).
 - The universal property of cartesian product types is treated in
   [`foundation.universal-property-cartesian-product-types`](foundation.universal-property-cartesian-product-types.md).
-
 - Functorial properties of dependent pair types are recorded in
   [`foundation.functoriality-dependent-pair-types`](foundation.functoriality-dependent-pair-types.md).
 - Functorial properties of dependent product types are recorded in

diff --git a/src/foundation/functoriality-coproduct-types.lagda.md b/src/foundation/functoriality-coproduct-types.lagda.md
@@ -547,7 +547,6 @@ module _
   [`foundation.equality-coproduct-types`](foundation.equality-coproduct-types.md).
 - The universal property of coproducts is treated in
   [`foundation.universal-property-coproduct-types`](foundation.universal-property-coproduct-types.md).
-
 - Functorial properties of cartesian product types are recorded in
   [`foundation.functoriality-cartesian-product-types`](foundation.functoriality-cartesian-product-types.md).
 - Functorial properties of dependent pair types are recorded in

diff --git a/src/foundation/functoriality-dependent-function-types.lagda.md b/src/foundation/functoriality-dependent-function-types.lagda.md
@@ -294,7 +294,6 @@ pr2 (automorphism-Π e f) = is-equiv-map-automorphism-Π e f
   [`foundation.type-arithmetic-dependent-function-types`](foundation.type-arithmetic-dependent-function-types.md).
 - Equality proofs in dependent function types are characterized in
   [`foundation.equality-dependent-function-types`](foundation.equality-dependent-function-types.md).
-
 - Functorial properties of function types are recorded in
   [`foundation.functoriality-function-types`](foundation.functoriality-function-types.md).
 - Functorial properties of dependent pair types are recorded in

diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md
@@ -540,7 +540,6 @@ module _
   [`foundation.equality-dependent-pair-types`](foundation.equality-dependent-pair-types.md).
 - The universal property of dependent pair types is treated in
   [`foundation.universal-property-dependent-pair-types`](foundation.universal-property-dependent-pair-types.md).
-
 - Functorial properties of cartesian product types are recorded in
   [`foundation.functoriality-cartesian-product-types`](foundation.functoriality-cartesian-product-types.md).
 - Functorial properties of dependent product types are recorded in

diff --git a/src/foundation/inhabited-types.lagda.md b/src/foundation/inhabited-types.lagda.md
@@ -225,6 +225,5 @@ is-contr-is-inhabited-is-prop {A = A} p h =
 - The notion of _nonempty types_ is treated in
   [`foundation.empty-types`](foundation.empty-types.md). In particular, every
   inhabited type is nonempty.
-
 - For the notion of _pointed types_, see
   [`structured-types.pointed-types`](structured-types.pointed-types.md).
diff --git a/src/foundation/type-arithmetic-cartesian-product-types.lagda.md b/src/foundation/type-arithmetic-cartesian-product-types.lagda.md
@@ -156,7 +156,6 @@ pr2 (equiv-add-redundant-prop is-prop-B f) =
   [`foundation.equality-cartesian-product-types`](foundation.equality-cartesian-product-types.md).
 - The universal property of cartesian product types is treated in
   [`foundation.universal-property-cartesian-product-types`](foundation.universal-property-cartesian-product-types.md).
-
 - Arithmetical laws involving dependent pair types are recorded in
   [`foundation.type-arithmetic-dependent-pair-types`](foundation.type-arithmetic-dependent-pair-types.md).
   - Arithmetical laws involving dependent product types are recorded in

diff --git a/src/foundation/type-arithmetic-coproduct-types.lagda.md b/src/foundation/type-arithmetic-coproduct-types.lagda.md
@@ -345,7 +345,6 @@ module _
   [`foundation.equality-coproduct-types`](foundation.equality-coproduct-types.md).
 - The universal property of coproducts is treated in
   [`foundation.universal-property-coproduct-types`](foundation.universal-property-coproduct-types.md).
-
 - Arithmetical laws involving dependent pair types are recorded in
   [`foundation.type-arithmetic-dependent-pair-types`](foundation.type-arithmetic-dependent-pair-types.md).
 - Arithmetical laws involving cartesian-product types are recorded in

diff --git a/src/foundation/type-arithmetic-dependent-function-types.lagda.md b/src/foundation/type-arithmetic-dependent-function-types.lagda.md
@@ -68,7 +68,6 @@ module _
   [`foundation.functoriality-dependent-function-types`](foundation.functoriality-dependent-function-types.md).
 - Equality proofs in dependent function types are characterized in
   [`foundation.equality-dependent-function-types`](foundation.equality-dependent-function-types.md).
-
 - Arithmetical laws involving cartesian product types are recorded in
   [`foundation.type-arithmetic-cartesian-product-types`](foundation.type-arithmetic-cartesian-product-types.md).
 - Arithmetical laws involving dependent pair types are recorded in
@@ -79,7 +78,6 @@ module _
   [`foundation.type-arithmetic-unit-type`](foundation.type-arithmetic-unit-type.md).
 - Arithmetical laws involving the empty type are recorded in
   [`foundation.type-arithmetic-empty-type`](foundation.type-arithmetic-empty-type.md).
-
 - In
   [`foundation.universal-property-empty-type`](foundation.universal-property-empty-type.md)
   we show that `empty` is the initial type, which can be considered a _left zero

diff --git a/src/foundation/type-arithmetic-dependent-pair-types.lagda.md b/src/foundation/type-arithmetic-dependent-pair-types.lagda.md
@@ -425,7 +425,6 @@ right-distributive-product-Σ {A} =
   [`foundation.equality-dependent-pair-types`](foundation.equality-dependent-pair-types.md).
 - The universal property of dependent pair types is treated in
   [`foundation.universal-property-dependent-pair-types`](foundation.universal-property-dependent-pair-types.md).
-
 - Arithmetical laws involving cartesian product types are recorded in
   [`foundation.type-arithmetic-cartesian-product-types`](foundation.type-arithmetic-cartesian-product-types.md).
 - Arithmetical laws involving dependent product types are recorded in

diff --git a/src/structured-types/central-h-spaces.lagda.md b/src/structured-types/central-h-spaces.lagda.md
@@ -44,5 +44,3 @@ is-central-h-space A =
 - Ulrik Buchholtz, Daniel Christensen, Jarl G. Taxerås Flaten, Egbert Rijke,
   _Central H-spaces and banded types_
   ([arXiv:2301.02636](https://arxiv.org/abs/2301.02636))
-
--
diff --git a/src/structured-types/pointed-types.lagda.md b/src/structured-types/pointed-types.lagda.md
@@ -49,6 +49,5 @@ ev-point-Pointed-Type A f = f (point-Pointed-Type A)
 
 - The notion of _nonempty types_ is treated in
   [`foundation.empty-types`](foundation.empty-types.md).
-
 - The notion of _inhabited types_ is treated in
   [`foundation.inhabited-types`](foundation.inhabited-types.md).
diff --git a/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md b/src/synthetic-homotopy-theory/1-acyclic-types.lagda.md
@@ -156,11 +156,9 @@ module _
 - \[BCDE21\]: Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó. Free
   groups in HoTT/UF in Agda.
   <https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html>. 2021.
-
 - \[MRR88\]: Ray Mines, Fred Richman and Wim Ruitenburg. A Course in
   Constructive Algebra. Universitext. Springer, 1988.
   [doi:10.1007/978-1-4419-8640-5](https://doi.org/10.1007/978-1-4419-8640-5).
-
 - \[Wär23\]: David Wärn. Path spaces of pushouts. Preprint.
   <https://dwarn.se/po-paths.pdf>. 2023.