{K : semiOutParam (Type u_1)} →
  (mul : K → K → K) →
    (∀ (a b c : K), a * b * c = a * (b * c)) →
      (one : K) →
        (∀ (a : K), 1 * a = a) →
          (∀ (a : K), a * 1 = a) →
            (npow : ℕ → K → K) →
              (∀ (x : K), npow 0 x = 1) → (∀ (n : ℕ) (x : K), npow (n + 1) x = npow n x * x) → (K → K) → K → K → K