はじめに 二項関係から生成される関係 同値類 同値類と同値関係の性質 はじめに 数学の勉強をしていると、関係 を次の等式を含むような最小の同値関係とする、という定義がよく出てきます。 しかし、この定義は関係 の具体的な構成を与えていないので、この…

Steve Awodey の Category Theory を読む シリーズトップ 3.2 Coproducts Example 3.5 Example 3.6 Example 3.9 Example 3.10 Proposition 3.11 3.4 Coequalizers Example 3.20 参考書籍 3.2 Coproducts Example 3.5 を の UMP より を満たすただ一つの arro…

Steve Awodey の Category Theory を読む シリーズトップ 2.1 Epis and monos Example 2.4 a function is epic iff surjective in any epi into a projective object splits any retract of a projective object is projective 2.3 Generalized elements ult…

Steve Awodey の Category Theory を読む シリーズトップ はじめに 1.2 Functions of sets 1.4 Examples of categories 圏 Definition 1.2 poset category が poset であること Functor は monotone function monotone function は Functor an example from …

はじめに length関数を実装する Gallina 風の実装 Ltac から Gallina へ Gallina の項を Ltac 呼び出しの結果として受け取る 気持ち悪い点 map関数(Ltac引数)を実装する map関数(Gallina引数)を実装する 最後に 参考書籍 はじめに Ltac は、Coq において証明…