Proofgold Proposition

∃ x0 . ∃ x2 : ι → ι . MetaCat_initial_p (λ x4 . True) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x0 x2

type
prop

theory
HotG

name
-

proof
PUNFE..

Megalodon
MetaCatSet_initial

proofgold address
TMF8p..^{MetaCatSet_initial}

creator
9568 PrCx1../4973a..

owner
9568 PrCx1../4973a..

term root
64829..