Let $A$ be a ring and $I$ be an ideal, the followings are equivalent conditions to say that $I$ is prime

1. $I$ is prime if $ab \in I$ than $a \in I$ or $b \in I$ for all $a,b \in A$
2. $I$ is prime if $A / I$ is an integral domain

Proof

Backward

Let $A / I$ be an integral domain, that's say if $x, y \in A / I$ and $xy = 0$ , then $x = 0$ or $y = 0$ . Let $(a + I)(b + I)$ be the zero element of $I$ (i.e. $(0 \in A) + I$ ), then $ab + I = I$ . Hence $a + I = I$ or $b + I = I$ , implies $a \in I$ or $b \in I$ .

Forward

Let $I$ be a prime ideal, let

then $ab \in I$ and therefore, $a \in I$ or $b \in I$ . Hence $a + I$ or $b + I$ is the zero coset in $A / I$ .

前提

1. 每個節點入場的時候都分配到一個代數（generation），這個數字是唯一的
2. 第一個啟動節點直接當選

當原始的領導者掛了（一段時間無回應），注意到這點的節點就開始問比自己老的所有節點是不是還活著

1. 收到 alive 回應，或是得到其他更高優先順序的候選節點資訊。
2. 從中選出最老（代數數字最小）的節點告知它當選了，當選節點會廣播自己當選的消息。

問題

1. 注意到領導者無回應而發起投票的節點可以超過一個
2. 兩個發起投票的節點有連線的節點當然可能不同

比如 5 6 都注意到 1 死亡，發起投票。3 4 跟 5 有連線於是選出 2；2 3 跟 6 有連線於是選出 3。這時候 2 3 就都覺得自己是領導者了，而且 5 對 6 的通知還是更不正確的結果。

當然補上當選節點廣播之後，較年輕的當選者會自己去除這個屬性也是可以，但這中間會有一小段時間可能發生（以資料庫而言）雙重寫入而遺失資料。

而且要注意到實際上當然可以比這麻煩的多，比如通訊密集時，更容易讓 leader 過載；同時 90% 的節點都發現這點並發起投票，那麼消除腦分裂前的混亂就會特別嚴重。

這是 An informal introduction to topos theory 的閱讀筆記，Leinster 在這裡說 generalized elements 可以說是 Category 的 internal language。而 set theoretic 裡面使用 element 的論證多半都能改用這樣的語言進行，甚至，不使用 LEM 與 AC 的構造式證明，可以在任意 topos 中使用。

除了在 Generalized element 已經討論過的 product $(x, y)$ ，topos 還有 exponentials $Y^X$ ，equalizer 也可以記為

表示 $X \rightrightarrows Y$ 。

這樣就無需使用大量的 diagram，而是採用數學家已經熟悉的集合式的論證即可。

Let $\mathcal{E}$ be a category, and let $A$ be an object of $\mathcal{E}$ . A generalized element of $A$ is simply a map in $\mathcal{E}$ with codomain $A$ .

A generalized element $x : S \to A$ is shape $S$ or $S$ -element of $A$ .

When $S = 1$ (the terminal) then $S$ -elements are called global elements.

Global elements can be very boring, for example in the category of groups.

The language of generalized elements is the internal language of the category. For example, let $\mathcal{E}$ be a category with finite products. An $S$ -element of $X \times Y$ consists of two component $x : S \to X, y : S \to Y$ and is denoted by $(x,y)$ , hence extended the notation of set-theoretic Cartesian product of global elements.

Let $M, N$ be differentiable manifolds (dimensions are $m$ and $n$ respectively). A differentiable map $\varphi : M \to N$ is said to be an immersion if

is injective for all $p \in M$ .

If in addition, $\varphi$ is a homeomorphism onto $\varphi(M) \subset N$ , where $\varphi(M)$ has the subspace topology induced from $N$ , then $\varphi$ is an embedding.

If $M \subset N$ and the inclusion $M \subset N$ is an embedding, then $M$ is a submanifold of $N$ .

Suppose $F \dashv G$ is an adjunction, and $G : B \to A$ is fully faithful, then counit $\varepsilon : FG \to 1_B$ is an isomorphism

Proof

Forward direction

To prove counit $\varepsilon_B : FG(B) \to B$ is an isomorphism, we need to find an inverse $\varepsilon^{-1}$ and show pre and post composition of them are identity. Let $\varepsilon^{-1} := G^{-1}\eta$ , then we have two targets

1. $\varepsilon^{-1} \gg \varepsilon = id_X$

   Apply $G$ to get

   $$\boxed{G G^{-1} \eta = G \varepsilon^{-1}} \gg G \varepsilon = id_{G(X)}$$

   hence the target is $\eta \gg G \varepsilon = id_{G(X)}$ , right triangle fills the target.

2. $\varepsilon \gg \varepsilon^{-1} = id_{FG(X)}$

   Use counit naturality on $\varepsilon^{-1}$ to get

   $$F \eta \gg \varepsilon_{FG(B)} = \varepsilon_B \gg \boxed{\varepsilon^{-1} = G^{-1}\eta}$$

   Therefore, we have target $F \eta \gg \varepsilon_{FG(B)} = id_{FG(X)}$ , left triangle fills the target.

Backward direction

For $G$ is faithful, we want to know if $Gf = Gg$ then $f = g$ . We first obtain two equations via naturality of counit:

Replace $Gf$ with $Gg$ then we have $\varepsilon_X \gg f = \varepsilon_X \gg g$ , counit is an isomorphism and hence left-cancellable, $f = g$ .

For $G$ is full, we want to show every $f$ there is a $a$ such that $G a = f$ . Let $a = \varepsilon_X^{-1} \gg \varphi^{-1} f$ (where $\varphi$ is the hom-set equivalence of adjunction), this is same as asking

because isomorphism property, we have

now we use isomorphism to cancel right, so $G(\varepsilon_X^{-1}) = \eta_{GX}$ .

The counterexample in the category of sets is

We have $f(p(x)) = f(x)$ for all $x : 2$ , but $p$ is not identity. Where $1, 2$ represent the set with $1$ and $2$ elements, respectively.

tr 最開始我的想法是讓每一張卡片自己都輸出一個 HTML 網頁，然後就想到「哎糟糕，被嵌入 (transclude 概念) 的網頁會有重複的共用元素」就放棄了，當時認為所以必須像 forester 那樣用 XML 才行

好久以後我再次考慮（2025/05）實現一個 forester fork 時才想到，只要每張卡生成一個 a.index.html 一個 a.embed.html 就可以避免重複元素了

順著這個想法我用 iframe 嵌入來實現功能，直到我實在解不開 JS 的工作空間問題，這逼我思考其他方案。結果過了幾天我想到其實根本不用這麼麻煩xd，transclude 直接讀 embed 的內容就好了（並且 escape 排版確保不破壞 pre tag 等對排版敏感的內容）

現在剩下的問題就是其實 index 其實也沒必要再用 racket 生成一次，而是應該把 header, footer 等內容插入，讀取自己的 embed 檔案，但目前耦合比較多（依靠 generate-index? 判斷是否生成這些區塊），需要重新思考怎麼編排這些程式

基本操作

• △: 劍 牽制斬
• △ + O: 劍 突進斬
• O 長按: 劍 蓄力上撈斬
• R2 + △: 劍 變形斬
• R2 + O: 劍 充能

強化瓶系統

最有效率的集氣連技是: O 長按 → △

但魔物太靈活時這樣可能會一直落空，不一定要堅持這樣打

充能模式

1. 充能盾牌（紅盾）

1. R2 + O 之後保持 O 不放開
2. △ + O 三次接 R2
   • 突進斬
   • 盾突刺
   • 高解
   • 屬性強化迴旋斬

2. 充能劍（紅劍）

• R2 + O 後按住 △ 進行蓄力
• 放開後打出「劍：高壓屬性斬」

3. 充能斧（紅斧）

1. L2 瞄準用 R1 集中攻擊打到傷口（必須命中才會觸發）
2. 精準防禦之後按 △
3. 騎乘打出處決後觸發

出紅斧是為了能長按攻擊鍵 △ 或是 O 時，斧會持續輸出而不是只有一次輸出

This is came from when I'm formalizing lemma 1.3.11 of Basic Category Theory, I miss a precondition ($H$ below must be a natural transformation in the lemma) and try to prove an impossible thing.

Let $F, G : \mathcal{C} \to \mathcal{D}$ be functors, and a family

Does $H$ must be natural?

The exterior algebra of vector space $V$ is defined as a $\mathbb{Z}$ -graded algebra:

A map $i : A \to X$ of spaces has the homotopy extension property for a space $Y$ if

1. for each homotopy $H : A \times I \to Y$
2. and for each map $f : X \to Y$ with $f(i(a)) = H(a, 0)$ for all $a \in A$

there is a homotopy $H' : X \times I \to Y$ such that

for all $a \in A$ , $x \in X$ and $t \in I$ . The idea can be expressed in the following commutative diagram:

The homotopy $H'$ is called the extension of $H$ with initial condition $f$ .

Let $\mathcal{C}$ and $\mathcal{D}$ be categories, let $F, G : \mathcal{C} \to \mathcal{D}$ be functors. A natural transformation $\alpha : F \Rightarrow G$ is a function consists of

1. For each $X \in \mathcal{C}$ , there is a morphism $\alpha_X : F(X) \to G(X)$ in $\mathcal{D}$ , called the $X$ -component of $\alpha$
2. For every morphism $f : X \to Y$ in $\mathcal{C}$ , there is a commute diagram

   

Sterling 的 https://www.forester-notes.org/QHXX/index.xml 精確的描述了常青筆記可能遭遇的困難，關鍵在於，常青筆記對於不停變化的目標，如數學、電腦程式框架等存在，本體論的目標並不統一。用數學為例，我們傳統上接受 ZFC 作為「集合論」的本體，但 topos theory 的發展給出另一套定義 ETCS https://en.wikipedia.org/wiki/Elementary_Theory_of_the_Category_of_Sets！ETCS 說我們覺得集合論是「由 sets 與 functions 構成的 well-pointed topos，有自然數 object 與 Epics split」。

這個定義並沒有循環定義（但使用了短語簡化說法），因為 sets 跟 functions 的公理可以直接給出，ETCS 並沒有比 ZFC 不穩固。

事實上我們甚至知道 ETCS 跟 ZFC 的差異，ETCS + replacement（https://en.wikipedia.org/wiki/Axiom_schema_of_replacement）等價於 ZFC 的推理能力。ZFC 中的某部份等價於 ETCS（參考 Sheaves in Geometry and Logic: A First Introduction to Topos Theory VI. 10）

重點是，既然沒辦法保證討論主題的永久不變，那就應該紀錄當下對主題的洞見，因而在未來仍可從思想中復原出結構。

Let $A$ be a skew-symmetric endomorphism of a vector space $V$ (hence $A$ can also be view as a tensor: $A \in \Lambda^2 V$ ) and $N = \dim{V}$ is even, the Pfaffian of $A$ is the number $\text{Pf}\ A$ defined as the constant factor in the tensor equality:

where $\set{e_1,\dots,e_N}$ is an orthonormal basis of $V$ .

The sign of Pfaffian depends on the orientation of the orthonormal basis.

https://samtoth.github.io/agda-synthetic-categories/index.xml

If $f : S^n \to \R^n$ is continuous then there exists a point $x \in S^n$ such that $f(x) = f(-x)$ .

Proof

Define $g(x) = f(x) - f(-x)$ , $g$ is continuous.

By

$g$ is antipode-preserving.

By the lemma, there is a point $x \in S^n$ such that $g(x) = 0$ , so $f(x) - f(-x) = 0$ then $f(x) = f(-x)$ .

This problem arose from studying the book Lectures on the Geometry of Manifolds: Suppose $V$ is a real vector space, and $\omega : V \times V \to \mathbb{R}$ is a symplectic duality, then $V$ has even dimension.

I can make some concrete computation on dimension 2 and 3 and roughly understand the reason, but I have no general proof.

After a month, I found a solution:

https://abooij.github.io/wiwikwlhott/index.html

https://liamoc.net/forest/dt-001Y/index.xml

Code and Materials for an interactive online course on Logic (part of Strathclyde's CS208 Logic and Algorithms module)

1. project link: https://github.com/msp-strath/cs208-logic
2. site link: https://personal.cis.strath.ac.uk/robert.atkey/cs208/index.html

我使用的編輯器工具是 Agda Mode on VS Code，也可以用 emacs 之類的。常用操作有

• ctrl+c, ctrl+l 會編譯檢查檔案，假設程式中有 ?，會被替換成所謂的 hole {! !}，其實就是待寫的程式

• ctrl+c, ctrl+, 可以窺看 hole 的目標類型，與當前 context 有哪些 term 可用

• ctrl+c, ctrl+r 會把 hole 中你打的程式碼往前提取，當然前提是類型是正確的

• ctrl+c, ctrl+m 會把 hole 中你打的程式碼直接當成結果，一樣類型要是正確的

• 一般來說一個 agda 定義如下

  hello : A → B
  hello a = {! !}

  ctrl+c, ctrl+c 會問你要把哪個變數用構造子分開，回答 a，假設有 a1 與 a2 兩個構造子，程式就會變成

  hello : A → B
  hello a1 = {! !}
  hello a2 = {! !}

使用 Linux 的使用者可以更改預設的 copy/cut 指令以免衝突。

已完成的軟體這種概念，是指一個軟體的功能已經沒有大幅度更動的必要，可以長期使用在產品上，而軟體本身只會進行必要的安全與移植性更新。我在 https://josem.co/the-beauty-of-finished-software/ 讀到這個想法。對應到筆記軟體上，我不希望軟體一直更新，尤其是當我一打開工具需要寫筆記時，上面的更新按鈕非常的讓人煩躁。同時，這個想法也是一種解放我們原先對軟體想像的開端，比起軟體如何如何，更重要的是真的去做，外部連結裡面也談到冰與火之歌正是用這樣的軟體寫出。

In the original setup I already explain the configuration, to do the same with Protonmail will need to install Proton Mail Bridge(https://proton.me/mail/bridge), then with configuration as below.

[sendemail]
  smtpEncryption = STARTTLS
  smtpServer = 127.0.0.1
  smtpUser = <your id>@protonmail.com
  smtpServerPort = 1025
  smtpPass = <your password>

A morphism $A \xrightarrow{\phi} B$ is point-surjective iff for every point $1 \xrightarrow{q} B$ , there exists a point $1 \xrightarrow{p} A$ that lifts $q$ (satisfy $\phi \circ p = q$ ).

I use gmail, and hence, I need to get a Google app password. After having the password, one has to setup ~/.gitconfig with content:

[sendemail]
  smtpEncryption = tls
  smtpServer = smtp.gmail.com
  smtpUser = <your id>@gmail.com
  smtpServerPort = 587
  smtpPass = <your password>

Then you are able to use git send-email command:

git switch -c branch-patch
git format-patch main
git send-email 0001-***********.patch

prompt will ask some questions, an important one is which mailing list is your target? After command success, your patch are sent.

For certain git repository you're working on, can config local repository via git config --edit, and add below to omit email list in command line.

[sendemail]
  to = <target email list>

好處

1. 可以有效分類特定話題，例如一個串是講約去哪裡吃飯、另一個串講專業內容
2. 可以用僅限提及的人，限制可見性，所以可以形成一定程度的群組概念

壞處

1. 兩方站點的站長都能看到內容
2. 客戶端不支援把一群提及名單固定成群組，這或許是一個可行的客戶端新功能

壞處的可能解法：公佈自己的 public key 讓對方加密訊息再傳，配上專用客戶軟體或許可以做的更方便

All you need are deallocator and allocator from ffi/unsafe/alloc.

(require ffi/unsafe
         ffi/unsafe/define
         ffi/unsafe/alloc)

(define-ffi-definer define-xxx
  (ffi-lib "" '(#f)))

(define-xxx free-yyy (_fun _YyyRef -> _void)
  #:c-id yyy_delete
  #:wrap (deallocator))
(define-xxx make-yyy (_fun -> _YyyRef)
  #:c-id yyy_new
  #:wrap (allocator free-yyy))

Sometimes we didn't have public ip, but temporary wants to test website, ngrok can help in this situation.

# expose localhost:8080 by HTTP
$ ngrok http 8080
# expose localhost:8080 by TCP
$ ngrok tcp 8080

XDP is eXpress Data Path, it's a technology about putting a BPF code virtual machine on the NIC(network interface controller) driver before kernel network stack so that we can filter the packet before kernel, it would make processing speed greater.

We can do following things on the packet:

1. XDP_PASS: allow the packet to pass through
2. XDP_DROP: drop the packet
3. XDP_TX: bounce the packet back on the same interface
4. XDP_REDIRECT: redirects the packet to another interface

Here is an example of counting how many IPv4/6 packets be dropped.

package main

import (
    "fmt"
    "os"
    "os/signal"

    bpf "github.com/iovisor/gobpf/bcc"
)

// bcc is from iovisor/bcc this project
/*
#cgo CFLAGS: -I/usr/include/bcc/compat
#cgo LDFLAGS: -lbcc
#include 
#include 
void perf_reader_free(void *ptr);
*/
import "C"

const source string = `
#define KBUILD_MODNAME "foo"
#include 
#include 
#include 
#include 
#include 
#include 
#include 
BPF_TABLE("array", int, long, dropcnt, 256);
static inline int parse_ipv4(void *data, u64 nh_off, void *data_end) {
    struct iphdr *iph = data + nh_off;
    if ((void*)&iph[1] > data_end)
        return 0;
    return iph->protocol;
}
static inline int parse_ipv6(void *data, u64 nh_off, void *data_end) {
    struct ipv6hdr *ip6h = data + nh_off;
    if ((void*)&ip6h[1] > data_end)
        return 0;
    return ip6h->nexthdr;
}
int xdp_prog1(struct xdp_md *ctx) {
    void* data_end = (void*)(long)ctx->data_end;
    void* data = (void*)(long)ctx->data;
    struct ethhdr *eth = data;

    uint64_t nh_off = sizeof(*eth);
    if (data + nh_off  > data_end)
        return XDP_DROP;
    uint16_t h_proto = eth->h_proto;
    if (h_proto == htons(ETH_P_8021Q) || h_proto == htons(ETH_P_8021AD)) {
        struct vlan_hdr *vhdr;
        vhdr = data + nh_off;
        nh_off += sizeof(struct vlan_hdr);
        if (data + nh_off > data_end)
            return XDP_DROP;
            h_proto = vhdr->h_vlan_encapsulated_proto;
    }
    if (h_proto == htons(ETH_P_8021Q) || h_proto == htons(ETH_P_8021AD)) {
        struct vlan_hdr *vhdr;
        vhdr = data + nh_off;
        nh_off += sizeof(struct vlan_hdr);
        if (data + nh_off > data_end)
            return XDP_DROP;
            h_proto = vhdr->h_vlan_encapsulated_proto;
    }
    int index;
    if (h_proto == htons(ETH_P_IP))
        index = parse_ipv4(data, nh_off, data_end);
    else if (h_proto == htons(ETH_P_IPV6))
        index = parse_ipv6(data, nh_off, data_end);
    else
        index = 0;
    long *value;
    value = dropcnt.lookup(&index);
    if (value) lock_xadd(value, 1);
    return XDP_DROP;
}
`

func usage() {
    fmt.Printf("Usage: %v \n", os.Args[0])
    fmt.Printf("e.g.: %v eth0\n", os.Args[0])
    os.Exit(1)
}

func main() {
    if len(os.Args) != 2 {
        usage()
    }
    module := bpf.NewModule(source, []string{
        "-w",
    })
    defer module.Close()

    fn, err := module.Load("xdp_prog1", C.BPF_PROG_TYPE_XDP, 1, 65536)
    if err != nil {
        fmt.Fprintf(os.Stderr, "Failed to load xdp prog: %v\n", err)
        os.Exit(1)
    }

    device := os.Args[1]
    if err := module.AttachXDP(device, fn); err != nil {
        fmt.Fprintf(os.Stderr, "Failed to attach xdp prog: %v\n", err)
        os.Exit(1)
    }

    defer func() {
        if err := module.RemoveXDP(device); err != nil {
            fmt.Fprintf(os.Stderr, "Failed to remove XDP from %s: %v\n", device, err)
        }
    }()

    fmt.Println("Dropping packets, hit CTRL+C to stop")
    sig := make(chan os.Signal, 1)
    signal.Notify(sig, os.Interrupt, os.Kill)

    dropcnt := bpf.NewTable(module.TableId("dropcnt"), module)

    <-sig

    fmt.Println("\n{IP protocol-number}: {total dropped pkts}")
    for it := dropcnt.Iter(); it.Next(); {
        key := bpf.GetHostByteOrder().Uint32(it.Key())
        value := bpf.GetHostByteOrder().Uint64(it.Leaf())

        if value > 0 {
            fmt.Printf("%v: %v pkts\n", key, value)
        }
    }
}

Mark-Sweep is a classic GC algorithm, it's combined with two parts, mark and sweep.

mark(root):
  if not marked?(root):
    mark(root)
  for obj in knowns(root):
    mark(obj)
sweep(heap):
  for obj in heap:
    if marked?(obj):
      unmark(obj)
    else:
      release(obj)

If we run collection (mark-sweep), then since each object is reachable from root, so no one would be released.

After do some executions, obj1 don't need obj3 anymore, so it became:

Now when we run collection, obj3 is unreachable from root, so it won't be marked! When running to sweep, it will be dropped.