Upgrade 1lab and clean up code

RedPRL · Jun 10, 2024 · f0c9ed2 · f0c9ed2
1 parent d38bcc6
commit f0c9ed2
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -31,7 +31,7 @@ FROM alpine AS onelab
 RUN apk add --no-cache git
 
 WORKDIR /dist/1lab
-ARG ONELAB_VERSION=5cb0edee762e05f14869817fbed5af3412da5e1f
+ARG ONELAB_VERSION=a3feb5b6ff900829e63a80abc1af18e9d8a35c46
 RUN \
   git init && \
   git remote add origin https://github.com/plt-amy/1lab && \

diff --git a/src/Mugen/Cat/HierarchyTheory/McBride.agda b/src/Mugen/Cat/HierarchyTheory/McBride.agda
@@ -15,7 +15,7 @@ open import Mugen.Cat.HierarchyTheory
 import Mugen.Order.Reasoning as Reasoning
 
 private variable
-  o o' r r' : Level
+  o r : Level
 
 --------------------------------------------------------------------------------
 -- The McBride Hierarchy Theory
@@ -116,7 +116,7 @@ module _ where
 
   McBride-functor : Functor (Displacements o r) (Hierarchy-theories o (o ⊔ r))
   McBride-functor .F₀ (_ , 𝒟) = McBride 𝒟
-  McBride-functor .F₁ σ .nat .η L .hom (l , d) = l , σ .hom # d
+  McBride-functor .F₁ σ .nat .η L .hom (l , d) = l , σ # d
   McBride-functor .F₁ {A , 𝒟} {B , ℰ} σ .nat .η L .pres-≤[]-equal {l1 , d1} {l2 , d2} =
     let module A = Reasoning A
         module B = Reasoning B