Proofgold Term Root Disambiguation

∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 . PreContinuousHom (pack_c x0 x2) (pack_c x1 x3) x4 = and (x4 ∈ setexp x1 x0) (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ x7 ∈ x1) ⟶ x3 x6 ⟶ x2 (λ x7 . and (x7 ∈ x0) (x6 (ap x4 x7))))

as obj
-

as prop
5059f..^{Hom_struct_c_pack}

theory
HotG

stx
820be..

address
TMFYK..^{Hom_struct_c_pack}