+
Reed
he/him
@@ -96,3 +93,18 @@ I like writing various forms of automation, especially those with a more
semantic flavor.
+
+
+
+
+
+I'm Naïm. I like the [computational trilogy](https://ncatlab.org/nlab/show/computational+trilogy)
+and arguing with Agda. I hate broken links and writing about myself.
+
+
diff --git a/src/Cat/Allegory/Morphism.lagda.md b/src/Cat/Allegory/Morphism.lagda.md
index 10b81626c..ffe4e8f15 100644
--- a/src/Cat/Allegory/Morphism.lagda.md
+++ b/src/Cat/Allegory/Morphism.lagda.md
@@ -1,7 +1,6 @@
diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md
index e4dd73267..35d856627 100644
--- a/src/Cat/Functor/Adjoint/Hom.lagda.md
+++ b/src/Cat/Functor/Adjoint/Hom.lagda.md
@@ -7,8 +7,6 @@ description: |
-Given a monoid $M$, we build a pointed precategory $B(M)$, where the
+Given a monoid $M$, we build a pointed precategory $\B{M}$, where the
endomorphism monoid of the point recovers $M$.
```agda
diff --git a/src/Cat/Instances/Discrete.lagda.md b/src/Cat/Instances/Discrete.lagda.md
index 86ecaa57d..667ce138e 100644
--- a/src/Cat/Instances/Discrete.lagda.md
+++ b/src/Cat/Instances/Discrete.lagda.md
@@ -61,7 +61,7 @@ lift-disc
lift-disc f .F₀ = f
lift-disc f .F₁ = ap f
lift-disc f .F-id = refl
-lift-disc f .F-∘ p q = ap-comp-path f q p
+lift-disc f .F-∘ p q = ap-∙ f q p
```
diff --git a/src/Cat/Restriction/Instances/Allegory.lagda.md b/src/Cat/Restriction/Instances/Allegory.lagda.md
index b0abbe8c8..c904ab353 100644
--- a/src/Cat/Restriction/Instances/Allegory.lagda.md
+++ b/src/Cat/Restriction/Instances/Allegory.lagda.md
@@ -1,8 +1,8 @@
@@ -112,7 +114,7 @@ data Cofibre {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (f : A → B) : Type
cone : ∀ a → tip ≡ base (f a)
```
-What's important here is that if a map $f$ has connected cofibre, then
+What's important here is that if a map $f$ has [[connected]] cofibre, then
it is a surjection --- so our proof that epis are surjective will factor
through showing that epis have connected cofibres^[note that all of
these types are propositions, so we have a bunch of equivalences].
@@ -120,7 +122,7 @@ these types are propositions, so we have a bunch of equivalences].
```agda
connected-cofibre→surjective
: ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} (f : A → B)
- → is-contr ∥ Cofibre f ∥₀
+ → is-connected (Cofibre f)
→ ∀ x → ∥ fibre f x ∥
connected-cofibre→surjective {A = A} {B = B} f conn x = transport cen (lift tt) where
```
@@ -169,7 +171,7 @@ inhabited), so it remains to show that any two points are merely equal.
epi→connected-cofibre
: ∀ {ℓ} (c d : n-Type ℓ 2) (f : ∣ c ∣ → ∣ d ∣)
→ Cr.is-epic (Sets ℓ) {c} {d} f
- → is-contr ∥ Cofibre f ∥₀
+ → is-connected (Cofibre f)
epi→connected-cofibre c d f epic = contr (inc tip) $
∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ w →
∥-∥₀-path.from (hom w)
diff --git a/src/Data/Set/Truncation.lagda.md b/src/Data/Set/Truncation.lagda.md
index 424dd4fd0..7eacc6797 100644
--- a/src/Data/Set/Truncation.lagda.md
+++ b/src/Data/Set/Truncation.lagda.md
@@ -29,6 +29,14 @@ data ∥_∥₀ {ℓ} (A : Type ℓ) : Type ℓ where
squash : is-set ∥ A ∥₀
```
+
+
We begin by defining the induction principle. The (family of) type(s) we
map into must be a set, as required by the `squash`{.Agda} constructor.
diff --git a/src/HoTT.lagda.md b/src/HoTT.lagda.md
index 8eb925e15..2fd46ef82 100644
--- a/src/HoTT.lagda.md
+++ b/src/HoTT.lagda.md
@@ -43,6 +43,7 @@ open import Data.Dec
open import Data.Nat using (ℕ-well-ordered ; Discrete-Nat)
open import Data.Sum
+open import Homotopy.Connectedness
open import Homotopy.Space.Circle
open import Homotopy.Space.Torus
open import Homotopy.Base
@@ -103,13 +104,13 @@ _ = Ωⁿ
* Lemma 2.2.1: `ap`{.Agda}
* Lemma 2.2.2:
- i. `ap-comp-path`{.Agda}
+ i. `ap-∙`{.Agda}
ii. _Definitional in cubical type theory_
iii. _Definitional in cubical type theory_
iv. _Definitional in cubical type theory_
@@ -321,7 +322,8 @@ _ = Singleton-is-contr
_ = equiv→is-hlevel
_ = ⊎-is-hlevel
_ = Σ-is-hlevel
-_ = contractible-if-inhabited
+_ = is-contr-if-inhabited→is-prop
+_ = is-prop→is-contr-if-inhabited
_ = H-Level-Dec
_ = disjoint-⊎-is-prop
_ = ℕ-well-ordered
@@ -333,7 +335,7 @@ _ = Finite-choice
* Exercise 3.1: `equiv→is-hlevel`{.Agda}
* Exercise 3.2: `⊎-is-hlevel`{.Agda}
* Exercise 3.3: `Σ-is-hlevel`{.Agda}
-* Exercise 3.5: `contractible-if-inhabited`{.Agda}
+* Exercise 3.5: `is-contr-if-inhabited→is-prop`{.Agda}, `is-prop→is-contr-if-inhabited`{.Agda}
* Exercise 3.6: `H-Level-Dec`{.Agda}
* Exercise 3.7: `disjoint-⊎-is-prop`{.Agda}
* Exercise 3.19: `ℕ-well-ordered`{.Agda}
@@ -582,6 +584,16 @@ _ = n-Tr-elim
* Lemma 7.3.2: `n-Tr-elim`{.Agda}
* Theorem 7.3.12: `n-Tr-path-equiv`{.Agda}
+### 7.5 Connectedness
+
+
+
+* Definition 7.5.1: `is-n-connected`{.Agda}
+
# Part 2 Mathematics
## Chapter 8 Homotopy theory
diff --git a/src/Homotopy/Base.lagda.md b/src/Homotopy/Base.lagda.md
index 59ccdc5a1..778e8f5e6 100644
--- a/src/Homotopy/Base.lagda.md
+++ b/src/Homotopy/Base.lagda.md
@@ -20,24 +20,14 @@ module Homotopy.Base where
This module contains the basic definitions for the study of synthetic
homotopy theory. Synthetic homotopy theory is the name given to studying
-$\infty$-groupoids in their own terms, i.e., the application of homotopy
+$\infty$-groupoids in their own terms, i.e., the application of homotopy type
theory to computing homotopy invariants of spaces. Central to the theory
-is the concept of _pointed type_ and _pointed map_. After all, [homotopy
+is the concept of [[pointed type]] and [[pointed map]]. After all, [homotopy
groups] are no more than the set-truncations of n-fold iterated loop
spaces, and loop spaces are always relative to a basepoint.
[homotopy groups]: Algebra.Group.Homotopy.html
-If we have pointed types $(A, a)$ and $(B, b)$, the most natural notion
-of function between them is not simply the type of functions $A \to B$,
-but rather those functions $A \to B$ which _preserve the basepoint_,
-i.e. the functions $f : A \to B$ equipped with paths $f(a) \equiv b$.
-
-```agda
-_→∙_ : ∀ {ℓ ℓ′} → Type∙ ℓ → Type∙ ℓ′ → Type _
-(A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] (f a ≡ b)
-```
-
A helper that will come in handy is `Σ∙`{.Agda}, which attaches the
north pole as the basepoint of the suspended space.
@@ -299,13 +289,15 @@ hubs-and-spokes→hlevel {A = A} (suc n) spheres x y =
```
-->
+:::{.definition #truncation}
Using this idea, we can define a general _$n$-truncation_ type, as a
joint generalisation of the [[propositional|propositional truncation]]
-and [set] truncations. While can not _directly_ build a type with a
+and [set] truncations. While we can not _directly_ build a type with a
constructor saying the type is $n$-truncated, what we _can_ do is freely
generate `hub`{.Agda}s and `spokes`{.Agda} for any $n$-sphere drawn on
-the $n$-truncation of $A$. The result is the universal $n$-type
+the $n$-truncation of $A$. The result is the universal $n$-type
admitting a map from $A$.
+:::
[set]: Data.Set.Truncation.html
diff --git a/src/Homotopy/Connectedness.lagda.md b/src/Homotopy/Connectedness.lagda.md
new file mode 100644
index 000000000..6a651df3a
--- /dev/null
+++ b/src/Homotopy/Connectedness.lagda.md
@@ -0,0 +1,117 @@
+
+
+```agda
+module Homotopy.Connectedness where
+```
+
+# Connectedness {defines="connected connectedness connectivity simply-connected"}
+
+We say that a type is **$n$-connected** if its $n$-[[truncation]] is [[contractible]].
+
+While being $n$-[[truncated]] expresses that all homotopy groups above $n$ are trivial,
+being $n$-connected means that all homotopy *below* $n$ are trivial.
+A type that is both $n$-truncated and $n$-connected is contractible.
+
+We give definitions in terms of the [[propositional truncation]] and [[set truncation]]
+for the lower levels, and then defer to the general "hubs and spokes" truncation.
+Note that our indices are offset by 2, just like [[h-levels]].
+
+```agda
+is-n-connected : ∀ {ℓ} → Type ℓ → Nat → Type _
+is-n-connected A zero = Lift _ ⊤
+is-n-connected A (suc zero) = ∥ A ∥
+is-n-connected A (suc (suc zero)) = is-contr ∥ A ∥₀
+is-n-connected A n@(suc (suc (suc _))) = is-contr (n-Tr A n)
+```
+
+Being $n$-connected is a proposition:
+
+```agda
+is-n-connected-is-prop : ∀ {ℓ} {A : Type ℓ} (n : Nat) → is-prop (is-n-connected A n)
+is-n-connected-is-prop zero _ _ = refl
+is-n-connected-is-prop (suc zero) = is-prop-∥-∥
+is-n-connected-is-prop (suc (suc zero)) = is-contr-is-prop
+is-n-connected-is-prop (suc (suc (suc n))) = is-contr-is-prop
+```
+
+For short, we say that a type is **connected** if it is $0$-connected, and
+**simply connected** if it is $1$-connected:
+
+```agda
+is-connected : ∀ {ℓ} → Type ℓ → Type _
+is-connected A = is-n-connected A 2
+
+is-simply-connected : ∀ {ℓ} → Type ℓ → Type _
+is-simply-connected A = is-n-connected A 3
+```
+
+## Pointed connected types
+
+In the case of [[pointed types]], there is an equivalent definition of being connected
+that is sometimes easier to work with: a pointed type is connected if every point is
+merely equal to the base point.
+
+```agda
+is-connected∙ : ∀ {ℓ} → Type∙ ℓ → Type _
+is-connected∙ (X , pt) = (x : X) → ∥ x ≡ pt ∥
+
+module _ {ℓ} {X@(_ , pt) : Type∙ ℓ} where
+ is-connected∙→is-connected : is-connected∙ X → is-connected ⌞ X ⌟
+ is-connected∙→is-connected c .centre = inc pt
+ is-connected∙→is-connected c .paths =
+ ∥-∥₀-elim hlevel! λ x → ∥-∥-rec! (ap inc ∘ sym) (c x)
+
+ is-connected→is-connected∙ : is-connected ⌞ X ⌟ → is-connected∙ X
+ is-connected→is-connected∙ c x =
+ ∥-∥₀-path.to (is-contr→is-prop c (inc x) (inc pt))
+```
+
+This alternative definition lets us formulate a nice elimination principle for pointed
+connected types: any family of propositions $P$ that holds on the base point holds everywhere.
+In particular, since `being a proposition is a proposition`{.Agda ident=is-prop-is-prop},
+we only need to check that $P(\point{})$ is a proposition.
+
+```agda
+connected∙-elim-prop
+ : ∀ {ℓ ℓ′} {X : Type∙ ℓ} {P : ⌞ X ⌟ → Type ℓ′}
+ → is-connected∙ X
+ → is-prop (P (X .snd))
+ → P (X .snd)
+ → ∀ x → P x
+connected∙-elim-prop {X = X} {P} conn prop pb x =
+ ∥-∥-rec (P-is-prop x) (λ e → subst P (sym e) pb) (conn x)
+ where abstract
+ P-is-prop : ∀ x → is-prop (P x)
+ P-is-prop x = ∥-∥-rec is-prop-is-prop (λ e → subst (is-prop ∘ P) (sym e) prop) (conn x)
+```
+
+Examples of pointed connected types include the [[circle]] and the [[delooping]] of a group.
+
+```agda
+S¹-is-connected : is-connected∙ (S¹ , base)
+S¹-is-connected = S¹-elim (inc refl) prop!
+
+Deloop-is-connected : ∀ {ℓ} {G : Group ℓ} → is-connected∙ (Deloop G , base)
+Deloop-is-connected = Deloop-elim-prop _ _ hlevel! (inc refl)
+```
diff --git a/src/Homotopy/Space/Circle.lagda.md b/src/Homotopy/Space/Circle.lagda.md
index 709e55468..797bdad16 100644
--- a/src/Homotopy/Space/Circle.lagda.md
+++ b/src/Homotopy/Space/Circle.lagda.md
@@ -14,7 +14,7 @@ open import Data.Int
module Homotopy.Space.Circle where
```
-# Spaces: The circle
+# Spaces: The circle {defines="circle"}
The first example of nontrivial space one typically encounters when
studying synthetic homotopy theory is the circle: it is, in a sense, the
@@ -65,6 +65,15 @@ S¹-rec b l base = b
S¹-rec b l (loop i) = l i
```
+
+
We call the map `möbius`{.Agda} a _double cover_ of the circle, since
the fibre at each point is a discrete space with two elements. It has an
action by the fundamental group of the circle, which has the effect of
diff --git a/src/Homotopy/Space/Sphere.lagda.md b/src/Homotopy/Space/Sphere.lagda.md
index 6e0c92cb2..b17d2ef92 100644
--- a/src/Homotopy/Space/Sphere.lagda.md
+++ b/src/Homotopy/Space/Sphere.lagda.md
@@ -114,7 +114,7 @@ using lemmas on transport in pathspaces.
iso-pf .rinv base = refl
iso-pf .rinv (loop i) =
ap (λ p → p i)
- (ap SuspS⁰→S¹ (merid N ∙ sym (merid S)) ≡⟨ ap-comp-path SuspS⁰→S¹ (merid N) (sym (merid S))⟩
+ (ap SuspS⁰→S¹ (merid N ∙ sym (merid S)) ≡⟨ ap-∙ SuspS⁰→S¹ (merid N) (sym (merid S))⟩
loop ∙ refl ≡⟨ ∙-id-r loop ⟩
loop ∎)
iso-pf .linv N = refl
diff --git a/src/Homotopy/Space/Suspension.lagda.md b/src/Homotopy/Space/Suspension.lagda.md
index 45f9388cb..c272bf6a9 100644
--- a/src/Homotopy/Space/Suspension.lagda.md
+++ b/src/Homotopy/Space/Suspension.lagda.md
@@ -22,7 +22,6 @@ data Susp {ℓ} (A : Type ℓ) : Type ℓ where
*TODO*: Draw a picture and explain!
-Suspension is an operation that increases the
-[connectivity](https://ncatlab.org/nlab/show/n-connected+space) of a type;
+Suspension is an operation that increases the [[connectivity]] of a type:
suspending an empty type makes it inhabited, suspending an inhabited type
makes it connected, suspending a connected type makes it 1-connected, etc.
diff --git a/src/Meta/Bind.lagda.md b/src/Meta/Bind.lagda.md
index a50b7ed55..4e56478f0 100644
--- a/src/Meta/Bind.lagda.md
+++ b/src/Meta/Bind.lagda.md
@@ -22,8 +22,12 @@ record Bind (M : Effect) : Typeω where
_>>_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → M.₀ A → M.₀ B → M.₀ B
_>>_ f g = f >>= λ _ → g
+ infixl 1 _>>=_
+
_=<<_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → (A → M.₀ B) → M.₀ A → M.₀ B
_=<<_ f x = x >>= f
+ infixr 1 _=<<_
+
open Bind ⦃ ... ⦄ public
```
diff --git a/src/Order/Frame/Reasoning.lagda.md b/src/Order/Frame/Reasoning.lagda.md
index 1bb1f6cc0..7a38e7dff 100644
--- a/src/Order/Frame/Reasoning.lagda.md
+++ b/src/Order/Frame/Reasoning.lagda.md
@@ -2,8 +2,8 @@
```agda
open import Cat.Prelude
-open import Order.Diagram.Lub
open import Order.Diagram.Glb
+open import Order.Diagram.Lub
open import Order.Semilattice
open import Order.Frame
open import Order.Base
diff --git a/src/bibliography.bibtex b/src/bibliography.bibtex
index 52e9b3b63..7ffeb15b8 100644
--- a/src/bibliography.bibtex
+++ b/src/bibliography.bibtex
@@ -130,3 +130,12 @@
archivePrefix={arXiv},
primaryClass={cs.LO}
}
+
+@misc{Symmetry,
+ title = {Symmetry},
+ author = {Marc Bezem and Ulrik Buchholtz and Pierre Cagne
+ and Bjørn Ian Dundas and Daniel R. Grayson},
+ date = {2023-08-23},
+ howpublished = {\url{https://github.com/UniMath/SymmetryBook}},
+ note = {Commit: \texttt{33011eb}}
+}
diff --git a/src/index.lagda.md b/src/index.lagda.md
index 66b91c27f..405252b5b 100644
--- a/src/index.lagda.md
+++ b/src/index.lagda.md
@@ -176,6 +176,7 @@ are developed under the `1Lab` namespace. Start here:
-- All of these module names are links you can click!
open import 1Lab.Type -- Universes
+open import 1Lab.Type.Pointed -- Pointed types
open import 1Lab.Path -- Path types
open import 1Lab.Path.Groupoid -- Groupoid structure of types
@@ -963,6 +964,7 @@ open import Algebra.Group.Cat.Base -- The category of groups
open import Algebra.Group.Cat.Monadic -- ... is monadic over Sets
open import Algebra.Group.Cat.FinitelyComplete -- Finite limits in Groups
open import Algebra.Group.Subgroup -- Subgroups, images and kernels
+open import Algebra.Group.Concrete -- Concrete groups (pointed connected groupoids)
open import Algebra.Group.Homotopy -- Homotopy groups
open import Algebra.Group.Homotopy.BAut
@@ -988,6 +990,23 @@ open import Algebra.Ring.Module.Free -- Free R-modules as a HIT
open import Algebra.Ring.Module.Category -- The bifibration of Mod over Ring
```
+# Homotopy theory
+
+Synthetic homotopy theory is the name given to studying
+$\infty$-groupoids in their own terms, i.e., the application of homotopy type
+theory to computing homotopy invariants of spaces.
+
+```agda
+open import Homotopy.Base -- Basic definitions
+open import Homotopy.Connectedness -- Connected types
+
+open import Homotopy.Space.Suspension -- Suspensions
+open import Homotopy.Space.Circle -- The circle
+open import Homotopy.Space.Sphere -- The n-spheres
+open import Homotopy.Space.Sinfty -- The ∞-sphere
+open import Homotopy.Space.Torus -- The torus
+```
+
diff --git a/src/preamble.tex b/src/preamble.tex
index 1f020ed0a..32c477ec8 100644
--- a/src/preamble.tex
+++ b/src/preamble.tex
@@ -73,6 +73,8 @@
\DeclareMathOperator*{\im}{im}
\DeclareMathOperator*{\Sub}{Sub}
\DeclareMathOperator*{\baut}{\mathbf{B}}
+\newcommand{\B}[1]{\mathbf{B} #1}
+\newcommand{\point}[1]{\bullet_{#1}}
\DeclareMathOperator{\Lan}{Lan}
\DeclareMathOperator{\Ran}{Ran}
diff --git a/support/nix/nixpkgs.nix b/support/nix/nixpkgs.nix
index 105027eff..26ccda5ed 100644
--- a/support/nix/nixpkgs.nix
+++ b/support/nix/nixpkgs.nix
@@ -1,7 +1,7 @@
-import (builtins.fetchTarball {
+args: import (builtins.fetchTarball {
name = "1lab-nixpkgs";
url = "https://github.com/nixos/nixpkgs/archive/cc4bb87f5457ba06af9ae57ee4328a49ce674b1b.tar.gz";
sha256 = "sha256:072q50x5p06qjf0cvz68gcrbkpv94bdl55h71j0rz6bgfhaqmiwy";
-}) {
+}) ({
overlays = [ (import ./haskell-packages.nix) ];
-}
+} // args)
diff --git a/support/nix/node/node-dependencies.nix b/support/nix/node/node-dependencies.nix
index aa5b189a6..e50ec1d34 100644
--- a/support/nix/node/node-dependencies.nix
+++ b/support/nix/node/node-dependencies.nix
@@ -906,8 +906,8 @@ let
};
};
args = {
- name = "cubical-1lab";
- packageName = "cubical-1lab";
+ name = "1lab";
+ packageName = "1lab";
version = "1.0.0";
src = ../../..;
dependencies = [
@@ -1018,7 +1018,7 @@ let
buildInputs = globalBuildInputs;
meta = {
description = " A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ";
- homepage = "https://github.com/plt-amy/cubical-1lab#readme";
+ homepage = "https://github.com/plt-amy/1lab#readme";
license = "AGPL-3.0";
};
production = false;
diff --git a/support/shake/app/Definitions.hs b/support/shake/app/Definitions.hs
index 9e4382339..bb79f43d2 100644
--- a/support/shake/app/Definitions.hs
+++ b/support/shake/app/Definitions.hs
@@ -122,7 +122,7 @@ addDefinition key@(getMangled -> keyt) def (Glossary ge) = Glossary (go False ke
Just def' | def' /= def -> error $ unlines
[ "Conflict when building link map:"
, "The files " ++ show (definitionModule def) ++ " and " ++ show (definitionModule def')
- ++ " both define the anchor " ++ show (definitionAnchor def)
+ ++ " both define the term " ++ show key
]
_ -> Map.insert key def{definitionCopy = c} ge
diff --git a/support/sort-imports.hs b/support/sort-imports.hs
index f9c119832..07295bc3f 100755
--- a/support/sort-imports.hs
+++ b/support/sort-imports.hs
@@ -2,6 +2,7 @@
{- stack --resolver lts-18.14 script
--package text
--package deepseq
+ --package filemanip
-}
{-# LANGUAGE OverloadedStrings #-}
module Main where
@@ -13,16 +14,22 @@ import Data.List (isSuffixOf, sortOn, groupBy, partition)
import qualified Data.Text.IO as Text
import qualified Data.Text as Text
import Data.Function (on)
-import Data.Foldable
+import Data.Foldable hiding (find)
import Data.Ord
import Debug.Trace
import System.Environment
+import System.FilePath.Find
import System.IO
main :: IO ()
-main = traverse_ sortImports =<< getArgs
+main = do
+ args <- getArgs
+ traverse_ sortImports =<< if null args then getAgdaFiles else pure args
+
+getAgdaFiles :: IO [FilePath]
+getAgdaFiles = find always (fileName ~~? "*.(agda|lagda.md)") "src"
sortImports :: FilePath -> IO ()
sortImports path
@@ -81,15 +88,20 @@ sortImpl lines = sorted ++ emptyLineBefore' mod where
(imports, io'') = partition ("import" `Text.isPrefixOf`) io'
(opens, prefix) = partition ("open" `Text.isPrefixOf`) io''
+ uniqueSortOn f = go . sortOn f where
+ go (x:x':xs) | x == x' = go (x':xs)
+ go (x:xs) = x : go xs
+ go [] = []
+
sorted = filter (not . Text.null) prefix
++ sortItems "open import" open_imports
++ emptyLineBefore (sortItems "import" imports)
- ++ emptyLineBefore (sortOn (Down . Text.length) opens)
+ ++ emptyLineBefore (uniqueSortOn (Down . Text.length) opens)
findItem prefix line = head (Text.words (Text.drop (Text.length prefix) line))
sortItems prefix =
drop 1
- . concatMap (("":) . sortOn (Down . Text.length . findItem prefix))
+ . concatMap (("":) . uniqueSortOn (Down . Text.length . findItem prefix))
. groupBy ((==) `on` fst . Text.breakOn "." . findItem prefix)
. sortOn (findItem prefix)
+