injℕ : ∀ {x y} → (S x) ≅ (S y) → x ≅ y
injℕ {x = x} (IdPath .(S _)) = IdPath x

injℕ² : ∀ {x y : ℕ} → (p : S x ≅ S y) → ap S (injℕ p) ≅ p
injℕ² {x = x} (IdPath (S x)) = IdPath (IdPath (S x))

-- хз как назвать
rep2 : ∀ {i} {A : U i} {a b c d : A} (p : a ≅ b) (q : c ≅ d) (h : a ≅ c) → b ≅ d
rep2 (IdPath .x₁) (IdPath x₁) (IdPath .x₁) = IdPath x₁

Setℕ : isSet ℕ
Setℕ Z Z (IdPath Z) (IdPath Z) = IdPath (IdPath Z)
Setℕ (S x) (S y) p q  =
  rep2 (injℕ² p) (injℕ² q) (ap (ap S) (Setℕ x y (injℕ p) (injℕ q)))