hats

cubical-experiments.agda-lib

@@ -11,4 +11,5 @@ flags:
     --allow-unsolved-metas
     --rewriting
     --guardedness
-    -WnoInteractionMetaBoundaries
+    -W noInteractionMetaBoundaries
+    -W noUnsupportedIndexedMatch

flake.nix

@@ -1,8 +1,8 @@
 {
   inputs = {
-    nixpkgs.url = "nixpkgs/haskell-updates";
+    nixpkgs.url = "nixpkgs/nixos-unstable";
     onelab = {
-      url = "github:plt-amy/1lab/even-odd";
+      url = "github:plt-amy/1lab/ncf/misc";
       flake = false;
     };
   };
@@ -22,6 +22,18 @@
             version = "unstable";
             src = inputs.onelab;
             GHCRTS = "-M5G";
+            postBuild = ''
+              shopt -s nullglob globstar extglob
+              interfaceFile() {
+                local f=$1
+                echo "''${f%.@(agda|lagda.md)}.agdai"
+              }
+              for f in src/**/*.agda src/**/*.lagda.md; do
+                if [[ ! -e "$(interfaceFile "$f")" ]]; then
+                  agda "$f"
+                fi
+              done
+            '';
           }))
         ]))
       ];

src/FirstGroupCohomology.agda

@@ -2,7 +2,7 @@ open import 1Lab.Path.Reasoning
 open import 1Lab.Prelude
 
 open import Algebra.Group.Cat.Base
-open import Algebra.Group.Concrete hiding (work)
+open import Algebra.Group.Concrete
 open import Algebra.Group.Ab
 
 open import Cat.Prelude

src/Hats.agda

@@ -0,0 +1,131 @@
+open import 1Lab.Path.Reasoning
+open import 1Lab.Prelude
+
+open import Algebra.Monoid.Category
+open import Algebra.Group
+
+open import Data.List hiding (lookup)
+open import Data.Fin
+open import Data.Fin.Closure
+
+open is-iso
+
+{-
+This is a formalisation of a hat puzzle whose statement you can read at any
+of these places:
+
+  https://www.jsoftware.com/pipermail/general/2007-June/030272.html
+  https://www.cut-the-knot.org/blue/PuzzleWithHats.shtml
+  https://twitter.com/gro_tsen/status/1618989823100096512
+
+🎩 SPOILERS AHEAD! 🎩
+-}
+module Hats where
+
+-- We assume there's at least one person, that each person is given a
+-- unique number from 0 to n - 1 during the concertation phase, and that
+-- everyone remembers everyone's numbers.
+module _ (n-1 : Nat) where
+  private
+    n = suc n-1
+    Person = Fin n
+    Hat = Fin n
+    Hats = Person → Hat
+
+  record Strategy : Type where
+    -- `guess i xs` is the guess made by the ith person upon seeing the n - 1
+    -- other hats given by `xs` (a vector of numbers from 0 to n - 1).
+    field
+      guess : Person → (Fin n-1 → Hat) → Hat
+
+    -- The relation `hats ✓ i` means that the ith person guesses correctly,
+    -- given the assignment `hats`.
+    _✓_ : Hats → Person → Type
+    hats ✓ i = guess i (delete hats i) ≡ hats i
+
+    -- We are interested in strategies where at least one person guesses
+    -- correctly for every assignment of hats.
+    field
+      one-right : ∀ hats → Σ Person λ i → hats ✓ i
+
+    -- First, note that, given this requirement, there can be at *most* one
+    -- correct guess for every assignment of hats.
+    -- This follows from a probabilistic argument: every person guesses correctly
+    -- with probability 1/n, so the total number of correct guesses across all
+    -- hat assignments is nⁿ.
+    -- In order to conclude, we use the fact that any surjection between finite
+    -- sets of equal cardinality is an equivalence.
+    exactly-one-right : ∀ hats → is-contr (Σ Person λ i → hats ✓ i)
+    exactly-one-right hats = is-hlevel≃ 0 (Fibre-equiv _ hats e⁻¹) (p-is-equiv .is-eqv hats)
+      where
+        probability : ∀ i → Iso (Σ Hats (_✓ i)) (Fin n-1 → Hat)
+        probability i .fst (hats , _) = delete hats i
+        probability i .snd .inv other .fst = other [ i ≔ guess i other ]
+        probability i .snd .inv other .snd =
+          guess i ⌜ delete (other [ i ≔ guess i other ]) i ⌝ ≡⟨ ap! (funext (delete-insert _ i _)) ⟩
+          guess i other                                      ≡˘⟨ insert-lookup _ i _ ⟩
+          (other [ i ≔ guess i other ]) i                    ∎
+        probability i .snd .rinv _ = funext (delete-insert _ i _)
+        probability i .snd .linv (hats , r) = Σ-prop-path! (funext (insert-delete _ i _ (sym r)))
+
+        only-one : Σ Hats (λ hats → Σ Person (hats ✓_)) ≃ Hats
+        only-one =
+          Σ _ (λ hats → Σ _ λ i → hats ✓ i) ≃⟨ Σ-swap₂ ⟩
+          Σ _ (λ i → Σ _ λ hats → hats ✓ i) ≃⟨ Σ-ap-snd (Iso→Equiv ∘ probability) ⟩
+          Fin n × (Fin n-1 → Fin n)         ≃˘⟨ Fin-suc-Π ⟩
+          (Fin n → Fin n)                   ≃∎
+
+        p : Σ Hats (λ hats → Σ Person (hats ✓_)) → Hats
+        p = fst
+        p-is-equiv : is-equiv p
+        p-is-equiv = Finite-surjection→equiv (inc only-one) p
+          λ other → inc ((other , one-right other) , refl)
+
+  open Strategy public
+
+  -- n-hypercubes of order m. We won't use the extra degree of generality,
+  -- but it doesn't hurt.
+  Hypercube : Nat → Type
+  Hypercube m = (Fin n → Fin m) → Fin m
+
+  -- Latin hypercubes, or n-ary quasigroups.
+  -- Every number appears exactly once on each "line"; equivalently,
+  -- every partial application to n - 1 coordinates is an automorphism.
+  is-latin : ∀ {m} → Hypercube m → Type
+  is-latin {m} h = ∀ (i : Fin n) (xs : Fin n-1 → Fin m) → is-equiv λ x → h (xs [ i ≔ x ])
+
+  Latin-hypercube : Nat → Type
+  Latin-hypercube m = Σ (Hypercube m) is-latin
+
+  -- Every latin n-hypercube h of order n induces a strategy where everyone
+  -- guesses that the multiplication of all the hats is equal to their index.
+  latin→strategy : Latin-hypercube n → Strategy
+  latin→strategy (h , lat) .guess i other = equiv→inverse (lat i other) i
+  latin→strategy (h , lat) .one-right hats =
+    h hats , Equiv.from (eqv (h hats)) refl
+    where
+      module L i = Equiv (_ , lat i (delete hats i))
+      eqv : ∀ (i : Fin n) → (L.from i i ≡ hats i) ≃ (h hats ≡ i)
+      eqv i =
+        L.from i i ≡ hats i ≃⟨ Equiv.adjunct (L.inverse i) ⟩
+        i ≡ L.to i (hats i) ≃⟨ sym-equiv ⟩
+        L.to i (hats i) ≡ i ≃⟨ ∙-pre-equiv (sym (ap h (funext (insert-delete hats i _ refl)))) ⟩
+        h hats ≡ i          ≃∎
+
+  -- In particular, every group structure on Fin n induces a strategy since
+  -- group multiplication is an n-ary equivalence.
+  group→latin : Group-on (Fin n) → Latin-hypercube n
+  group→latin G = mul , mul-equiv
+    where
+      open Group-on G hiding (magma-hlevel)
+
+      mul : ∀ {m} → (Fin m → Fin n) → Fin n
+      mul xs = fold underlying-monoid (tabulate xs)
+
+      mul-equiv : ∀ {m} (i : Fin (suc m)) (xs : Fin m → Fin n)
+                → is-equiv (λ x → mul (xs [ i ≔ x ]))
+      mul-equiv fzero xs = ⋆-equivr _
+      mul-equiv {suc m} (fsuc i) xs = ∙-is-equiv (mul-equiv i (xs ∘ fsuc)) (⋆-equivl _)
+
+  group→strategy : Group-on (Fin n) → Strategy
+  group→strategy = latin→strategy ∘ group→latin

src/TangentBundles.agda

@@ -2,6 +2,7 @@ open import 1Lab.Path.Cartesian
 open import 1Lab.Path.Reasoning
 open import 1Lab.Prelude
 
+open import Algebra.Group.Concrete.Abelian
 open import Algebra.Group.Concrete
 
 open import Data.Set.Truncation
@@ -11,6 +12,7 @@ open import Data.Nat
 open import Data.Sum
 
 open import Homotopy.Space.Suspension.Properties
+open import Homotopy.Connectedness.Automation
 open import Homotopy.Space.Suspension
 open import Homotopy.Connectedness
 open import Homotopy.Space.Circle