Proofgold Object

λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . In_rec_iii (λ x2 . λ x3 : ι → ι → ι → ι . If_iii (ordinal x2) (λ x4 . If_ii (prim1 x4 (56ded.. (4ae4a.. x2))) (x0 x4 (λ x5 . x3 (e4431.. x5) x5)) (Descr_ii (λ x5 : ι → ι . True))) (λ x4 . Descr_ii (λ x5 : ι → ι . True))) (e4431.. x1) x1

type
(ι → (ι → ι → ι) → ι → ι) → ι → ι → ι

theory
HoTg

name
-

definition
PUTG4..

Megalodon
-

proofgold address
TMGPb..

creator
3831 PrGxv../a9b2e..

owner
3831 PrGxv../a9b2e..

term root
b16fa..