Concrete groups (#254)

Defines connectedness, concrete groups (pointed connected groupoids),
and an equivalence between the categories of concrete and abstract
(set-based) groups.

The section on delooping homomorphisms is largely inspired by
[[Symmetry](https://unimath.github.io/SymmetryBook/book.pdf) §4.10],
which was apparently written by Thierry Coquand(?).

I'm not sure how to best organise concepts into modules in a way that
avoids cyclic dependencies. If you have any ideas at all, please advise.
Currently things are kind of strewn about between `1Lab.Type.Pointed`,
`1Lab.Connectedness`, `Algebra.Group.Homotopy`, `Homotopy.Base`, and now
`Algebra.Group.Concrete`, with all sorts of 🐔🔄🥚 problems lurking around
the corner.

.github/pull_request_template.md

@@ -6,7 +6,7 @@ Please include a quick description of the changes here.
 
 Before submitting a merge request, please check the items below:
 
-- [ ] The imports are sorted (use `find -type f -name \*.agda -or -name \*.lagda.md | xargs support/sort-imports.hs`)
+- [ ] The imports are sorted with `support/sort-imports.hs`
 
 - [ ] All code blocks have "agda" as their language. This is so that
 tools like Tokei can report accurate line counts for proofs vs. text.

1lab.agda-lib

@@ -1,4 +1,4 @@
-name: cubical-1lab
+name: 1lab
 include:
   src
   wip

CONTRIBUTING.md

@@ -6,15 +6,16 @@ Thanks for taking the time to contribute!
 This file holds the conventions we use around the codebase, but they're
 guidelines, and not strict rules: If you're unsure of something, hop on
 [the Discord](https://discord.gg/Zp2e8hYsuX) and ask there, or open [a
-discussion thread](https://github.com/plt-amy/cubical-1lab/discussions)
+discussion thread](https://github.com/plt-amy/1lab/discussions)
 if that's more your style.
 
 ### General guidelines
 
 Use British spelling everywhere that it differs from American: Homotopy
 fib**re**, fib**red** category, colo**u**red operad, etc --- both in
 prose and in Agda. Keep prose paragraphs limited to 72 characters of
-length. Prefer link anchors (Pandoc "reference links") to inline links.
+length. Prefer wikilinks or link anchors (Pandoc "reference links") to
+inline links.
 
 ### Agda code style
 

README.md

@@ -1,5 +1,5 @@
 [![Discord](https://img.shields.io/discord/914172963157323776?label=Discord&logo=discord)](https://discord.gg/Zp2e8hYsuX)
-[![Build 1Lab](https://github.com/plt-amy/cubical-1lab/actions/workflows/build.yml/badge.svg)](https://github.com/plt-amy/cubical-1lab/actions/workflows/build.yml)
+[![Build 1Lab](https://github.com/plt-amy/1lab/actions/workflows/build.yml/badge.svg)](https://github.com/plt-amy/1lab/actions/workflows/build.yml)
 
 # [1Lab](https://1lab.dev)
 

default.nix

@@ -2,9 +2,10 @@
   inNixShell ? false
   # Do we want the full Agda package for interactive use? Set to false in CI
 , interactive ? true
+, system ? builtins.currentSystem
 }:
 let
-  pkgs = import ./support/nix/nixpkgs.nix;
+  pkgs = import ./support/nix/nixpkgs.nix { inherit system; };
   inherit (pkgs) lib;
 
   our-ghc = pkgs.labHaskellPackages.ghcWithPackages (ps: with ps; [

package.json

@@ -1,5 +1,5 @@
 {
-  "name": "cubical-1lab",
+  "name": "1lab",
   "version": "1.0.0",
   "description": " A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory ",
   "main": "index.js",
@@ -8,14 +8,14 @@
   },
   "repository": {
     "type": "git",
-    "url": "git+https://github.com/plt-amy/cubical-1lab.git"
+    "url": "git+https://github.com/plt-amy/1lab.git"
   },
   "author": "Amélia Liao et. al.",
   "license": "AGPL-3.0",
   "bugs": {
-    "url": "https://github.com/plt-amy/cubical-1lab/issues"
+    "url": "https://github.com/plt-amy/1lab/issues"
   },
-  "homepage": "https://github.com/plt-amy/cubical-1lab#readme",
+  "homepage": "https://github.com/plt-amy/1lab#readme",
   "devDependencies": {
     "@types/d3": "^7.1.0",
     "d3": "^7.4.4",

src/1Lab/Equiv/Biinv.lagda.md

@@ -176,11 +176,11 @@ suffices to show that `is-biinv`{.Agda} is contractible when it is
 inhabited:
 
 [a proposition]: agda://1Lab.HLevel#is-prop
-[contractible if inhabited]: agda://1Lab.HLevel#contractible-if-inhabited
+[contractible if inhabited]: agda://1Lab.HLevel#is-contr-if-inhabited→is-prop
 
 ```agda
 is-biinv-is-prop : {f : A → B} → is-prop (is-biinv f)
-is-biinv-is-prop {f = f} = contractible-if-inhabited contract where
+is-biinv-is-prop {f = f} = is-contr-if-inhabited→is-prop contract where
   contract : is-biinv f → is-contr (is-biinv f)
   contract ibiinv =
     ×-is-hlevel 0 (is-iso→is-contr-linv iiso)

src/1Lab/Equiv/HalfAdjoint.lagda.md

@@ -176,7 +176,7 @@ another $(x, p)$ using a very boring calculation:
 
     path : ap f (ap g (sym p) ∙ η x) ∙ p ≡ ε y
     path =
-      ap f (ap g (sym p) ∙ η x) ∙ p                   ≡⟨ ap₂ _∙_ (ap-comp-path f (ap g (sym p)) (η x)) refl ∙ sym (∙-assoc _ _ _) ⟩
+      ap f (ap g (sym p) ∙ η x) ∙ p                   ≡⟨ ap₂ _∙_ (ap-∙ f (ap g (sym p)) (η x)) refl ∙ sym (∙-assoc _ _ _) ⟩
       ap (λ x → f (g x)) (sym p) ∙ ⌜ ap f (η x) ⌝ ∙ p ≡⟨ ap! (zig _) ⟩ -- by the triangle identity
       ap (f ∘ g) (sym p) ∙ ⌜ ε (f x) ∙ p ⌝            ≡⟨ ap! (homotopy-natural ε p)  ⟩ -- by naturality of ε
 ```
@@ -189,7 +189,7 @@ $\varepsilon$ lets us "push it past $p$" to get something we can cancel:
 
 ```agda
       ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ∙ ε y     ≡⟨ ∙-assoc _ _ _ ⟩
-      ⌜ ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ⌝ ∙ ε y ≡˘⟨ ap¡ (ap-comp-path (f ∘ g) (sym p) p) ⟩
+      ⌜ ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ⌝ ∙ ε y ≡˘⟨ ap¡ (ap-∙ (f ∘ g) (sym p) p) ⟩
       ap (f ∘ g) ⌜ sym p ∙ p ⌝ ∙ ε y              ≡⟨ ap! (∙-inv-r _) ⟩
       ap (f ∘ g) refl ∙ ε y                       ≡⟨⟩
       refl ∙ ε y                                  ≡⟨ ∙-id-l (ε y) ⟩

src/1Lab/HIT/Truncation.lagda.md

@@ -48,7 +48,7 @@ is-prop-∥-∥ = squash
 ```agda
 instance
   H-Level-truncation : ∀ {n} {ℓ} {A : Type ℓ} → H-Level ∥ A ∥ (suc n)
-  H-Level-truncation = hlevel-instance (is-prop→is-hlevel-suc squash)
+  H-Level-truncation = prop-instance squash
 ```
 -->
 

src/1Lab/HLevel.lagda.md

@@ -9,7 +9,7 @@ open import 1Lab.Type
 module 1Lab.HLevel where
 ```
 
-# h-Levels
+# h-Levels {defines="h-level n-type truncated"}
 
 The "homotopy level" (h-level for short) of a type is a measure of how
 [truncated] it is, where the numbering is offset by 2. Specifically, a
@@ -36,8 +36,10 @@ _homotopy $(n-2)$-types_. For instance: "The sets are the homotopy
 0-types". The use of the $-2$ offset is so the naming here matches that
 of the HoTT book.
 
+:::{.definition #contractible}
 The h-levels are defined by induction, where the base case are the
 _contractible types_.
+:::
 
 [truncated]: https://ncatlab.org/nlab/show/truncated+object
 
@@ -77,7 +79,7 @@ type.
   interval-contractible .paths (seg i) j = seg (i ∧ j)
 ```
 
-:::{.definition #proposition}
+:::{.definition #proposition alias="property"}
 A type is (n+1)-truncated if its path types are all n-truncated.
 However, if we directly take this as the definition, the types we end up
 with are very inconvenient! That's why we introduce this immediate step:
@@ -114,7 +116,9 @@ is-set : ∀ {ℓ} → Type ℓ → Type ℓ
 is-set A = is-hlevel A 2
 ```
 
+:::{.definition #groupoid}
 Similarly, the types of h-level 3 are called **groupoids**.
+:::
 
 ```agda
 is-groupoid : ∀ {ℓ} → Type ℓ → Type ℓ
@@ -182,8 +186,12 @@ which is that the propositions are precisely the types which are
 contractible when they are inhabited:
 
 ```agda
-contractible-if-inhabited : ∀ {ℓ} {A : Type ℓ} → (A → is-contr A) → is-prop A
-contractible-if-inhabited cont x y = is-contr→is-prop (cont x) x y
+is-contr-if-inhabited→is-prop : ∀ {ℓ} {A : Type ℓ} → (A → is-contr A) → is-prop A
+is-contr-if-inhabited→is-prop cont x y = is-contr→is-prop (cont x) x y
+
+is-prop→is-contr-if-inhabited : ∀ {ℓ} {A : Type ℓ} → is-prop A → A → is-contr A
+is-prop→is-contr-if-inhabited prop x .centre = x
+is-prop→is-contr-if-inhabited prop x .paths y = prop x y
 ```
 
 The proof that any contractible type is a proposition is not too
@@ -372,6 +380,13 @@ is-hlevel-is-prop (suc (suc n)) x y i a b =
   is-hlevel-is-prop (suc n) (x a b) (y a b) i
 ```
 
+<!--
+```agda
+is-hlevel-is-hlevel-suc : ∀ {ℓ} {A : Type ℓ} (k n : Nat) → is-hlevel (is-hlevel A n) (suc k)
+is-hlevel-is-hlevel-suc k n = is-prop→is-hlevel-suc (is-hlevel-is-prop n)
+```
+-->
+
 # Dependent h-Levels
 
 In cubical type theory, it's natural to consider a notion of _dependent_

src/1Lab/HLevel/Retracts.lagda.md

@@ -352,9 +352,10 @@ instance
   H-Level-sigma {n = n} .H-Level.has-hlevel =
     Σ-is-hlevel n (hlevel n) λ _ → hlevel n
 
-  H-Level-path′
-    : ∀ {n} ⦃ s : H-Level S (suc n) ⦄ {x y} → H-Level (Path S x y) n
-  H-Level-path′ {n = n} .H-Level.has-hlevel = Path-is-hlevel' n (hlevel (suc n)) _ _
+  H-Level-PathP
+    : ∀ {n} {S : I → Type ℓ} ⦃ s : H-Level (S i1) (suc n) ⦄ {x y}
+    → H-Level (PathP S x y) n
+  H-Level-PathP {n = n} .H-Level.has-hlevel = PathP-is-hlevel' n (hlevel (suc n)) _ _
 
   H-Level-Lift
     : ∀ {n} ⦃ s : H-Level T n ⦄ → H-Level (Lift ℓ T) n

src/1Lab/Path.lagda.md

@@ -268,6 +268,21 @@ Square : ∀ {ℓ} {A : Type ℓ} {a00 a01 a10 a11 : A}
 Square p q s r = PathP (λ i → p i ≡ r i) q s
 ```
 
+<!--
+```
+SquareP : ∀ {ℓ}
+  (A : I → I → Type ℓ)
+  {a₀₀ : A i0 i0} {a₀₁ : A i0 i1}
+  {a₁₀ : A i1 i0} {a₁₁ : A i1 i1}
+  (p : PathP (λ i → A i i0) a₀₀ a₁₀)
+  (q : PathP (λ j → A i0 j) a₀₀ a₀₁)
+  (s : PathP (λ j → A i1 j) a₁₀ a₁₁)
+  (r : PathP (λ i → A i i1) a₀₁ a₁₁)
+  → Type ℓ
+SquareP A p q s r = PathP (λ i → PathP (λ j → A i j) (p i) (r i)) q s
+```
+-->
+
 The arguments to `Square`{.Agda} are as in the following diagram, listed
 in the order “PQSR”. This order is a bit unusual (it's one off from
 being alphabetical, for instance) but it does have a significant
@@ -1028,6 +1043,8 @@ be reflexivity. For definiteness, we chose the left face:
 _∙_ : ∀ {ℓ} {A : Type ℓ} {x y z : A}
     → x ≡ y → y ≡ z → x ≡ z
 p ∙ q = refl ·· p ·· q
+
+infixr 30 _∙_
 ```
 
 The ordinary, “single composite” of $p$ and $q$ is the dashed face in
@@ -1061,17 +1078,29 @@ setting the _right_ face to `refl`{.Agda}.
 ```
 
 We can use the filler and heterogeneous composition to define composition of `PathP`{.Agda}s
-in a given type family:
+and `Square`{.Agda}s:
 
 ```agda
 _∙P_ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} {x y z : A} {x′ : B x} {y′ : B y} {z′ : B z} {p : x ≡ y} {q : y ≡ z}
-     → PathP (λ i → B (p i)) x′ y′ → PathP (λ i → B (q i)) y′ z′
+     → PathP (λ i → B (p i)) x′ y′
+     → PathP (λ i → B (q i)) y′ z′
      → PathP (λ i → B ((p ∙ q) i)) x′ z′
 _∙P_ {B = B} {x′ = x′} {p = p} {q = q} p′ q′ i =
   comp (λ j → B (∙-filler p q j i)) (∂ i) λ where
     j (i = i0) → x′
     j (i = i1) → q′ j
     j (j = i0) → p′ i
+
+_∙₂_ : ∀ {ℓ} {A : Type ℓ} {a00 a01 a02 a10 a11 a12 : A}
+       {p : a00 ≡ a01} {p′ : a01 ≡ a02}
+       {q : a00 ≡ a10} {s : a01 ≡ a11} {t : a02 ≡ a12}
+       {r : a10 ≡ a11} {r′ : a11 ≡ a12}
+     → Square p q s r
+     → Square p′ s t r′
+     → Square (p ∙ p′) q t (r ∙ r′)
+(α ∙₂ β) i j = ((λ i → α i j) ∙ (λ i → β i j)) i
+
+infixr 30 _∙P_ _∙₂_
 ```
 
 ## Uniqueness
@@ -1196,6 +1225,12 @@ its filler), it is contractible:
   → r ≡ p ∙ q
 ∙-unique {p = p} {q} r square i =
   ··-unique refl p q (_ , square) (_ , (∙-filler p q)) i .fst
+
+··-unique' : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
+           → {p : w ≡ x} {q : x ≡ y} {r : y ≡ z} {s : w ≡ z}
+           → (β : Square (sym p) q s r)
+           → s ≡ p ·· q ·· r
+··-unique' β i = ··-contract _ _ _ (_ , β) (~ i) .fst
 ```
 -->
 
@@ -1246,6 +1281,18 @@ apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
     → (p : PathP A x y)
     → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
 apd f p i = f i (p i)
+
+ap-square
+  : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′}
+      {a00 a01 a10 a11 : A}
+      {p : a00 ≡ a01}
+      {q : a00 ≡ a10}
+      {s : a01 ≡ a11}
+      {r : a10 ≡ a11}
+  → (f : (a : A) → B a)
+  → (α : Square p q s r)
+  → SquareP (λ i j → B (α i j)) (ap f p) (ap f q) (ap f s) (ap f r)
+ap-square f α i j = f (α i j)
 ```
 -->
 
@@ -1261,9 +1308,9 @@ module _ where
     f : A → B
     g : B → C
 
-  ap-comp : {x y : A} {p : x ≡ y}
-          → ap (λ x → g (f x)) p ≡ ap g (ap f p)
-  ap-comp = refl
+  ap-∘ : {x y : A} {p : x ≡ y}
+       → ap (λ x → g (f x)) p ≡ ap g (ap f p)
+  ap-∘ = refl
 
   ap-id : {x y : A} {p : x ≡ y}
         → ap (λ x → x) p ≡ p
@@ -1284,12 +1331,13 @@ for the open box with sides `refl`, `ap f p` and `ap f q`, so they must be equal
 [uniqueness]: 1Lab.Path.html#uniqueness
 
 ```agda
-  ap-comp-path : (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
-               → ap f (p ∙ q) ≡ ap f p ∙ ap f q
-  ap-comp-path f p q i = ··-unique refl (ap f p) (ap f q)
-    (ap f (p ∙ q)    , λ k j → f (∙-filler p q k j))
-    (ap f p ∙ ap f q , ∙-filler _ _)
-    i .fst
+  ap-·· : (f : A → B) {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
+        → ap f (p ·· q ·· r) ≡ ap f p ·· ap f q ·· ap f r
+  ap-·· f p q r = ··-unique' (ap-square f (··-filler p q r))
+
+  ap-∙ : (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
+       → ap f (p ∙ q) ≡ ap f p ∙ ap f q
+  ap-∙ f p q = ap-·· f refl p q
 ```
 
 # Syntax Sugar
@@ -1323,7 +1371,6 @@ x ≡⟨⟩ x≡y = x≡y
 _∎ : ∀ {ℓ} {A : Type ℓ} (x : A) → x ≡ x
 x ∎ = refl
 
-infixr 30 _∙_ _∙P_
 infixr 2 _≡⟨⟩_ _≡˘⟨_⟩_
 infix  3 _∎
 
@@ -1359,21 +1406,6 @@ your convenience, it's here too:
 
 Try pressing it!
 
-<!--
-```
-SquareP : ∀ {ℓ}
-  (A : I → I → Type ℓ)
-  {a₀₀ : A i0 i0} {a₀₁ : A i0 i1}
-  {a₁₀ : A i1 i0} {a₁₁ : A i1 i1}
-  (p : PathP (λ i → A i i0) a₀₀ a₁₀)
-  (q : PathP (λ j → A i0 j) a₀₀ a₀₁)
-  (s : PathP (λ j → A i1 j) a₁₀ a₁₁)
-  (r : PathP (λ i → A i i1) a₀₁ a₁₁)
-  → Type ℓ
-SquareP A p q s r = PathP (λ i → PathP (λ j → A i j) (p i) (r i)) q s
-```
--->
-
 # Dependent Paths
 
 Surprisingly often, we want to compare inhabitants $a : A$ and $b : B$

src/1Lab/Path/Groupoid.lagda.md

@@ -19,7 +19,7 @@ module 1Lab.Path.Groupoid where
 _ = Path
 _ = hfill
 _ = ap-refl
-_ = ap-comp-path
+_ = ap-∙
 _ = ap-sym
 ```
 -->
@@ -208,7 +208,7 @@ equal to `sym (sym p)`. In that case, we show that `sym p ∙ sym (sym p)
 
 In addition to the groupoid identities for paths in a type, it has been
 established that functions behave like functors: These are the lemmas
-`ap-refl`{.Agda}, `ap-comp-path`{.Agda} and `ap-sym`{.Agda} in the
+`ap-refl`{.Agda}, `ap-∙`{.Agda} and `ap-sym`{.Agda} in the
 [1Lab.Path] module.
 
 [1Lab.Path]: 1Lab.Path.html#functorial-action