Proofgold Object

λ x0 . and (struct_b x0) (unpack_b_o x0 (λ x1 . λ x2 : ι → ι → ι . and (∀ x3 . x3 ∈ x1 ⟶ bij x1 x1 (x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ bij x1 x1 (λ x4 . x2 x4 x3))))

type
ι → ο

theory
HotG

name
Quasigroup

definition
PUMEt..

Megalodon
struct_b_quasigroup

proofgold address
TMSVh..^{struct_b_quasigroup}

creator
9727 PrCx1../8a2ed..

owner
9727 PrCx1../8a2ed..

term root
d858c..