The Hierarchy of Core Terms in Agda

agda.dot

digraph AgdaCoreTermHierarchy {
    rankdir=BT;
    fontname="Helvetica,Arial,sans-serif";
    
    nodesep=0.7;
    ranksep=0.9;

    node [shape=box, style="rounded,filled", fillcolor="#f0f8ff", fontname="Helvetica,Arial,sans-serif", penwidth=1.5, color="#4682b4"];
    edge [color="#d35400", fontname="Helvetica,Arial,sans-serif", fontsize=11, fontcolor="#d35400"];

    // ==========================================
    // Layers
    // ==========================================

    subgraph cluster_values {
        label = "Layer 0: Values, function implementations, and proof witnesses";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        
        "3"; "true";
        "λ x → not x" [fillcolor="#e1ffff", color="#008b8b"];
        "λ m n → m + n" [fillcolor="#e1ffff", color="#008b8b"];
        "refl {lzero} {ℕ} {3}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set0_types {
        label = "Layer 1: Base types, function types, and propositions about values";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        
        "ℕ"; "Bool";
        "Bool → Bool" [fillcolor="#e1ffff", color="#008b8b"];
        "ℕ → ℕ → ℕ" [fillcolor="#e1ffff", color="#008b8b"];
        "3 ≡ 3" [fillcolor="#fffacd", color="#b8860b"];
        "refl {lsuc lzero} {Set₀} {Bool}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set1_types {
        label = "Layer 2: Set₀, polymorphic types, and propositions over Set₀";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₀" [fillcolor="#e6e6fa", color="#9370db"];
        "ℕ ≡ Bool" [fillcolor="#fffacd", color="#b8860b"];
        "Bool ≡ Bool" [fillcolor="#fffacd", color="#b8860b"];
        "{A : Set₀} → A → A" [fillcolor="#e0ffe0", color="#2e8b57"];
        "refl {lsuc (lsuc lzero)} {Set₁} {Set₀}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set2_types {
        label = "Layer 3: Set₁ and propositions over Set₁";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₁" [fillcolor="#e6e6fa", color="#9370db"];
        "Set₀ ≡ Set₀" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set3_types {
        label = "Layer 4: Set₂ ... and so on";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₂" [fillcolor="#e6e6fa", color="#9370db"];
    }

    "Set₃..." [shape=none, fillcolor=none, color=none];

    // ==========================================
    // Typing Judgments
    // ==========================================

    // --- Layer 0 → Layer 1 ---
    "3" -> "ℕ" [label=" : "];
    "true" -> "Bool" [label=" : "];
    "λ x → not x" -> "Bool → Bool" [label=" : "];
    "λ m n → m + n" -> "ℕ → ℕ → ℕ" [label=" : "];
    "refl {lzero} {ℕ} {3}" -> "3 ≡ 3" [label=" : "];

    // --- Layer 1 → Layer 2 ---
    "ℕ" -> "Set₀" [label=" : "];
    "Bool" -> "Set₀" [label=" : "];
    "Bool → Bool" -> "Set₀" [label=" : "];
    "ℕ → ℕ → ℕ" -> "Set₀" [label=" : "];
    "3 ≡ 3" -> "Set₀" [label=" : "];
    "refl {lsuc lzero} {Set₀} {Bool}" -> "Bool ≡ Bool" [label=" : "];

    // --- Layer 2 → Layer 3 ---
    "Set₀" -> "Set₁" [label=" : "];
    "ℕ ≡ Bool" -> "Set₁" [label=" : "];
    "Bool ≡ Bool" -> "Set₁" [label=" : "];
    "{A : Set₀} → A → A" -> "Set₁" [label=" : "];
    "refl {lsuc (lsuc lzero)} {Set₁} {Set₀}" -> "Set₀ ≡ Set₀" [label=" : "];

    // --- Layer 3 → Layer 4 ---
    "Set₁" -> "Set₂" [label=" : "];
    "Set₀ ≡ Set₀" -> "Set₂" [label=" : "];

    // --- Extends infinitely ---
    "Set₂" -> "Set₃..." [label=" : "];
}

agda_zh_TW.dot

digraph AgdaCoreTermHierarchy {
    rankdir=BT;
    fontname="Helvetica,Arial,sans-serif";
    
    nodesep=0.7;
    ranksep=0.9;

    node [shape=box, style="rounded,filled", fillcolor="#f0f8ff", fontname="Helvetica,Arial,sans-serif", penwidth=1.5, color="#4682b4"];
    edge [color="#d35400", fontname="Helvetica,Arial,sans-serif", fontsize=11, fontcolor="#d35400"];

    // ==========================================
    // 層級劃分
    // ==========================================

    subgraph cluster_values {
        label = "第 0 層：值、函數實作與證明實體";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        
        "3"; "true";
        "λ x → not x" [fillcolor="#e1ffff", color="#008b8b"];
        "λ m n → m + n" [fillcolor="#e1ffff", color="#008b8b"];
        "refl {lzero} {ℕ} {3}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set0_types {
        label = "第 1 層：基礎型別、函數型別與關於值的命題";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        
        "ℕ"; "Bool";
        "Bool → Bool" [fillcolor="#e1ffff", color="#008b8b"];
        "ℕ → ℕ → ℕ" [fillcolor="#e1ffff", color="#008b8b"];
        "3 ≡ 3" [fillcolor="#fffacd", color="#b8860b"];
        "refl {lsuc lzero} {Set₀} {Bool}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set1_types {
        label = "第 2 層：Set₀、多型與 Set₀ 上的命題";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₀" [fillcolor="#e6e6fa", color="#9370db"];
        "ℕ ≡ Bool" [fillcolor="#fffacd", color="#b8860b"];
        "Bool ≡ Bool" [fillcolor="#fffacd", color="#b8860b"];
        "{A : Set₀} → A → A" [fillcolor="#e0ffe0", color="#2e8b57"];
        "refl {lsuc (lsuc lzero)} {Set₁} {Set₀}" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set2_types {
        label = "第 3 層：Set₁ 與 Set₁ 上的命題";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₁" [fillcolor="#e6e6fa", color="#9370db"];
        "Set₀ ≡ Set₀" [fillcolor="#fffacd", color="#b8860b"];
    }

    subgraph cluster_set3_types {
        label = "第 4 層：Set₂ ⋯ 以此類推";
        style = dashed; color = "#888888"; fontcolor = "#555555";
        "Set₂" [fillcolor="#e6e6fa", color="#9370db"];
    }

    "Set₃..." [shape=none, fillcolor=none, color=none];

    // ==========================================
    // Typing Judgments
    // ==========================================

    // --- 第 0 層 → 第 1 層 ---
    "3" -> "ℕ" [label=" : "];
    "true" -> "Bool" [label=" : "];
    "λ x → not x" -> "Bool → Bool" [label=" : "];
    "λ m n → m + n" -> "ℕ → ℕ → ℕ" [label=" : "];
    "refl {lzero} {ℕ} {3}" -> "3 ≡ 3" [label=" : "];

    // --- 第 1 層 → 第 2 層 ---
    "ℕ" -> "Set₀" [label=" : "];
    "Bool" -> "Set₀" [label=" : "];
    "Bool → Bool" -> "Set₀" [label=" : "];
    "ℕ → ℕ → ℕ" -> "Set₀" [label=" : "];
    "3 ≡ 3" -> "Set₀" [label=" : "];
    "refl {lsuc lzero} {Set₀} {Bool}" -> "Bool ≡ Bool" [label=" : "];

    // --- 第 2 層 → 第 3 層 ---
    "Set₀" -> "Set₁" [label=" : "];
    "ℕ ≡ Bool" -> "Set₁" [label=" : "];
    "Bool ≡ Bool" -> "Set₁" [label=" : "];
    "{A : Set₀} → A → A" -> "Set₁" [label=" : "];
    "refl {lsuc (lsuc lzero)} {Set₁} {Set₀}" -> "Set₀ ≡ Set₀" [label=" : "];

    // --- 第 3 層 → 第 4 層 ---
    "Set₁" -> "Set₂" [label=" : "];
    "Set₀ ≡ Set₀" -> "Set₂" [label=" : "];

    // --- 無限延伸 ---
    "Set₂" -> "Set₃..." [label=" : "];
}