Proofgold Term Root Disambiguation

∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . x4 ∈ prim6 (prim6 0)) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0

as obj
-

as prop
4e15c..^{MetaCatSmallSet_initial}

theory
HotG

stx
2772d..

address
TMQrf..^{MetaCatSmallSet_initial}