diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda
index 49abf3f..395d08a 100644
--- a/src/NonEmpty.agda
+++ b/src/NonEmpty.agda
@@ -24,6 +24,25 @@ foldl : {A B : Type} → (B → A → B) → B → List⁺ A → B
 foldl _+_ acc [ x ]⁺ = acc + x
 foldl _+_ acc (x ∷⁺ xs) = foldl _+_ (acc + x) xs
 
+cons⁺ : {A : Type} → A → List A → List⁺ A
+cons⁺ a [] = [ a ]⁺
+cons⁺ a (x ∷ xs) = a ∷⁺ cons⁺ x xs
+
+_⁺++⁺_ : {A : Type} → List⁺ A → List⁺ A → List⁺ A
+[ x ]⁺ ⁺++⁺ l₁ = x ∷⁺ l₁
+(x ∷⁺ l₀) ⁺++⁺ l₁ = x ∷⁺ (l₀ ⁺++⁺ l₁)
+
+_++⁺_ : {A : Type} → List A → List⁺ A → List⁺ A
+[] ++⁺ l₁ = l₁
+(x ∷ l₀) ++⁺ l₁ = x ∷⁺ (l₀ ++⁺ l₁)
+
+_⁺++_ : {A : Type} → List⁺ A → List A → List⁺ A
+[ x ]⁺ ⁺++ [] = [ x ]⁺
+[ x ]⁺ ⁺++ (y ∷ l₁) = (x ∷⁺ [ y ]⁺ ) ⁺++ l₁
+(x ∷⁺ l₀) ⁺++ l₁ = x ∷⁺ (l₀ ⁺++ l₁)
+
+infixr 20 _⁺++⁺_ _++⁺_ _⁺++_
+
 list⁺-to-list : {A : Type} → List⁺ A → List A
 list⁺-to-list [ x ]⁺ = x ∷ []
 list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs
@@ -39,10 +58,7 @@ vec-to-list⁺ (x V.∷ xs@(_ V.∷ _)) = x ∷⁺ vec-to-list⁺ xs
 list-to-list⁺? : {A : Type} → List A → Maybe (List⁺ A)
 list-to-list⁺? [] = cake
 list-to-list⁺? (x ∷ xs) = real (cons⁺ x xs)
-  where
-    cons⁺ : {A : Type} → A → List A → List⁺ A
-    cons⁺ a [] = [ a ]⁺
-    cons⁺ a (x ∷ xs) = a ∷⁺ cons⁺ x xs
+
 
 instance
   ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A)