defn: Ordered families of equivalences (#245)

OFEs are a presentation of certain metric spaces which see some use in the literature on guarded recursion/step indexing, e.g. the “standard” model of the Iris logic lives in the category of COFEs.
the1lab · Aug 10, 2023 · 08b3d7e · 08b3d7e
1 parent 09ed1f3
commit 08b3d7e
Show file tree

Hide file tree

Showing 18 changed files with 1,348 additions and 46 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -32,8 +32,8 @@ jobs:
         uses: actions/cache@v3
         with:
           path: _build
-          key: shake-3-${{ env.shake_version }}-${{ github.run_id }}
-          restore-keys: shake-3-${{ env.shake_version }}-
+          key: shake-4-${{ env.shake_version }}-${{ github.run_id }}
+          restore-keys: shake-4-${{ env.shake_version }}-
 
       - name: Build 🛠️
         run: |

diff --git a/src/1Lab/Reflection.lagda.md b/src/1Lab/Reflection.lagda.md
@@ -8,7 +8,7 @@ open import 1Lab.Type hiding (absurd)
 open import Data.Product.NAry
 open import Data.Vec.Base
 open import Data.Bool
-open import Data.List
+open import Data.List.Base
 ```
 -->
 
@@ -27,7 +27,7 @@ open import Meta.Alt public
 
 open Data.Vec.Base using (Vec ; [] ; _∷_ ; lookup ; tabulate) public
 open Data.Product.NAry using ([_]) public
-open Data.List public
+open Data.List.Base public
 open Data.Bool public
 ```
 

diff --git a/src/1Lab/Reflection/HLevel.agda b/src/1Lab/Reflection/HLevel.agda
@@ -10,7 +10,7 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Bool
-open import Data.List
+open import Data.List.Base
 
 open import Meta.Foldable
 
@@ -678,11 +678,6 @@ instance
   decomp-univalence : ∀ {ℓ} {A B : Type ℓ} → hlevel-decomposition (A ≡ B)
   decomp-univalence = decomp (quote ≡-is-hlevel) (`level ∷ `search ∷ `search ∷ [] )
 
-  -- List isn't really a type on the same footing as all the others, but
-  -- we're here, so we might as well, right?
-  decomp-list : ∀ {ℓ} {A : Type ℓ} → hlevel-decomposition (List A)
-  decomp-list = decomp (quote ListPath.List-is-hlevel) (`level-minus 2 ∷ `search ∷ [])
-
   -- This one really ought to work with instance selection only, but
   -- Agda has trouble with the (1 + k + n) level in H-Level-n-Type. The
   -- decomposition here is a bit more flexible.

diff --git a/src/1Lab/Reflection/Marker.agda b/src/1Lab/Reflection/Marker.agda
@@ -3,7 +3,7 @@ open import 1Lab.Path
 open import 1Lab.Type
 
 open import Data.Maybe.Base
-open import Data.List
+open import Data.List.Base
 
 open import Prim.Data.Nat
 

diff --git a/src/1Lab/Reflection/Record.agda b/src/1Lab/Reflection/Record.agda
@@ -4,7 +4,6 @@ open import 1Lab.Equiv
 open import 1Lab.Path
 open import 1Lab.Type
 
-open import Data.List
 
 import Prim.Data.Sigma as S
 import Prim.Data.Nat as N

diff --git a/src/1Lab/Reflection/Variables.agda b/src/1Lab/Reflection/Variables.agda
@@ -3,7 +3,7 @@ open import 1Lab.Type
 
 open import Data.Fin.Base
 open import Data.Nat.Base
-open import Data.List hiding (reverse)
+open import Data.List.Base hiding (reverse)
 
 module 1Lab.Reflection.Variables where