Proofgold Object

λ x0 x1 x2 . unpack_c_o x0 (λ x3 . λ x4 : (ι → ο) → ο . unpack_c_o x1 (λ x5 . λ x6 : (ι → ο) → ο . and (x2 ∈ setexp x5 x3) (∀ x7 : ι → ο . (∀ x8 . x7 x8 ⟶ x8 ∈ x5) ⟶ x6 x7 ⟶ x4 (λ x8 . and (x8 ∈ x3) (x7 (ap x2 x8))))))

type
ι → ι → ι → ο

theory
HotG

name
PreContinuousHom

definition
PUdXV..

Megalodon
Hom_struct_c

proofgold address
TMa74..^Hom_struct_c

creator
9630 PrCx1../ad422..

owner
9630 PrCx1../ad422..

term root
9dfc2..