Ident 公理 Cut オペラッド結合 Weak 水増し Cont 冗長性縮約 contraは矛盾 Perm 交換 CtxAndIntroL CtxAndIntroR CtxtOrIntro CtXImpIntro （LJ変形） CtxNotIntro CtxUnivIntro CtxExIntro TrgAndIntro TrgOrIntroL TrgOrIntroR TrgImpIntro TrgNotIntro T…

等式の種類： definitional equality ： Leanカーネルが判定する項の同一性。システムレベルで「同じ」とみなす。 propositional equality ： 等値性を意味する命題（真か偽の文）。証明がないと保証されない。システムレベルで事前に成立している同一性では…

型付きJSON（むかし、XIONとかXJSON呼んでいたヤツ）をマクロで実装する。 ベキ等可換モノイドからジョイン半束を作る。 乗法ベキ等可換環のスペクトル理論（昔のブログ記事にある） 距離連続写像は位相連続写像である。 定義・証明だけでなくて組織化を注意…

型と計算 命題と証明 型演算／構成子 命題結合子 依存型構成子 限量子 型ファミリー (命題ファミリー) インデックス域 論域 インデックス 個体 インデックス変数 限量束縛変数 関数 保証 戻り型 結論命題 ターゲット型 ターゲット命題（質問の） 引数リスト …