小编Ale*_*cki的帖子

我有以下内容：

open import Agda.Builtin.Equality\nopen import Agda.Builtin.Nat renaming (Nat to \xe2\x84\x95)\nopen import Agda.Builtin.Sigma\nopen import Agda.Primitive\n\n_\xc3\x97_ : {n m : Level} (A : Set n) (B : Set m) \xe2\x86\x92 Set (n \xe2\x8a\x94 m)\nX \xc3\x97 Y = \xce\xa3 X (\xce\xbb _ \xe2\x86\x92 Y)\n\n\xe2\x84\x95\xc2\xb2 : Set\n\xe2\x84\x95\xc2\xb2 = \xe2\x84\x95 \xc3\x97 \xe2\x84\x95 \n\ncanonical : \xe2\x84\x95\xc2\xb2 \xe2\x86\x92 \xe2\x84\x95\xc2\xb2\ncanonical (x , 0) = (x , 0)\ncanonical (0 , y) = (0 , y)\ncanonical (suc x , suc y) = canonical (x , y)\n\np1 : (a : …