chore: only lift ℤ and ℤ/n as needed

Having ℤ unlifted means that we can use the category reasoning
combinators to prove identities of the integers without having to
sprinkle lifts and lowers everywhere.

src/Algebra/Group/Cat/Base.lagda.md

@@ -1,7 +1,10 @@
 <!--
 ```agda
+open import Algebra.Semigroup using (is-semigroup)
 open import Algebra.Prelude
+open import Algebra.Monoid using (is-monoid)
 open import Algebra.Group
+open import Algebra.Magma using (is-magma)
 
 open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Properties
@@ -69,6 +72,34 @@ to-group : ∀ {ℓ} {A : Type ℓ} → make-group A → Group ℓ
 to-group {A = A} mg = el A (mg .make-group.group-is-set) , (to-group-on mg)
 ```
 
+<!--
+```agda
+LiftGroup : ∀ {ℓ} ℓ' → Group ℓ → Group (ℓ ⊔ ℓ')
+LiftGroup {ℓ} ℓ' G = G' where
+  module G = Group-on (G .snd)
+  open is-group
+  open is-monoid
+  open is-semigroup
+  open is-magma
+
+  G' : Group (ℓ ⊔ ℓ')
+  G' .fst = el! (Lift ℓ' ⌞ G ⌟)
+  G' .snd ._⋆_ (lift x) (lift y) = lift (x G.⋆ y)
+  G' .snd .has-is-group .unit = lift G.unit
+  G' .snd .has-is-group .inverse (lift x) = lift (G.inverse x)
+  G' .snd .has-is-group .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set = hlevel 2
+  G' .snd .has-is-group .has-is-monoid .has-is-semigroup .associative = ap lift G.associative
+  G' .snd .has-is-group .has-is-monoid .idl = ap lift G.idl
+  G' .snd .has-is-group .has-is-monoid .idr = ap lift G.idr
+  G' .snd .has-is-group .inversel = ap lift G.inversel
+  G' .snd .has-is-group .inverser = ap lift G.inverser
+
+G→LiftG : ∀ {ℓ} (G : Group ℓ) → Groups.Hom G (LiftGroup lzero G)
+G→LiftG G .hom = lift
+G→LiftG G .preserves .pres-⋆ _ _ = refl
+```
+-->
+
 ## The underlying set
 
 The category of groups admits a `faithful`{.Agda ident=is-faithful}

src/Algebra/Group/Instances/Cyclic.lagda.md

@@ -19,7 +19,6 @@ open import Data.Nat
 open represents-subgroup
 open normal-subgroup
 open is-group-hom
-open Lift
 ```
 -->
 
@@ -29,7 +28,7 @@ module Algebra.Group.Instances.Cyclic where
 
 <!--
 ```agda
-private module ℤ {ℓ} = Group-on (ℤ {ℓ} .snd) hiding (magma-hlevel)
+private module ℤ = Group-on (ℤ .snd) hiding (magma-hlevel)
 ```
 -->
 
@@ -75,32 +74,32 @@ $n$ when $n \geq 1$, and is the infinite cyclic group when $n = 0$.
 
 ```agda
 infix 30 _·ℤ
-_·ℤ : ∀ (n : Nat) {ℓ} → normal-subgroup (ℤ {ℓ}) λ (lift i) → el (n ∣ℤ i) (∣ℤ-is-prop n i)
+_·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-is-prop n i)
 (n ·ℤ) .has-rep .has-unit = ∣ℤ-zero
 (n ·ℤ) .has-rep .has-⋆ = ∣ℤ-+
 (n ·ℤ) .has-rep .has-inv = ∣ℤ-negℤ
-(n ·ℤ) {ℓ} .has-conjugate {lift x} {lift y} = subst (n ∣ℤ_) x≡y+x-y
+(n ·ℤ) .has-conjugate {x} {y} = subst (n ∣ℤ_) x≡y+x-y
   where
     x≡y+x-y : x ≡ y +ℤ (x -ℤ y)
     x≡y+x-y =
-      x                  ≡⟨ ap lower (ℤ.insertl {h = lift {ℓ = ℓ} y} (ℤ.inverser {x = lift y})) ⟩
+      x                  ≡⟨ ℤ.insertl {h = y} (ℤ.inverser {x = y}) ⟩
       y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩
       y +ℤ (x -ℤ y)      ∎
 
 infix 25 ℤ/_
-ℤ/_ : Nat → ∀ {ℓ} → Group ℓ
+ℤ/_ : Nat → Group lzero
 ℤ/ n = ℤ /ᴳ n ·ℤ
 ```
 
 $\ZZ/n\ZZ$ is an [[abelian group]], since the commutativity of
 addition descends to the quotient.
 
 ```agda
-ℤ/n-commutative : ∀ n {ℓ} → is-commutative-group {ℓ} (ℤ/ n)
-ℤ/n-commutative n = elim! λ x y → ap (inc ⊙ lift) (+ℤ-commutative x y)
+ℤ/n-commutative : ∀ n → is-commutative-group (ℤ/ n)
+ℤ/n-commutative n = elim! λ x y → ap inc (+ℤ-commutative x y)
 
 infix 25 ℤ-ab/_
-ℤ-ab/_ : Nat → ∀ {ℓ} → Abelian-group ℓ
+ℤ-ab/_ : Nat → Abelian-group lzero
 ℤ-ab/_ n = from-commutative-group (ℤ/ n) (ℤ/n-commutative n)
 ```
 
@@ -109,24 +108,23 @@ by $1$.
 
 <!--
 ```agda
-module _ (n : Nat) {ℓ} where
-  open Group-on {ℓ} ((ℤ/ n) .snd)
-  ℤ/n = (ℤ/ n) {ℓ}
+module _ (n : Nat) where
+  open Group-on ((ℤ/ n) .snd)
 ```
 -->
 
 ```agda
-  ℤ/n-cyclic : is-cyclic ℤ/n
+  ℤ/n-cyclic : is-cyclic (ℤ/ n)
   ℤ/n-cyclic = inc (1 , gen) where
-    gen : ℤ/n is-generated-by 1
+    gen : ℤ/ n is-generated-by 1
     gen = elim! λ x → inc (x , Integers.induction Int-integers
-      {P = λ x → inc (lift x) ≡ pow ℤ/n 1 x}
+      {P = λ x → inc x ≡ pow (ℤ/ n) 1 x}
       refl
       (λ x →
-        inc (lift x)        ≡ pow ℤ/n 1 x        ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩
-        inc (lift x) ⋆ 1    ≡ pow ℤ/n 1 x ⋆ 1    ≃⟨ ∙-pre-equiv (sym (ap (inc ⊙ lift) (+ℤ-oner x))) ⟩
-        inc (lift (sucℤ x)) ≡ pow ℤ/n 1 x ⋆ 1    ≃⟨ ∙-post-equiv (sym (pow-sucr ℤ/n 1 x)) ⟩
-        inc (lift (sucℤ x)) ≡ pow ℤ/n 1 (sucℤ x) ≃∎)
+        inc x        ≡ pow (ℤ/ n) 1 x        ≃⟨ _ , equiv→cancellable (⋆-equivr 1) ⟩
+        inc x ⋆ 1    ≡ pow (ℤ/ n) 1 x ⋆ 1    ≃⟨ ∙-pre-equiv (sym (ap inc (+ℤ-oner x))) ⟩
+        inc (sucℤ x) ≡ pow (ℤ/ n) 1 x ⋆ 1    ≃⟨ ∙-post-equiv (sym (pow-sucr (ℤ/ n) 1 x)) ⟩
+        inc (sucℤ x) ≡ pow (ℤ/ n) 1 (sucℤ x) ≃∎)
       x)
 ```
 
@@ -148,31 +146,32 @@ module _
   (wraps : x^ pos n ≡ unit)
   where
 
-  ℤ/-out : Groups.Hom (ℤ/ n) G
-  ℤ/-out .hom = Coeq-rec (apply x^-) λ (lift a , lift b , n∣a-b) → zero-diff $
+  ℤ/-out : Groups.Hom (LiftGroup ℓ (ℤ/ n)) G
+  ℤ/-out .hom (lift i) = Coeq-rec (apply x^- ⊙ lift) (λ (a , b , n∣a-b) → zero-diff $
     let k , k*n≡a-b = ∣ℤ→fibre n∣a-b in
     x^ a — x^ b          ≡˘⟨ pres-diff (x^- .preserves) {lift a} {lift b} ⟩
     x^ (a -ℤ b)          ≡˘⟨ ap x^_ k*n≡a-b ⟩
     x^ (k *ℤ pos n)      ≡⟨ ap x^_ (*ℤ-commutative k (pos n)) ⟩
     x^ (pos n *ℤ k)      ≡⟨ pow-* G x (pos n) k ⟩
     pow G ⌜ x^ pos n ⌝ k ≡⟨ ap! wraps ⟩
     pow G unit k         ≡⟨ pow-unit G k ⟩
-    unit                 ∎
+    unit                 ∎)
+    i
   ℤ/-out .preserves .pres-⋆ = elim! λ x y →
     x^- .preserves .pres-⋆ (lift x) (lift y)
 ```
 
 We can check that $\ZZ/0\ZZ \is \ZZ$:
 
 ```agda
-ℤ-ab/0≡ℤ-ab : ∀ {ℓ} → ℤ-ab/ 0 ≡ ℤ-ab {ℓ}
+ℤ-ab/0≡ℤ-ab : ℤ-ab/ 0 ≡ ℤ-ab
 ℤ-ab/0≡ℤ-ab = ∫-Path
   (total-hom
-    (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff (ap lift p)))
+    (Coeq-rec (λ z → z) (λ (_ , _ , p) → ℤ.zero-diff p))
     (record { pres-⋆ = elim! λ _ _ → refl }))
   (is-iso→is-equiv (iso inc (λ _ → refl) (elim! λ _ → refl)))
 
-ℤ/0≡ℤ : ∀ {ℓ} → ℤ/ 0 ≡ ℤ {ℓ}
+ℤ/0≡ℤ : ℤ/ 0 ≡ ℤ
 ℤ/0≡ℤ = Grp→Ab→Grp (ℤ/ 0) (ℤ/n-commutative 0) ∙ ap Abelian→Group ℤ-ab/0≡ℤ-ab
 ```
 
@@ -182,16 +181,16 @@ $x : \ZZ$ to the representative of its congruence class modulo $n$,
 $x \% n$.
 
 ```agda
-ℤ/n≃ℕ<n : ∀ n {ℓ} → .⦃ Positive n ⦄ → ⌞ (ℤ/ n) {ℓ} ⌟ ≃ ℕ< n
-ℤ/n≃ℕ<n n .fst = Coeq-rec (λ (lift i) → i %ℤ n , x%ℤy<y i n)
-  λ (lift x , lift y , p) → Σ-prop-path! (divides-diff→same-rem n x y p)
+ℤ/n≃ℕ<n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ ℕ< n
+ℤ/n≃ℕ<n n .fst = Coeq-rec (λ i → i %ℤ n , x%ℤy<y i n)
+  λ (x , y , p) → Σ-prop-path! (divides-diff→same-rem n x y p)
 ℤ/n≃ℕ<n n .snd = is-iso→is-equiv $ iso
-  (λ (i , p) → inc (lift (pos i)))
+  (λ (i , p) → inc (pos i))
   (λ i → Σ-prop-path! (ℕ<-%ℤ i))
   (elim! λ i → quot (same-rem→divides-diff n (pos (i %ℤ n)) i
     (ℕ<-%ℤ (_ , x%ℤy<y i n))))
 
-Finite-ℤ/n : ∀ n {ℓ} → .⦃ Positive n ⦄ → ⌞ (ℤ/ n) {ℓ} ⌟ ≃ Fin n
+Finite-ℤ/n : ∀ n → .⦃ Positive n ⦄ → ⌞ ℤ/ n ⌟ ≃ Fin n
 Finite-ℤ/n n = ℤ/n≃ℕ<n n ∙e Fin≃ℕ< e⁻¹
 ```
 
@@ -205,6 +204,7 @@ corresponds to $1 : [2!]$.
 ℤ/2→S₂ : Groups.Hom (ℤ/ 2) (S 2)
 ℤ/2→S₂ = ℤ/-out 2 (Equiv.from (Fin-permutations 2) 1)
   (Equiv.injective (Fin-permutations 2) refl)
+  Groups.∘ G→LiftG (ℤ/ 2)
 ```
 
 In order to conclude the proof, we show that the function $f : \ZZ/2\ZZ

src/Algebra/Group/Instances/Dihedral.lagda.md

@@ -37,7 +37,7 @@ by `negation`{.Agda}.
 
 ```agda
 Dih : ∀ {ℓ} → Abelian-group ℓ → Group ℓ
-Dih G = Semidirect-product (ℤ/ 2) (Abelian→Group G) $
+Dih G = Semidirect-product (LiftGroup _ (ℤ/ 2)) (Abelian→Group G) $
   ℤ/-out 2 (F-map-iso Ab↪Grp (negation G)) (ext λ _ → inv-inv)
   where open Abelian-group-on (G .snd)
 ```

src/Algebra/Group/Instances/Integers.lagda.md

@@ -13,7 +13,6 @@ open import Data.Int
 open import Data.Nat
 
 open is-group-hom
-open Lift
 ```
 -->
 
@@ -29,26 +28,24 @@ private module ℤ = Integers Int-integers
 
 # The group of integers {defines="integer-group group-of-integers"}
 
-The fundamental example of an [[abelian group]] is the group of [[**integers**]], $\ZZ$, under
-addition. A type-theoretic interjection is necessary: the integers live
-on the zeroth universe, so to have an $\ell$-sized group of integers, we
-must lift it.
+The fundamental example of an [[abelian group]] is the group of
+[[**integers**]], $\ZZ$, under addition.
 
 ```agda
-ℤ-ab : ∀ {ℓ} → Abelian-group ℓ
+ℤ-ab : Abelian-group lzero
 ℤ-ab = to-ab mk-ℤ where
   open make-abelian-group
-  mk-ℤ : make-abelian-group (Lift _ Int)
+  mk-ℤ : make-abelian-group Int
   mk-ℤ .ab-is-set = hlevel 2
-  mk-ℤ .mul (lift x) (lift y) = lift (x +ℤ y)
-  mk-ℤ .inv (lift x) = lift (negℤ x)
+  mk-ℤ .mul x y = x +ℤ y
+  mk-ℤ .inv x = negℤ x
   mk-ℤ .1g = 0
-  mk-ℤ .idl (lift x) = ap lift (+ℤ-zerol x)
-  mk-ℤ .assoc (lift x) (lift y) (lift z) = ap lift (+ℤ-assoc x y z)
-  mk-ℤ .invl (lift x) = ap lift (+ℤ-invl x)
-  mk-ℤ .comm (lift x) (lift y) = ap lift (+ℤ-commutative x y)
+  mk-ℤ .idl x = +ℤ-zerol x
+  mk-ℤ .assoc x y z = +ℤ-assoc x y z
+  mk-ℤ .invl x = +ℤ-invl x
+  mk-ℤ .comm x y = +ℤ-commutative x y
 
-ℤ : ∀ {ℓ} → Group ℓ
+ℤ : Group lzero
 ℤ = Abelian→Group ℤ-ab
 ```
 
@@ -85,16 +82,22 @@ module _ {ℓ} (G : Group ℓ) where
         pow (a +ℤ b) ⋆ x    ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (pow-sucr (a +ℤ b)) ⟩
         pow (sucℤ (a +ℤ b)) ≡ pow a ⋆ pow (sucℤ b) ≃⟨ ∙-pre-equiv (ap pow (+ℤ-sucr a b)) ⟩
         pow (a +ℤ sucℤ b)   ≡ pow a ⋆ pow (sucℤ b) ≃∎
+```
 
-    pow-hom : Groups.Hom ℤ G
+A type-theoretic interjection is necessary: the integers live on the
+zeroth universe, so to have an $\ell$-sized group of integers, we
+must lift it.
+
+```agda
+    pow-hom : Groups.Hom (LiftGroup ℓ ℤ) G
     pow-hom .hom (lift i) = pow i
     pow-hom .preserves .pres-⋆ (lift a) (lift b) = pow-+ a b
 ```
 
 This is the unique group homomorphism $\ZZ \to G$ that sends $1$ to $x$.
 
 ```agda
-    pow-unique : (g : Groups.Hom ℤ G) → g # 1 ≡ x → g ≡ pow-hom
+    pow-unique : (g : Groups.Hom (LiftGroup ℓ ℤ) G) → g # 1 ≡ x → g ≡ pow-hom
     pow-unique g g1≡x = ext $ ℤ.map-out-unique (λ i → g # lift i)
       (pres-id (g .preserves))
       λ y →
@@ -158,7 +161,7 @@ one generator.
 
 ```agda
 ℤ-free : Free-object Grp↪Sets (el! ⊤)
-ℤ-free .Free-object.free = ℤ
+ℤ-free .Free-object.free = LiftGroup lzero ℤ
 ℤ-free .Free-object.unit _ = 1
 ℤ-free .Free-object.fold {G} x = pow-hom G (x _)
 ℤ-free .Free-object.commute {G} {x} = ext λ _ → pow-1 G (x _)
@@ -173,12 +176,12 @@ notation. In fact, we can show that $n \cdot x$ coincides with the
 multiplication $n \times x$ in the group of integers itself.
 
 ```agda
-pow-ℤ : ∀ {ℓ} a b → Lift.lower (pow (ℤ {ℓ}) (lift a) b) ≡ a *ℤ b
-pow-ℤ {ℓ} a = ℤ.induction (sym (*ℤ-zeror a)) λ b →
-  lower (pow ℤ (lift a) b)        ≡ a *ℤ b      ≃⟨ ap (_+ℤ a) , equiv→cancellable (equiv≃ Lift-≃ Lift-≃ .fst (_ , Group-on.⋆-equivr (ℤ {ℓ} .snd) (lift a)) .snd) ⟩
-  lower (pow ℤ (lift a) b) +ℤ a   ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (ap lower (pow-sucr ℤ (lift a) b)) ⟩
-  lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩
-  lower (pow ℤ (lift a) (sucℤ b)) ≡ a *ℤ sucℤ b ≃∎
+pow-ℤ : ∀ a b → pow ℤ a b ≡ a *ℤ b
+pow-ℤ a = ℤ.induction (sym (*ℤ-zeror a)) λ b →
+  pow ℤ a b        ≡ a *ℤ b      ≃⟨ ap (_+ℤ a) , equiv→cancellable (Group-on.⋆-equivr (ℤ .snd) a) ⟩
+  pow ℤ a b +ℤ a   ≡ a *ℤ b +ℤ a ≃⟨ ∙-pre-equiv (pow-sucr ℤ a b) ⟩
+  pow ℤ a (sucℤ b) ≡ a *ℤ b +ℤ a ≃⟨ ∙-post-equiv (sym (*ℤ-sucr a b)) ⟩
+  pow ℤ a (sucℤ b) ≡ a *ℤ sucℤ b ≃∎
 ```
 :::
 
@@ -238,9 +241,8 @@ We quickly note that $\ZZ$ is torsion-free, since multiplication by
 a nonzero integer is injective.
 
 ```agda
-ℤ-torsion-free : ∀ {ℓ} → is-torsion-free (ℤ {ℓ})
-ℤ-torsion-free (lift n) (k , (k>0 , nk≡0) , _) = ap lift $
-  *ℤ-injectiver (pos k) n 0
-    (λ p → <-not-equal k>0 (pos-injective (sym p)))
-    (sym (pow-ℤ n (pos k)) ∙ ap Lift.lower nk≡0)
+ℤ-torsion-free : is-torsion-free ℤ
+ℤ-torsion-free n (k , (k>0 , nk≡0) , _) = *ℤ-injectiver (pos k) n 0
+  (λ p → <-not-equal k>0 (pos-injective (sym p)))
+  (sym (pow-ℤ n (pos k)) ∙ nk≡0)
 ```

src/Data/Int/DivMod.lagda.md

@@ -21,7 +21,7 @@ module Data.Int.DivMod where
 
 <!--
 ```agda
-private module ℤ = Abelian-group-on (ℤ-ab {lzero} .snd)
+private module ℤ = Abelian-group-on (ℤ-ab .snd)
 ```
 -->
 
@@ -85,7 +85,7 @@ $b - (-a)\%b$ as the remainder.
     lemma =
       assign neg (q * b + suc r)                               ≡⟨ ap (assign neg) (+-commutative (q * b) _) ⟩
       negsuc (r + q * b)                                       ≡˘⟨ negℤ-+ℤ-negsuc r (q * b) ⟩
-      negℤ (pos r) +ℤ negsuc (q * b)                           ≡⟨ ap (_+ℤ negsuc (q * b)) (ap Lift.lower (ℤ.insertl {h = lift (negℤ (pos b'))} (ap lift (+ℤ-invl (pos b'))) {f = lift (negℤ (pos r))})) ⟩
+      negℤ (pos r) +ℤ negsuc (q * b)                           ≡⟨ ap (_+ℤ negsuc (q * b)) (ℤ.insertl {h = negℤ (pos b')} (+ℤ-invl (pos b')) {f = negℤ (pos r)}) ⟩
       ⌜ negℤ (pos b') ⌝ +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡˘⟨ ap¡ (assign-neg b') ⟩
       assign neg b' +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b)     ≡⟨ ap (_+ℤ negsuc (q * b)) (+ℤ-commutative (assign neg b') (pos b' -ℤ pos r)) ⟩
       (pos b' -ℤ pos r) +ℤ assign neg b' +ℤ negsuc (q * b)     ≡˘⟨ +ℤ-assoc (pos b' -ℤ pos r) _ _ ⟩
@@ -135,7 +135,7 @@ hence it must be zero.
   b∣r'-r .fst = q -ℤ q'
   b∣r'-r .snd =
     (q -ℤ q') *ℤ pos b        ≡⟨ *ℤ-distribr-minus (pos b) q q' ⟩
-    q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ap Lift.lower (ℤ.equal-sum→equal-diff (lift (q *ℤ pos b)) (lift (pos r)) (lift (q' *ℤ pos b)) (lift (pos r')) (ap lift (sym (recover p) ∙ recover p'))) ⟩
+    q *ℤ pos b -ℤ q' *ℤ pos b ≡⟨ ℤ.equal-sum→equal-diff (q *ℤ pos b) (pos r) (q' *ℤ pos b) (pos r') (sym (recover p) ∙ recover p') ⟩
     pos r' -ℤ pos r           ≡⟨ pos-pos r' r ⟩
     r' ℕ- r                   ∎
 
@@ -186,7 +186,7 @@ divides-diff→same-rem n x y n∣x-y
     p' : y ≡ (q -ℤ k) *ℤ pos n +ℤ pos r
     p' =
       y                                            ≡˘⟨ negℤ-negℤ y ⟩
-      negℤ (negℤ y)                                ≡⟨ ap Lift.lower (ℤ.insertr (ℤ.inversel {lift x}) {f = lift (negℤ (negℤ y))}) ⟩
+      negℤ (negℤ y)                                ≡⟨ ℤ.insertr (ℤ.inversel {x}) {f = negℤ (negℤ y)} ⟩
       ⌜ negℤ (negℤ y) +ℤ negℤ x ⌝ +ℤ x             ≡⟨ ap! (+ℤ-commutative (negℤ (negℤ y)) _) ⟩
       ⌜ negℤ x -ℤ negℤ y ⌝ +ℤ x                    ≡˘⟨ ap¡ (negℤ-distrib x (negℤ y)) ⟩
       negℤ ⌜ x -ℤ y ⌝ +ℤ x                         ≡˘⟨ ap¡ z ⟩

src/Homotopy/Space/Circle.lagda.md

@@ -300,9 +300,9 @@ loopⁿ-+ a = Integers.induction Int-integers
 
 π₁S¹≡ℤ : π₁Groupoid.π₁ S¹∙ S¹-is-groupoid ≡ ℤ
 π₁S¹≡ℤ = sym $ ∫-Path
-  (total-hom (Equiv.from ΩS¹≃integers ∘ Lift.lower)
-    (record { pres-⋆ = λ (lift a) (lift b) → loopⁿ-+ a b }))
-  (∙-is-equiv (Lift-≃ .snd) ((ΩS¹≃integers e⁻¹) .snd))
+  (total-hom (Equiv.from ΩS¹≃integers)
+    (record { pres-⋆ = loopⁿ-+ }))
+  ((ΩS¹≃integers e⁻¹) .snd)
 ```
 
 Furthermore, since the loop space of the circle is a set, we automatically