単語： 直積と直和は双対です。 λ記法 有向グラフ 射 閉圏 関手 双対 域・余域 終対象・始対象 錐・余錐 語句・文： 双対的に、関手の余極限からの射 関手の余極限からの射 双対的に、関手の余極限は余錐の圏の始対象の頂点になっている。余極限への射が一意…

モジュール（Leanモジュールと外部・他言語モジュール） 名前空間 セクション キーワード （module は無い、欲しかったが） import namespace section open ： pretectedなら修飾必要、privateは見えない。export は修飾なしになる。 scoped ： 名前空間内に…

数値ランク付きタグの構文は、例えば [s3] のように数字で終わる名前として、[printed 2023-02-11] のようなパラメータを持ったタグも欲しくなる。名前空間を識別する接頭辞付きタグをいれると、構造タグは： 名前空間接頭辞で修飾されたタグ 数値ランク付き…

自然数の具体的リテラルを (nat_lit 3) とか書くが、事情は不明。追記： /-- The `nat_lit n` macro constructs "raw numeric literals". This corresponds to the `Expr.lit (.natVal n)` constructor in the `Expr` data type. Normally, when you write a…

罪も多い。次を混乱させてしまった。 指標とモデル圏 パラメータ付き指標とファイバー付きモデル圏 忘却射影に対するセクション（so-called インスタンス） ひとつのモデル モデル圏／ファイバー付きモデル圏のあいだの関手（構成手続き） 特に、ファイバー…

({foo := "hello"} : Bar) の代わりに、{foo := "hello" : Bar} が使える。 namespace Temp structure Bar where foo : String := "hello" baz : String := foo ++ "world" #check {foo := "hi" : Bar} #check { : Bar} #eval { : Bar}.baz instance : ToStr…

自然数集合から可換モノイドへのインスタンスメーカーが3つあって、 足し算 掛け算 最大値（小さくないほう） 最小公倍数 それとは別に、ベキ等可換モノイド（演算記号 ◇）をジョイン（演算記号 ∨）半束にするインスタンスメーカーがあるとする。インスタン…

指標Σに対して、モデルの集合は |Model[Σ]| となる。適当な集合 K からの写像 K → |Model[Σ]| をインスタンスメーカー〈クリエイター | コンストラクタ | ビルダー〉と呼ぶ。なんらかの忘却射影 U:|Model[Σ]| → K があり、インスタンスメーカーがセクション…