Proofgold Object

λ x0 : ι → ι → ο . λ x1 : ι → ι . λ x2 . If_i (x0 x2 (x1 x2)) (x1 x2) (canonical_elt x0 x2)

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

theory
HoTg

name
canonical_elt_def

definition
PUM2d..

Megalodon
-

proofgold address
TMc7v..

creator
4654 PrGxv../40f9e..

owner
4654 PrGxv../40f9e..

term root
cd4f6..