Proofgold Object

λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . and (x0 x2 x2) (x2 = canonical_elt_def x0 x1 x2)

type
(ι → ι → ο) → (ι → ι) → ι → ο

theory
HoTg

name
quotient_def

definition
PUM2d..

Megalodon
-

proofgold address
TMGvL..

creator
4654 PrGxv../59558..

owner
4654 PrGxv../59558..

term root
612d4..