Merge branch 'master' into sierpinski-object

.github/workflows/main.yml

@@ -13,14 +13,37 @@ jobs:
     if: github.event.pull_request.draft == false
     steps:
     - name: "Clone repository"
-      uses: actions/checkout@v2
+      uses: actions/checkout@v4
+
+    - name: "Print environment information"
+      shell: bash
+      run: |
+        echo "github.ref_name = ${{ github.ref_name }}"
+        echo "github.sha = ${{ github.sha }}"
+        echo "github.event.before = ${{ github.event.before }}"
+
+    - name: "Restore cached .agdai files"
+      id: cache-agdai-restore
+      uses: actions/cache/restore@v4
+      with:
+        path: _build
+        key: ${{ runner.os }}-agdai-cache-${{ github.ref_name }}-${{ github.event.before }}
+
     - name: Run Agda
       id: typecheck
       uses: ayberkt/[email protected]
       with:
         main-file: AllModulesIndex.lagda
         source-dir: source
         unsafe: true
+
+    - name: "Save .agdai files"
+      id: cache-agdai-save
+      uses: actions/cache/save@v4
+      with:
+        path: _build
+        key: ${{ runner.os }}-agdai-cache-${{ github.ref_name }}-${{ github.sha }}
+
     - name: Upload HTML
       id: html-upload
       if: github.ref == 'refs/heads/master'

imports.sh

@@ -0,0 +1,133 @@
+#!/usr/bin/env bash
+set -Eeo pipefail
+
+# Created by Tom de Jong in September 2024.
+
+
+# Ensure we have GNU-style sed
+# See https://stackoverflow.com/questions/4247068/sed-command-with-i-option-failing-on-mac-but-works-on-linux
+if [[ "$OSTYPE" == "darwin"* ]]; then
+  # Require gnu-sed.
+  if ! [ -x "$(command -v gsed)" ]; then
+    echo "Error: 'gsed' is not istalled." >&2
+    echo "If you are using Homebrew, install with 'brew install gnu-sed'." >&2
+    exit 1
+  fi
+  sed_cmd=gsed
+else
+  sed_cmd=sed
+fi
+
+
+# "catch exit status 1" grep wrapper
+# https://stackoverflow.com/questions/6550484/prevent-grep-returning-an-error-when-input-doesnt-match/49627999#49627999
+c1grep() { grep "$@" || test $? = 1; }
+
+
+print_usage() {
+  printf "From TypeTopology/source, run this script as
+  ./imports.sh UF/Embeddings.lagda
+to report redundant imports in UF/Embeddings.lagda.
+
+Alternatively, use the -d (directory) flag to report redundant
+imports in all .lagda files in the UF/ directory, e.g.
+  ./imports.sh -d UF/
+NB: The forward slash at the end of the directory is important.
+
+Use the -r flag to remove redundant imports (without reporting them), e.g.
+  ./imports.sh -d -r UF/
+  ./imports.sh -r UF/Embeddings.lagda
+
+Wrong flags, or the -h (help) flag, displays this message.
+"
+}
+
+
+# Implement option flags
+# https://stackoverflow.com/questions/7069682/how-to-get-arguments-with-flags-in-bash
+dir_flag=false
+rem_flag=false
+
+OPTIND=1
+while getopts 'drh' flag; do
+  case "${flag}" in
+    d) dir_flag=true ;;
+    r) rem_flag=true ;;
+    h) print_usage
+       exit 0 ;;
+    *) print_usage
+       exit 1 ;;
+  esac
+done
+
+
+# Discard options so we can get the file/directory name next
+shift "$((OPTIND-1))"
+if [ $# -ge 1 ] && [ -n "$1" ]; then
+  input=$1
+else
+  print_usage
+  exit 1
+fi
+
+
+check_imports() {
+  unused=()
+  local file=$1
+
+  # Get all line numbers that have 'open import ...'
+  imports=$(c1grep -n "open import" $file | cut -d ':' -f1)
+
+  # Get the cluster, e.g. 'UF' or 'DomainTheory/Lifting'
+  cluster=$(dirname $file)
+
+  # And with '.' instead of '/'
+  clustermod=$(echo $cluster | ${sed_cmd} 's/\//./')
+
+  # Get the (relative) module name
+  modname=$(basename $file | ${sed_cmd} 's/.lagda$//')
+
+  # Set up a temporary file for testing
+  temp="UnusedImportTesting"
+  fulltemp="${cluster}/${temp}.lagda"
+
+  local i
+  for i in $imports;
+  do
+    ${sed_cmd} "$i s/^/-- /" $file > $fulltemp # Comment out an import
+
+    # Replace module name to match the temporary file
+    oldmod="module ${clustermod}.${modname}"
+    newmod="module ${clustermod}.${temp}"
+    ${sed_cmd} -i "s/${oldmod}/${newmod}/" $fulltemp
+
+    # Try to scope-check and save (line numbers of) any redundant imports
+    agda --only-scope-checking $fulltemp > /dev/null &&
+      {
+        unused+=( $i )
+      }
+
+    rm $fulltemp
+  done
+
+  if $rem_flag; then
+      ${sed_cmd} -i "${unused[*]/%/d;}" $file # Remove redundant imports
+  else # Report redundant imports
+      for i in $unused;
+      do
+	import=$(${sed_cmd} -n "${i}p" $file | awk -F 'open import ' '{print $2}')
+	echo "Importing $import was not necessary"
+      done
+  fi
+}
+
+
+if $dir_flag; then # Check all *.lagda files in given directory
+  for i in ${input}*.lagda
+  do
+    check_imports $i
+    echo "Done with $(basename $i)"
+  done
+else
+  check_imports $input # Check a single file
+fi

source/AllModulesIndex.lagda

@@ -4,7 +4,7 @@
    constructive univalent mathematics
    written in Agda
 
-   Tested with Agda 2.6.4.3
+   Tested with Agda 2.6.4.3 and 2.7.0
 
    Martin Escardo and collaborators, 2010--2024--∞
    Continuously evolving.

source/Apartness/Definition.lagda

@@ -0,0 +1,205 @@
+Martin Escardo, 26 January 2018.
+
+Moved from the file TotallySeparated 22 August 2024.
+
+Definition of apartness relation and basic general facts.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+module Apartness.Definition where
+
+open import MLTT.Spartan
+open import UF.DiscreteAndSeparated hiding (tight)
+open import UF.FunExt
+open import UF.Lower-FunExt
+open import UF.NotNotStablePropositions
+open import UF.PropTrunc
+open import UF.Sets
+open import UF.Sets-Properties
+open import UF.Subsingletons
+open import UF.Subsingletons-FunExt
+
+is-prop-valued
+ is-irreflexive
+ is-symmetric
+ is-strongly-cotransitive
+ is-tight
+ is-strong-apartness
+  : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
+
+is-prop-valued           _♯_ = ∀ x y → is-prop (x ♯ y)
+is-irreflexive           _♯_ = ∀ x → ¬ (x ♯ x)
+is-symmetric             _♯_ = ∀ x y → x ♯ y → y ♯ x
+is-strongly-cotransitive _♯_ = ∀ x y z → x ♯ y → (x ♯ z) + (y ♯ z)
+is-tight                 _♯_ = ∀ x y → ¬ (x ♯ y) → x ＝ y
+is-strong-apartness      _♯_ = is-prop-valued _♯_
+                             × is-irreflexive _♯_
+                             × is-symmetric _♯_
+                             × is-strongly-cotransitive _♯_
+
+Strong-Apartness : 𝓤 ̇ → (𝓥 : Universe) → 𝓥 ⁺ ⊔ 𝓤 ̇
+Strong-Apartness X 𝓥 = Σ _♯_ ꞉ (X → X → 𝓥 ̇) , is-strong-apartness _♯_
+
+\end{code}
+
+Not-not equal elements are not apart, and hence, in the presence of
+tightness, they are equal. It follows that tight apartness types are
+sets.
+
+\begin{code}
+
+double-negation-of-equality-gives-negation-of-apartness
+ : {X : 𝓤 ̇ } (x y : X) (_♯_ : X → X → 𝓥 ̇ )
+ → is-irreflexive _♯_
+ → ¬¬ (x ＝ y)
+ → ¬ (x ♯ y)
+double-negation-of-equality-gives-negation-of-apartness x y _♯_ i
+ = contrapositive f
+ where
+  f : x ♯ y → ¬ (x ＝ y)
+  f a refl = i y a
+
+tight-types-are-¬¬-separated' : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                              → is-irreflexive _♯_
+                              → is-tight _♯_
+                              → is-¬¬-separated X
+tight-types-are-¬¬-separated' _♯_ i t = f
+ where
+  f : ∀ x y → ¬¬ (x ＝ y) → x ＝ y
+  f x y φ = t x y (double-negation-of-equality-gives-negation-of-apartness
+                    x y _♯_ i φ)
+
+tight-types-are-sets' : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                      → funext 𝓤 𝓤₀
+                      → is-irreflexive _♯_
+                      → is-tight _♯_
+                      → is-set X
+tight-types-are-sets' _♯_ fe i t =
+ ¬¬-separated-types-are-sets fe (tight-types-are-¬¬-separated' _♯_ i t)
+
+\end{code}
+
+To define apartness we need to define (weak) cotransitivity, and for
+this we need to assume the existence of propositional truncations.
+
+\begin{code}
+
+module Apartness (pt : propositional-truncations-exist) where
+
+ open PropositionalTruncation pt
+
+ is-cotransitive is-apartness : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
+
+ is-cotransitive _♯_ = ∀ x y z → x ♯ y → x ♯ z ∨ y ♯ z
+ is-apartness    _♯_ = is-prop-valued _♯_
+                     × is-irreflexive _♯_
+                     × is-symmetric _♯_
+                     × is-cotransitive _♯_
+
+ Apartness : 𝓤 ̇ → (𝓥 : Universe) → 𝓥 ⁺ ⊔ 𝓤 ̇
+ Apartness X 𝓥 = Σ _♯_ ꞉ (X → X → 𝓥 ̇) , is-apartness _♯_
+
+ apartness-is-prop-valued : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                          → is-apartness _♯_
+                          → is-prop-valued _♯_
+ apartness-is-prop-valued _♯_ (p , i , s , c) = p
+
+ apartness-is-irreflexive : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                          → is-apartness _♯_
+                          → is-irreflexive _♯_
+ apartness-is-irreflexive _♯_ (p , i , s , c) = i
+
+ apartness-is-symmetric : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                        → is-apartness _♯_
+                        → is-symmetric _♯_
+ apartness-is-symmetric _♯_ (p , i , s , c) = s
+
+ apartness-is-cotransitive : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                           → is-apartness _♯_
+                           → is-cotransitive _♯_
+ apartness-is-cotransitive _♯_ (p , i , s , c) = c
+
+ not-not-equal-not-apart : {X : 𝓤 ̇ } (x y : X) (_♯_ : X → X → 𝓥 ̇ )
+                         → is-apartness _♯_
+                         → ¬¬ (x ＝ y)
+                         → ¬ (x ♯ y)
+ not-not-equal-not-apart x y _♯_ (_ , i , _ , _) =
+  double-negation-of-equality-gives-negation-of-apartness x y _♯_ i
+
+ tight-types-are-¬¬-separated : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                              → is-apartness _♯_
+                              → is-tight _♯_
+                              → is-¬¬-separated X
+ tight-types-are-¬¬-separated _♯_ (_ , i , _ , _) =
+  tight-types-are-¬¬-separated' _♯_ i
+
+ tight-types-are-sets : {X : 𝓤 ̇ } (_♯_ : X → X → 𝓥 ̇ )
+                      → funext 𝓤 𝓤₀
+                      → is-apartness _♯_
+                      → is-tight _♯_
+                      → is-set X
+ tight-types-are-sets _♯_ fe (_ , i , _ , _) = tight-types-are-sets' _♯_ fe i
+
+\end{code}
+
+The above use apartness data, but its existence is enough, because
+being a ¬¬-separated type and being a set are propositions.
+
+\begin{code}
+
+ tight-separated' : funext 𝓤 𝓤
+                  → {X : 𝓤 ̇ }
+                  → (∃ _♯_ ꞉ (X → X → 𝓤 ̇ ), is-apartness _♯_ × is-tight _♯_)
+                  → is-¬¬-separated X
+ tight-separated' {𝓤} fe {X} = ∥∥-rec (being-¬¬-separated-is-prop fe) f
+   where
+    f : (Σ _♯_ ꞉ (X → X → 𝓤 ̇ ), is-apartness _♯_ × is-tight _♯_)
+      → is-¬¬-separated X
+    f (_♯_ , a , t) = tight-types-are-¬¬-separated _♯_ a t
+
+ tight-types-are-sets'' : funext 𝓤 𝓤
+                        → {X : 𝓤 ̇ }
+                        → (∃ _♯_ ꞉ (X → X → 𝓤 ̇ ), is-apartness _♯_ × is-tight _♯_)
+                        → is-set X
+ tight-types-are-sets'' {𝓤} fe {X} = ∥∥-rec (being-set-is-prop fe) f
+   where
+    f : (Σ _♯_ ꞉ (X → X → 𝓤 ̇ ), is-apartness _♯_ × is-tight _♯_) → is-set X
+    f (_♯_ , a , t) = tight-types-are-sets _♯_ (lower-funext 𝓤 𝓤 fe) a t
+
+\end{code}
+
+The following is the standard equivalence relation induced by an
+apartness relation. The tightness axiom defined above says that this
+equivalence relation is equality.
+
+\begin{code}
+
+ is-equiv-rel : {X : 𝓤 ̇ } → (X → X → 𝓥 ̇ ) → 𝓤 ⊔ 𝓥 ̇
+ is-equiv-rel _≈_ = is-prop-valued _≈_
+                  × reflexive _≈_
+                  × symmetric _≈_
+                  × transitive _≈_
+
+ negation-of-apartness-is-equiv-rel : {X : 𝓤 ̇ }
+                                    → funext 𝓤 𝓤₀
+                                    → (_♯_ : X → X → 𝓤 ̇ )
+                                    → is-apartness _♯_
+                                    → is-equiv-rel (λ x y → ¬ (x ♯ y))
+ negation-of-apartness-is-equiv-rel {𝓤} {X} fe _♯_ (♯p , ♯i , ♯s , ♯c)
+  = p , ♯i , s , t
+  where
+   p : (x y : X) → is-prop (¬ (x ♯ y))
+   p x y = negations-are-props fe
+
+   s : (x y : X) → ¬ (x ♯ y) → ¬ (y ♯ x)
+   s x y u a = u (♯s y x a)
+
+   t : (x y z : X) → ¬ (x ♯ y) → ¬ (y ♯ z) → ¬ (x ♯ z)
+   t x y z u v a = v (♯s z y (left-fails-gives-right-holds (♯p z y) b u))
+    where
+     b : (x ♯ y) ∨ (z ♯ y)
+     b = ♯c x z y a
+
+\end{code}