Credit to Lambda Duck, I'm just posting it here for sharing convenience

MultiplyCircle.agda

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.HITs.S1

SInt : Type₀
SInt = base ≡ base

module _ {A : Set} (p : A ≡ A) (a : A) where
  mhelix : S¹ → Set
  mhelix base = A
  mhelix (loop i) = p i

  mencode : ∀ x → base ≡ x → mhelix x
  mencode x p = subst mhelix p a

  SIntElim : SInt → A
  SIntElim = mencode base

addNPath2 : (n : SInt) → (base ≡ base) ≡ (base ≡ base)
addNPath2 n i = base ≡ n i

_*S_ : SInt → SInt → SInt
n *S m = SIntElim (addNPath2 n) refl m

_*S'_ : SInt → SInt → SInt
(n *S' m) i = case n i of λ where
   base → base
   (loop i) → m i

two : SInt
two = loop ∙ loop

three : SInt
three = loop ∙∙ loop ∙∙ loop

four : SInt
four = two *S two

example : SInt
example = three *S' (three *S three)

{-
Normalize example

λ i₁ →
  hcomp
  (λ i₂ .o →
     (λ { base → base
        ; (loop i)
            → transp
              (λ j →
                 base ≡
                 hcomp (λ { j₁ (j = i0) → loop (~ j₁) ; j₁ (j = i1) → loop j₁ })
                 (loop j))
              i0
              (transp
               (λ i₃ →
                  base ≡
                  hcomp (λ { j (i₃ = i0) → loop (~ j) ; j (i₃ = i1) → loop j })
                  (loop i₃))
               i0
               (transp
                (λ i₃ →
                   base ≡
                   hcomp (λ { j (i₃ = i0) → loop (~ j) ; j (i₃ = i1) → loop j })
                   (loop i₃))
                i0 (λ _ → base)))
              i
        ; (hcomp {.ℓ-zero} {.S¹} {φ = φ} u a)
            → hcomp
              (λ i₃ .o₁ →
                 transp (λ i₄ → S¹) i₃
                 (.extendedlambda1
                  (λ i₄ →
                     hcomp (λ { j (i₄ = i0) → loop (~ j) ; j (i₄ = i1) → loop j })
                     (loop i₄))
                  (transp
                   (λ j →
                      base ≡
                      hcomp (λ { j₁ (j = i0) → loop (~ j₁) ; j₁ (j = i1) → loop j₁ })
                      (loop j))
                   i0
                   (transp
                    (λ i₄ →
                       base ≡
                       hcomp (λ { j (i₄ = i0) → loop (~ j) ; j (i₄ = i1) → loop j })
                       (loop i₄))
                    i0
                    (transp
                     (λ i₄ →
                        base ≡
                        hcomp (λ { j (i₄ = i0) → loop (~ j) ; j (i₄ = i1) → loop j })
                        (loop i₄))
                     i0 (λ _ → base))))
                  i₁ (u i₃ _)))
              (transp (λ i₃ → S¹) i0
               (.extendedlambda1
                (λ i₃ →
                   hcomp (λ { j (i₃ = i0) → loop (~ j) ; j (i₃ = i1) → loop j })
                   (loop i₃))
                (transp
                 (λ j →
                    base ≡
                    hcomp (λ { j₁ (j = i0) → loop (~ j₁) ; j₁ (j = i1) → loop j₁ })
                    (loop j))
                 i0
                 (transp
                  (λ i₃ →
                     base ≡
                     hcomp (λ { j (i₃ = i0) → loop (~ j) ; j (i₃ = i1) → loop j })
                     (loop i₃))
                  i0
                  (transp
                   (λ i₃ →
                      base ≡
                      hcomp (λ { j (i₃ = i0) → loop (~ j) ; j (i₃ = i1) → loop j })
                      (loop i₃))
                   i0 (λ _ → base))))
                i₁ a))
        })
     ((λ { (i₁ = i0) → loop (~ i₂) ; (i₁ = i1) → loop i₂ }) _))
  (hcomp
   (λ i₂ .o →
      primPOr (~ i₁) i₁ (λ _ → base)
      (λ _ →
         hcomp (λ { j (i₂ = i0) → loop (~ j) ; j (i₂ = i1) → loop j })
         (loop i₂))
      _)
   (hcomp
    (λ i₂ .o →
       primPOr (~ i₁) i₁ (λ _ → base)
       (λ _ →
          hcomp (λ { j (i₂ = i0) → loop (~ j) ; j (i₂ = i1) → loop j })
          (loop i₂))
       _)
    (hcomp
     (λ i₂ .o →
        primPOr (~ i₁) i₁ (λ _ → base)
        (λ _ →
           hcomp (λ { j (i₂ = i0) → loop (~ j) ; j (i₂ = i1) → loop j })
           (loop i₂))
        _)
     base)))
-}