(p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    (R : Type u₁) →
      [inst : CommSemiring R] →
        [CharP R p] →
          [PerfectRing R p] →
            (S : Type u₂) → [inst_3 : CommSemiring S] → [inst_4 : CharP S p] → (R →+* S) ≃ (R →+* Perfection S p)