bump 1lab; web improvements

ncfavier · Dec 21, 2023 · 29bab18 · 29bab18
1 parent be8d37d
commit 29bab18
Show file tree

Hide file tree

Showing 5 changed files with 79 additions and 31 deletions.
diff --git a/.github/workflows/web.yaml b/.github/workflows/web.yaml
@@ -9,8 +9,8 @@ jobs:
         with:
           extra_nix_config: |
             access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-            extra-substituters = https://nix.monade.li
-            extra-trusted-public-keys = nix.monade.li:2Zgy59ai/edDBizXByHMqiGgaHlE04G6Nzuhx1RPFgo=
+            extra-substituters = https://nix.monade.li https://ncfavier.cachix.org
+            extra-trusted-public-keys = nix.monade.li:2Zgy59ai/edDBizXByHMqiGgaHlE04G6Nzuhx1RPFgo= ncfavier.cachix.org-1:RpBMt+EIZOwVwU1CW71cWZAVJ9DCNbCMsX8VOGSf3ME=
       - name: Build
         run: |
           web=$(nix -L build --print-out-paths)

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -1,28 +1,53 @@
 {
   inputs = {
     nixpkgs.url = "nixpkgs/haskell-updates";
+    _1lab = {
+      url = "github:plt-amy/1lab";
+      flake = false;
+    };
   };
 
-  outputs = { self, nixpkgs, ... }: let
+  outputs = inputs@{ self, nixpkgs, ... }: let
     system = "x86_64-linux";
     pkgs = nixpkgs.legacyPackages.${system};
+    inherit (nixpkgs) lib;
   in {
     packages.${system}.default = pkgs.stdenv.mkDerivation {
       name = "cubical-experiments";
       src = self;
       nativeBuildInputs = with pkgs; [
-        (agda.withPackages (p: with p; [ cubical _1lab ]))
+        (agda.withPackages (p: with p; [
+          cubical
+          (_1lab.overrideAttrs (old: lib.optionalAttrs (inputs ? _1lab) {
+            version = "unstable";
+            src = inputs._1lab;
+            GHCRTS = "-M5G";
+          }))
+        ]))
       ];
       LC_ALL = "C.UTF-8";
-      extraHead = ''
+      postHead = ''
         <meta name="author" content="Naïm Favier">
         <meta name="viewport" content="width=device-width, initial-scale=1, user-scalable=yes">
         <link rel="icon" type="image/png" href="//monade.li/favicon.png">
       '';
+      preBodyInternal = ''
+        <h3>
+          <a href="/">index</a> ∙
+          <a href="https://github.com/ncfavier/cubical-experiments/blob/main/@MODULE@">source</a>
+        </h3>
+      '';
+      preBodyExternal = ''
+        <h3><a href="/">index</a></h3>
+        <p style="border-left: 5px solid #facc15; padding: 1rem;">
+          ⚠️ This module is not part of this project and is only included for reference.<br>
+          It is either part of the <a href="https://1lab.dev">1lab</a>, the <a href="https://github.com/agda/cubical">cubical</a> library, or a built-in Agda module.
+        </p>
+      '';
       buildPhase = ''
-        shopt -s extglob
+        shopt -s extglob nullglob
         for f in src/*.agda src/*.lagda*; do
-          mod=''${f%%.@(agda|lagda*)} mod=''${mod##*/}
+          base=''${f##*/} mod=''${base%%.@(agda|lagda*)}
           if grep -qE 'import *(1Lab|Cat)\.' "$f"; then
             echo "import $mod" >> Everything-1Lab.agda
           else
@@ -34,8 +59,19 @@
         done
         agda -i . --html --html-dir="$out" --html-highlight=all --css=style.css --highlight-occurrences Everything.agda
         agda -i . --html --html-dir="$out" --html-highlight=all --css=style.css --highlight-occurrences Everything-1Lab.agda
-        substituteInPlace "$out"/highlight-hover.js --replace getSelectorAll querySelectorAll
-        substituteInPlace "$out"/*.html --replace '</head>' "$extraHead</head>"
+        for f in "$out"/*.html; do
+          base=''${f##*/} mod=''${base%%.html}
+          src=(src/"$mod".@(agda|lagda*))
+          if (( ''${#src} )); then
+            substituteInPlace "$f" \
+              --replace '</head>' "$postHead</head>" \
+              --replace '<body>' "<body>''${preBodyInternal/@MODULE@/"''${src[0]}"}"
+          else
+            substituteInPlace "$f" \
+              --replace '</head>' "$postHead</head>" \
+              --replace '<body>' "<body>$preBodyExternal"
+          fi
+        done
         cp ${self}/{index.html,style.css} "$out"/
         substituteInPlace "$out"/index.html --subst-var-by modules "$(< mods)"
       '';

diff --git a/src/FirstGroupCohomology.agda b/src/FirstGroupCohomology.agda
@@ -1,24 +1,18 @@
-open import 1Lab.Prelude
 open import 1Lab.Path.Reasoning
-open import 1Lab.Reflection.Induction
-open import Algebra.Group
-open import Algebra.Group.Ab
-open import Algebra.Group.Homotopy
-open import Algebra.Group.Concrete
+open import 1Lab.Prelude
+
 open import Algebra.Group.Cat.Base
+open import Algebra.Group.Concrete
+open import Algebra.Group.Ab
+
 open import Cat.Prelude
-open import Homotopy.Connectedness
+
+open import Homotopy.Space.Delooping
 
 module FirstGroupCohomology where
 
 open Precategory
 
-unquoteDecl Deloop-elim-set = make-elim-n 2 Deloop-elim-set (quote Deloop)
-
-instance
-  H-Level-Deloop' : ∀ {ℓ} {G : Group ℓ} {n} → H-Level (Deloop G) (3 + n)
-  H-Level-Deloop' {G = G} = H-Level-Deloop G
-
 Deloop∙ : ∀ {ℓ} (G : Group ℓ) → Type∙ ℓ
 Deloop∙ G = Deloop G , base
 
@@ -28,16 +22,13 @@ DeloopC G = concrete-group (Deloop∙ G) Deloop-is-connected (hlevel 3)
 π₁BG≡G : ∀ {ℓ} (G : Group ℓ) → π₁B (DeloopC G) ≡ G
 π₁BG≡G G = π₁≡π₀₊₁ ∙ sym (G≡π₁B G)
 
-Group-is-abelian : ∀ {ℓ} → Group ℓ → Type _
-Group-is-abelian G = Group-on-is-abelian (G .snd)
-
 -- Any two loops commute in the delooping of an abelian group.
-ab→square : ∀ {ℓ} {H : Group ℓ} (H-ab : Group-is-abelian H)
+ab→square : ∀ {ℓ} {H : Group ℓ} (H-ab : is-commutative-group H)
           → {x : Deloop H} (p q : x ≡ x) → Square p q q p
 ab→square {H = H} H-ab {x} = Deloop-elim-prop H (λ x → (p q : x ≡ x) → Square p q q p) hlevel!
-  (λ p q → commutes→square (subst Group-is-abelian (sym (π₁BG≡G H)) H-ab p q)) x
+  (λ p q → commutes→square (subst is-commutative-group (sym (π₁BG≡G H)) H-ab p q)) x
 
-module _ {ℓ} (G : Group ℓ) (H : Group ℓ) (H-ab : Group-is-abelian H) where
+module _ {ℓ} (G : Group ℓ) (H : Group ℓ) (H-ab : is-commutative-group H) where
   -- The first cohomology of G with coefficients in H.
   -- We will show that it is equivalent to the set of group homomorphisms from G
   -- to H, assuming that H is abelian.
@@ -49,7 +40,7 @@ module _ {ℓ} (G : Group ℓ) (H : Group ℓ) (H-ab : Group-is-abelian H) where
   work : ∀ f → f base ≡ base → is-contr (fibre unpoint (inc f))
   work f ptf .centre = (f , ptf) , refl
   work f ptf .paths ((g , ptg) , g≡f) = Σ-prop-path! (Σ-pathp
-    (funext (Deloop-elim-set hlevel! (ptf ∙ sym ptg) λ z → ∥-∥-rec!
+    (funext (Deloop-elim-set G _ hlevel! (ptf ∙ sym ptg) λ z → ∥-∥-rec!
       (λ g≡f → J
         (λ g _ → ∀ ptg → Square (ap f (path z)) (ptf ∙ sym ptg) (ptf ∙ sym ptg) (ap g (path z)))
         (λ _ → ab→square H-ab _ _)

diff --git a/style.css b/style.css
@@ -20,9 +20,13 @@ body {
   color: var(--foreground);
 }
 
-a {
+:any-link {
   text-decoration: none;
-  color: inherit;
+  color: var(--literal);
+}
+
+h1 a, h2 a, h3 a {
+  color: inherit !important;
 }
 
 /* Aspects. */