renamed N+N=N

Freek98 · Freek98 · commit 34d491f5611d · 2025-08-14T16:37:29.000+02:00
diff --git a/Cubical/Data/Nat/Bijections/Sum.agda b/Cubical/Data/Nat/Bijections/Sum.agda
@@ -71,5 +71,5 @@ private
   partitionDouble≅ℕ : Iso (partition double refl doubleInc) ℕ
   partitionDouble≅ℕ = partition≅ℕ double refl doubleInc
 
-ℕ≅ℕ⊎ℕ : Iso (ℕ ⊎ ℕ) ℕ
-ℕ≅ℕ⊎ℕ = compIso (invIso partitionDouble≅ℕ⊎ℕ) partitionDouble≅ℕ
+ℕ⊎ℕ≅ℕ : Iso (ℕ ⊎ ℕ) ℕ
+ℕ⊎ℕ≅ℕ = compIso (invIso partitionDouble≅ℕ⊎ℕ) partitionDouble≅ℕ
