Added it, btw is there something like spoiler tag to make it collapsed initially and not clutter up description?

No, it is not abuse of logic: fix (S . (* Z)) should have 1 === S Z as fixpoint, because
S . (* Z) $ S Z = S Z (1 + 1 * 0 = 1); and your definition successfully yields it for fix (S . (Z *)) = S Z.

Just in case: it has changed slightly.

module Counting.Preloaded where
import Control.Arrow ((***))

data Nat = Z | S Nat deriving (Show, Eq, Ord)

nat :: a -> (Nat -> a) -> Nat -> a
nat a _ Z = a
nat _ aa (S n) = aa n

iterNat :: (a -> a) -> Nat -> (a -> a)
iterNat _ Z = id
iterNat aa (S n) = aa . iterNat aa n

natUnderflow :: String
natUnderflow = "Nat is non-negative"

instance Num Nat where
  (+) = iterNat S
  a * b = iterNat (b+) a Z
  a - Z = a
  Z - b = error natUnderflow
  S a - S b = a - b
  abs = id
  signum Z = Z
  signum (S _) = S Z
  fromInteger x
    | x < 0 = error natUnderflow
    | x == 0 = Z
    | otherwise = S $ fromInteger $ x - 1

instance Enum Nat where
  toEnum x
    | x < 0 = error natUnderflow
    | x == 0 = Z
    | otherwise = S $ toEnum $ x - 1
  fromEnum x = iterNat (+1) x 0

instance Real Nat where toRational = toRational . fromEnum

instance Integral Nat where
  quotRem a Z = error "divide by zero"
  quotRem a b = until ((< b) . snd) (S *** subtract b) (Z, a)
  divMod = quotRem
  toInteger n = iterNat (+1) n 0

I have updated description ("Order of inhabitants in infinite lists won't be tested."), hope it clarifies it. It was complementary task, so I think strictness is unnecessary.

Here:

module Counting.Preloaded where
import Control.Arrow ((***))

data Nat = Z | S Nat deriving (Show, Eq, Ord)

nat :: a -> (Nat -> a) -> Nat -> a
nat a _ Z = a
nat _ aa (S n) = aa n

iterNat :: (a -> a) -> a -> Nat -> a
iterNat _ a Z = a
iterNat aa a (S n) = iterNat aa (aa a) n

natUnderflow :: String
natUnderflow = "Nat is non-negative"

instance Num Nat where
  (+) = iterNat S
  a * b = iterNat (+a) Z b
  a - Z = a
  Z - b = error natUnderflow
  S a - S b = a - b
  abs = id
  signum Z = Z
  signum (S _) = S Z
  fromInteger x
    | x < 0 = error natUnderflow
    | x == 0 = Z
    | otherwise = S $ fromInteger $ x - 1

instance Enum Nat where
  toEnum x
    | x < 0 = error natUnderflow
    | x == 0 = Z
    | otherwise = S $ toEnum $ x - 1
  fromEnum = iterNat (+1) 0

instance Real Nat where toRational = toRational . fromEnum

instance Integral Nat where
  quotRem a Z = error "divide by zero"
  quotRem a b = until ((< b) . snd) (S *** subtract b) (Z, a)
  divMod = quotRem
  toInteger = iterNat (+1) 0

In addition, according to the approach, mentioned in that paper, you could implement set of all subsets in haskell as

powerset :: [a] -> [[a]]
powerset = filterM $ const [False, True]

Good question)
Yes, when count @t is infinity we could not conclude, that t is countable (in mathematical sense).

So ℵ₀ = count @Nat < count @[Nat] = 2^ℵ₀ in terms of cardinal numbers,
and type/set t is countable iff count @t == count @Nat.

We can not express such things in haskell, so when infinity, we just write all formally.

Also if count @x >= 2 then type Nat -> x is not countable.

You always can go to Solutions section and then Show Kata Test Cases.

Another approach (without Proxy, using TypeApplications) could be found in this kata.

Here:

{-# LANGUAGE FlexibleInstances #-}
module YonedaLemmaPreloaded where
import Data.Proxy

newtype Count x = Count { getCount :: Int } deriving (Show, Eq)

mapC :: (Int -> Int) -> Count x -> Count y
mapC f (Count x) = Count $ f x

liftC2 :: (Int -> Int -> Int) -> Count x -> Count y -> Count z
liftC2 op (Count x) (Count y) = Count $ x `op` y

coerce :: Count a -> Count b
coerce (Count n) = Count n

class Countable c where
  count' :: Proxy c -> Count c
  count' Proxy = count
  count :: Count c
  count = count' Proxy

class Factor f where
  factor' :: Countable c => Proxy c -> Count (f c)
  factor' Proxy = factor
  factor :: Countable c => Count (f c)
  factor = factor' Proxy

instance (Factor f, Countable c) => Countable (f c) where
  count = factor

Description updated: both approaches are mentioned now.
In Test Cases random types are generated, and I don't know how to do it without Proxy-s and existentials, so I cannot completely avoid using Proxy.

Yes, you are right, I have updated tests for Factor [].
Thank you for pointing it out!

Type Void has no constructors.
It could be defined:

{-# LANGUAGE EmptyDataDecls #-}
data Void

It is in base.