According to the paper you linked, I think the answer to the question you want to ask is, "no." Pentation is not definable in a stratified version of system F.
The paper says that their system can define every super-elementary function, and all definable functions are super-elementary. The super-elementary functions are level $\mathcal{E}^4$ in the Grzegorczyk hierarchy, and according to wikipedia, moving to the next hyper-operation requires one additional step in that hierarchy. So, $\mathcal{E}^4$ contains tetration, products and sums of tetration, and finite compositions of tetration, but pentation isn't included until $\mathcal{E}^5$. So it is beyond the capabilities of the stratified system F.
This also answers your other question (of course), because the union of all levels in the Grzegorczyk hierarchy is exactly the primitive recursive functions, and the Ackermann function is not primitive recursive. So it cannot be defined.
Now, Agda of course is capable of defining pentation (and the Ackermann function), because any Church numeral can be used to get an equivalent value of the inductively defined natural numbers, and then those can be used to compute the function and converted back to a Church numeral. But presumably that's not what you're interested in.
However, there is also another possibility. Agda's predefined universes are closed under induction-recursion. This means that (in a way) they contain universes of their own, and far, far more universes than exist in the predicative system presented in the paper (which only has $\omega$ many universes, I believe). You can of course define Church numerals for each of these universes. But, I do not know what effect adding quantity of universes (and ignoring structure besides Pi types) has on the ability to define functions on the Church numerals.
Edit:
I did some additional investigation to expand on my last idea, and was able to define pentation of Church numerals. Here is some code, with explanations.
module Pent where
open import Function
open import Level hiding (suc)
open import Data.Unit
import Data.Product
import Data.Nat as N
open N using (ℕ)
Most of this is just for convenience. I won't be cheating with the natural numbers, but they're easier to visualize at the end.
The following exhibits Set as a Mahlo universe. This means that for any A : Set and B : A → Set, there is a universe U : Set that is itself closed under A and B
module Mahlo (A : Set) (B : A → Set) where
data U : Set
T : U → Set
data U where
A' : U
B' : A → U
Π : (s : U) (f : T s → U) → U
syntax Π s (λ x → t) = Π[ x ∈ s ] t
T A' = A
T (B' a) = B a
T (Π s f) = (x : T s) → T (f x)
infixr 4 _⇒_
_⇒_ : U → U → U
a ⇒ b = Π[ _ ∈ a ] b
I haven't included any universe structure in U besides Pi types. But this means that we can define the type of Church numerals over U, and easily build up to exponentiation of such numerals:
CH : Set
CH = (r : U) → (T r → T r) → T r → T r
zro : CH
zro r s z = z
suc : CH → CH
suc m r s = s ∘ m r s
one : CH
one = suc zro
infixl 10 _+_
_+_ : CH → CH → CH
(m + n) r s = m r s ∘ n r s
infixl 20 _×_
_×_ : CH → CH → CH
(m × n) r = m r ∘ n r
infixr 30 _^_
_^_ : CH → CH → CH
(m ^ n) r = n (r ⇒ r) (m r)
However, that is where we get stuck for 'generic' universes about which we know nothing but that they have Pi types (i.e. we don't really know anything about A and B).
Next we define Church numerals valued in arbitrary Set levels:
CHURCH : (α : Level) → Set (Level.suc α)
CHURCH α = ∀(R : Set α) → (R → R) → (R → R)
It is possible to define tetration of CHURCH zero as follows:
_↑_ : CHURCH zero → CHURCH zero → CHURCH zero
(m ↑ n) R s z = n CH (_^_ m') one R' s z
where
open Mahlo R (const ⊤) renaming (A' to R')
m' : CH
m' = m CH suc zro
So, this might not look like anything special is going on, but it's actually a bit crazier than it first appears. We have two Church numerals over Set, and R : Set that is our result type. So, we use the fact that Set is Mahlo to find a universe U inside Set that contains R. This means that Church numerals over U also live inside Set, which means we can 1) lower our big church numeral m into them, and 2) repeatedly exponentiate the lowered numeral by itself n times. And since U contains R, the numeral we construct is able to iterate the R → R function on the R value to give our answer.
Now, since tetration is defined with a uniform type, it's easy to define pentation as you defined tetration:
_⇈_ : CHURCH zero → CHURCH (Level.suc zero) → CHURCH zero
(m ⇈ n) = n (CHURCH zero) (_↑_ m) (λ R s z → s z)
If you want to visualize the results, you can use the following:
module Visualize where
open Data.Product
toCH : ∀{α} → ℕ → CHURCH α
toCH 0 R s z = z
toCH (N.suc n) R s z = s (toCH n R s z)
fromCH : ∀{α} → CHURCH α → ℕ
fromCH m = lower $ m (Lift _ ℕ) (lift ∘ N.suc ∘ lower) (lift N.zero)
lift₀ : (CHURCH zero → CHURCH zero → CHURCH zero) → ℕ → ℕ → ℕ
lift₀ op m n = fromCH (op (toCH m) (toCH n))
lift₁ : (CHURCH zero → CHURCH (Level.suc zero) → CHURCH zero) → ℕ → ℕ → ℕ
lift₁ op m n = fromCH (op (toCH m) (toCH n))
2↑2 2↑3 2↑4 3↑2 3↑3 : ℕ
2↑2 = lift₀ _↑_ 2 2
2↑3 = lift₀ _↑_ 2 3
2↑4 = lift₀ _↑_ 2 4
3↑2 = lift₀ _↑_ 3 2
3↑3 = lift₀ _↑_ 3 3
2⇈2 2⇈3 : ℕ
2⇈2 = lift₁ _⇈_ 2 2
2⇈3 = lift₁ _⇈_ 2 3
tetr : ℕ
tetr = 3↑3
pent : ℕ
pent = 2⇈3
Note, I got tired of waiting for 3↑3 to finish.
So, just to go back a bit, the universe creation principle I used was basically: for every set $R$ there exists a universe $U$ with $R \in U$, which is basically the Grothendieck universe axiom, except all of these universes are themselves inside the universe Set (and the universes are much weaker than set theoretic universes). But this is actually just scratching the surface of how powerful Mahlo is, because you'll notice I essentially did nothing with the B family. So I'm confident you can go beyond pentation with this. This is just the easiest one step further.
(To expand slightly on the last paragraph, the axiom "there exists a universe $V$ such that for every set $S \in V$ there exists a universe $U \in V$ such that $S \in U$" means (if I understand correctly) that $V$ is related to a 1-inaccessible cardinal/ordinal. But Mahlo cardinals/ordinals are hyper-hyper-hyper-...-inaccessible, which is well beyond that.)
Edit 2:
Here is a simpler development showing how you can define uniform tetration with $\omega+1$ universe levels. It uses the latest Agda to be able to talk about Setω, but you might be able to do it in older Agda versions if you inline CHURCH.
module PentPoly where
open import Level
open import Function
open import Agda.Primitive
module Gen (α : Level) where
Church : Set (suc α)
Church = ∀(R : Set α) → (R → R) → (R → R)
one : Church
one R s z = s z
_+_ : Church → Church → Church
(m + n) R s = n R s ∘ m R s
_×_ : Church → Church → Church
(m × n) R = n R ∘ m R
_^_ : Church → Church → Church
(m ^ n) R = n (R → R) (m R)
CHURCH : Setω
CHURCH = ∀(α : Level) (R : Set α) → (R → R) → (R → R)
_↑_ : CHURCH → CHURCH → CHURCH
(m ↑ n) α R s z = n (suc α) Church (_^_ m') one R s z
where
open Gen α
m' : Church
m' = m α
I think the way to think about this is that we're taking advantage of Setω being a limit of the universes below it. So any iteration we are asked to do occurs at some particular level below it, and we can iterate exponentiation one level above that. I think this means that we can get all hyper-operations with 'only' $\omega \cdot \omega$ universes.
I also realized my Mahlo above is wrong. It says that for every family on Set there is a universe (U,T) that contains that family. But Mahlo is actually the property that for every mapping between families of sets, there is a universe such that the mapping restricts to that universe. This looks like:
module Mahlo
(f₁ : (X : Set) → (X → Set) → Set)
(f₂ : (X : Set) → (Y : X → Set) → f₁ X Y → Set)
where
data U : Set
T : U → Set
data U where
Π : (x : U) → (y : T x → U) → U
reflect₁ : (x : U) → (y : T x → U) → U
reflect₂ : (x : U) → (y : T x → U) → f₁ (T x) (T ∘ y) → U
T (Π x y) = (v : T x) → T (y v)
T (reflect₁ x y) = f₁ (T x) (T ∘ y)
T (reflect₂ x y z) = f₂ (T x) (T ∘ y) z
res : Σ[ x ∈ U ] (T x → U) → Σ[ x ∈ U ] (T x → U)
res (x , y) = (reflect₁ x y , reflect₂ x y)
But this is even further unnecessary power from the perspective of the original question.
