Proofgold Object

λ x0 x1 . pack_b {x2 ∈ setexp x0 x0|and (bij x0 x0 (ap x2)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))

type
ι → ι → ι

theory
HotG

name
symgroup_fixing

definition
PUMaE..

Megalodon
symgroup_fixing

proofgold address
TMFNy..^{symgroup_fixing}

creator
4924 Pr6Pc../0f9c5..

owner
4924 Pr6Pc../0f9c5..

term root
683be..