次の記事の内容を今の言葉で書き直す。 n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編 セオリーとインスティチューション - (新) 檜山正幸のキマイラ飼育記 メモ編

指標と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog) パート分けと多パート指標〈multipart signature〉は、テレスコープで解釈できる。法則パートを定義できれば、有法則指標と無法則指標の概念も定義できる。$`(S \sqsubseteq T)`$ のとき、$`S`$ が無法…

$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$ $`\cat{Sign}`$ 指標の圏 $`\cat{Alg}`$ 代数の圏 $`\mathbb{F}:\cat{Sign} \dashv \cat{Alg} : \mathbb{U}`$ 自由忘却随伴系 $`J:\ca…

本編でいつか書くかも知れない。

https://www.win.tue.nl/automath/archive/pdf/aut103.pdf Telescopic mappings in typed lambda calculus by N.G. de Bruijn ド・ブラウンのテレスコープ https://leanprover.github.io/reference/declarations.html#contexts-and-telescopes Leanのテレス…

相対指標と利用法 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Within}{ \sqsubseteq } `$指標の圏は $`\cat{Sign}`$ と書く。指標はローマン体大文字。指標…