Proofgold Object

λ x0 . λ x1 : ι → ι . {x2 ∈ prim4 (lam x0 (λ x2 . prim3 (x1 x2)))|∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3}

type
ι → (ι → ι) → ι

theory
HotG

name
Pi

definition
PUdQg..

Megalodon
Pi

proofgold address
TMb8z..^Pi

creator
4899 Pr6Pc../10032..

owner
4899 Pr6Pc../10032..

term root
40f1c..